Definitions: Mathlib.NumberTheory, part 2 of 3

MulCharstructureMathlib.NumberTheory.MulChar.Basic, type

Wording

multiplicative characteristic of R and #2 (from the name)

English

Let $R$ and $\mathrm{R'}$ be sets. Then the multiplicative characteristics of $R$ and $\mathrm{R'}$ are a basic type.

MulChar.IsQuadraticdefMathlib.NumberTheory.MulChar.Basic, predicate

Wording

x2 is quadratic (from the docstring)

English

Let $x_{2}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Then $x_{2}$ is quadratic, if for all elements $a$ of $R$, $\EqtMACRoH {x_{2} (a)}{0}$, $\EqtMACRoH {x_{2} (a)}{1}$ or $\EqtMACRoH {x_{2} (a)}{\operatorname{neg} (1)}$.

MulChar.domRestrictdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the restriction of T and x3 (from the docstring)

English

Let $T$ be an element of $S$. Let $x_{3}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Then the restriction of $T$ and $x_{3}$ is a multiplicative characteristic of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {T}{x_{4}})}$ and $\mathrm{R'}$ defined as the multiplicative characteristic of the composition of the unit homomorphism of $x_{3}$ and the map of the subtype of $T$.

MulChar.domRestrictHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the restriction of T and #2 (from the docstring)

English

Let $T$ be an element of $S$. Let $\mathrm{R''}$ be a set. Then the restriction of $T$ and $\mathrm{R''}$ is a monoid homomorphism of the set of multiplicative characteristics of $R$ and $\mathrm{R''}$ and the set of multiplicative characteristics of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {T}{x_{3}})}$ and $\mathrm{R''}$.

MulChar.equivToUnitHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the equivalence to unit homomorphism (from the name)

English

The equivalence to unit homomorphism is an equivalence from the set of multiplicative characteristics of $R$ and $\mathrm{R'}$ to the set of monoid homomorphisms of $\UnitsMACRoAO {R}$ and $\UnitsMACRoAO {\mathrm{R'}}$.

MulChar.invdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the inverse of x2 (from the docstring)

English

Let $x_{2}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Then the inverse of $x_{2}$ is a multiplicative characteristic of $R$ and $\mathrm{R'}$.

MulChar.muldefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the product of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be multiplicative characteristics of $R$ and $\mathrm{R'}$. Then the product of $x_{2}$ and $x_{3}$ is a multiplicative characteristic of $R$ and $\mathrm{R'}$.

MulChar.mulEquivToUnitHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the multiplicative equivalence to unit homomorphism (from the name)

English

The multiplicative equivalence to unit homomorphism is a multiplicative equivalence of the set of multiplicative characteristics of $R$ and $\mathrm{R'}$ and the set of monoid homomorphisms of $\UnitsMACRoAO {R}$ and $\UnitsMACRoAO {\mathrm{R'}}$.

MulChar.ofUnitHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the multiplicative characteristic of f (from the name)

English

Let $f$ be a monoid homomorphism of $\UnitsMACRoAO {R}$ and $\UnitsMACRoAO {\mathrm{R'}}$. Then the multiplicative characteristic of $f$ is a multiplicative characteristic of $R$ and $\mathrm{R'}$.

MulChar.ringHomCompdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the ring homomorphism composition of x3 and f (from the name)

English

Let $x_{3}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Let $f$ be a ring homomorphism of $\mathrm{R'}$ and $\mathrm{R''}$. Then the ring homomorphism composition of $x_{3}$ and $f$ is a multiplicative characteristic of $R$ and $\mathrm{R''}$.

MulChar.ringHomCompHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the ring homomorphism composition homomorphism of f (from the name)

English

Let $f$ be a ring homomorphism of $\mathrm{R'}$ and $\mathrm{R''}$. Then the ring homomorphism composition homomorphism of $f$ is a monoid homomorphism of the set of multiplicative characteristics of $R$ and $\mathrm{R'}$ and the set of multiplicative characteristics of $R$ and $\mathrm{R''}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x_{3}$ to the ring homomorphism composition of $x_{3}$ and $f$ and $\mathrm{MulChar\_\_ringHomComp\_one}$ applied to $f$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{MulChar\_\_ringHomComp\_mul}$ applied to $x_{4}$, $x_{5}$ and $f$.

MulChar.toMonoidWithZeroHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the monoid with zero homomorphism of x2 (from the name)

English

Let $x_{2}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Then the monoid with zero homomorphism of $x_{2}$ is a monoid with zero homomorphism of $R$ and $\mathrm{R'}$.

MulChar.toUnitHomdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the unit homomorphism of x2 (from the name)

English

Let $x_{2}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Then the unit homomorphism of $x_{2}$ is a monoid homomorphism of $\UnitsMACRoAO {R}$ and $\UnitsMACRoAO {\mathrm{R'}}$ defined as the map of the monoid homomorphism of $x_{2}$.

MulChar.trivialdefMathlib.NumberTheory.MulChar.Basic, function or constant

Wording

the trivial multiplicative character of R and #2 (from the docstring)

English

Let $R$ and $\mathrm{R'}$ be sets. Then the trivial multiplicative character of $R$ and $\mathrm{R'}$ is a multiplicative characteristic of $R$ and $\mathrm{R'}$.

MulCharClassclassMathlib.NumberTheory.MulChar.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$ and $\mathrm{R'}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulCharClass}$ holds for $F$, $R$ and $\mathrm{R'}$.

Mathlib.NumberTheory.MulChar.Duality

MulChar.mulCharEquivdefMathlib.NumberTheory.MulChar.Duality, function or constant

Wording

the multiplicative characteristic equivalence of M and R (from the name)

English

Let $M$ and $R$ be sets. Then the multiplicative characteristic equivalence of $M$ and $R$ is a multiplicative equivalence of the set of multiplicative characteristics of the set of multiplicative characteristics of $M$ and $R$ and $R$ and $\UnitsMACRoAO {M}$ defined as the composition of the multiplicative equivalence to unit homomorphism and the composition of the inverse of the left monoid homomorphism congruence of the unit and the composition of the left monoid homomorphism congruence of the multiplicative equivalence to unit homomorphism and the monoid homomorphism monoid homomorphism equivalence of $\UnitsMACRoAO {M}$ and $R$.

MulChar.subgroupOrderIsoSubgroupMulChardefMathlib.NumberTheory.MulChar.Duality, function or constant

Wording

the subgroup order isomorphism subgroup multiplicative characteristic of M and R (from the name)

English

Let $M$ and $R$ be sets. Then the subgroup order isomorphism subgroup multiplicative characteristic of $M$ and $R$ is an order isomorphism of the set of subgroups of $\UnitsMACRoAO {M}$ and the set of order duals of the set of subgroups of the set of multiplicative characteristics of $M$ and $R$ defined as the composition of the subgroup order isomorphism subgroup monoid homomorphism of $\UnitsMACRoAO {M}$ and $R$ and the dual of the map subgroup of the inverse of the multiplicative equivalence to unit homomorphism.

Mathlib.NumberTheory.MulChar.Lemmas

MulChar.equiv_rootsOfUnitydefMathlib.NumberTheory.MulChar.Lemmas, function or constant

Wording

the equivalence root of M and R (from the name)

English

Let $M$ and $R$ be sets. Then the equivalence root of $M$ and $R$ is a multiplicative equivalence of the set of multiplicative characteristics of $M$ and $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (\operatorname{card} (\UnitsMACRoAO {M}), R)}{x_{4}})}$.

MulChar.ofRootOfUnitydefMathlib.NumberTheory.MulChar.Lemmas, function or constant

Wording

the multiplicative characteristic of h and hg (from the name)

English

Assume that $x_{4}$ is an element of the root of the cardinality of $\UnitsMACRoAO {M}$ and $R$. Assume that for all units $x_{5}$ of $M$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{5}}$. Then the multiplicative characteristic of $h$ and $\mathrm{hg}$ is a multiplicative characteristic of $M$ and $R$.

MulChar.starCompdefMathlib.NumberTheory.MulChar.Lemmas, function or constant

Wording

the star composition of x3 (from the name)

English

Let $x_{3}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Then the star composition of $x_{3}$ is a multiplicative characteristic of $R$ and $\mathrm{R'}$ defined as the ring homomorphism composition of $x_{3}$ and the star ring end of $\mathrm{R'}$.

Mathlib.NumberTheory.NumberField.AdeleRing

NumberField.AdeleRingdefMathlib.NumberTheory.NumberField.AdeleRing, type

Wording

adele ring of R and K (from the name)

English

Let $R$ and $K$ be sets. Then an adele ring of $R$ and $K$ is an element of the function that maps $R$ and $K$ to $\mathrm{Prod}$ applied to the set of infinite adele rings of $K$ and the set of finite adele rings of $R$ and $K$.

NumberField.AdeleRing.ofAdicCompletiondefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the adele ring of v (from the name)

English

Let $R$ and $K$ be sets. Let $v$ be a height one spectrum of $R$. Then the adele ring of $v$ is a monoid homomorphism of the set of adic completions of $K$ and $v$ and the set of adele rings of $R$ and $K$ defined as the product of $1$ and the embedding of the completion of $K$ and $v$.

NumberField.AdeleRing.ofCompletiondefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the adele ring of v (from the name)

English

Let $R$ and $K$ be sets. Let $v$ be an infinite place of $K$. Then the adele ring of $v$ is a monoid homomorphism of the set of completions of $v$ and the set of adele rings of $R$ and $K$ defined as the product of the embedding of the completion of $v$ and $1$.

NumberField.AdeleRing.principalSubgroupdefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the principal subgroup of R and K (from the name)

English

Let $R$ and $K$ be sets. Then the principal subgroup of $R$ and $K$ is an additive subgroup of the set of adele rings of $R$ and $K$ defined as the additive subgroup of the range of the algebra map of $K$ and the set of adele rings of $R$ and $K$.

NumberField.IdeleClassGroupdefMathlib.NumberTheory.NumberField.AdeleRing, type

Wording

idele class group of R and K (from the name)

English

Let $R$ and $K$ be sets. Then an idele class group of $R$ and $K$ is an element of the function that maps $R$ and $K$ to the set of quotients of the set of idele groups of $R$ and $K$ and the principal subgroup of $R$ and $K$.

NumberField.IdeleClassGroup.ofAdicCompletiondefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the idele class group of v (from the name)

English

Let $R$ and $K$ be sets. Let $v$ be a height one spectrum of $R$. Then the idele class group of $v$ is a monoid homomorphism of the set of units of the set of adic completions of $K$ and $v$ and the set of idele class groups of $R$ and $K$ defined as the composition of $\operatorname{mk'}$ applied to the principal subgroup of $R$ and $K$ and the idele group of $v$.

NumberField.IdeleClassGroup.ofCompletiondefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the idele class group of v (from the name)

English

Let $R$ and $K$ be sets. Let $v$ be an infinite place of $K$. Then the idele class group of $v$ is a monoid homomorphism of the set of units of the set of completions of $v$ and the set of idele class groups of $R$ and $K$ defined as the composition of $\operatorname{mk'}$ applied to the principal subgroup of $R$ and $K$ and the idele group of $v$.

NumberField.IdeleGroupdefMathlib.NumberTheory.NumberField.AdeleRing, type

Wording

idele group of R and K (from the name)

English

Let $R$ and $K$ be sets. Then an idele group of $R$ and $K$ is an element of the function that maps $R$ and $K$ to the set of units of the set of adele rings of $R$ and $K$.

NumberField.IdeleGroup.ofAdicCompletiondefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the idele group of v (from the name)

English

Let $R$ and $K$ be sets. Let $v$ be a height one spectrum of $R$. Then the idele group of $v$ is a monoid homomorphism of the set of units of the set of adic completions of $K$ and $v$ and the set of idele groups of $R$ and $K$ defined as the map of the adele ring of $v$.

NumberField.IdeleGroup.ofCompletiondefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the idele group of v (from the name)

English

Let $R$ and $K$ be sets. Let $v$ be an infinite place of $K$. Then the idele group of $v$ is a monoid homomorphism of the set of units of the set of completions of $v$ and the set of idele groups of $R$ and $K$ defined as the map of the adele ring of $v$.

NumberField.IdeleGroup.principalSubgroupdefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the principal subgroup of R and K (from the name)

English

Let $R$ and $K$ be sets. Then the principal subgroup of $R$ and $K$ is a subgroup of the set of idele groups of $R$ and $K$ defined as the range of the unit embedding of $R$ and $K$.

NumberField.IdeleGroup.unitEmbeddingdefMathlib.NumberTheory.NumberField.AdeleRing, function or constant

Wording

the unit embedding of R and K (from the name)

English

Let $R$ and $K$ be sets. Then the unit embedding of $R$ and $K$ is a monoid homomorphism of $\UnitsMACRoAO {K}$ and the set of idele groups of $R$ and $K$ defined as the map of $\operatorname{toMonoidHom}$ applied to the algebra map of $K$ and the set of adele rings of $R$ and $K$.

Mathlib.NumberTheory.NumberField.Basic

NumberFieldclassMathlib.NumberTheory.NumberField.Basic, predicate

Wording

K is a number field (from the name)

English

Let $K$ be a set. Then we can say that $K$ is a number field.

NumberField.RingOfIntegersdefMathlib.NumberTheory.NumberField.Basic, type

Wording

ring of integer of K (from the name)

English

Let $K$ be a set. Then a ring of integer of $K$ is an element of the function that maps $K$ to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (\Integer , K)}{x_{1}})}$.

NumberField.RingOfIntegers.algEquivdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the algebra isomorphism of L and R (from the name)

English

Let $K$, $L$ and $R$ be sets. Then the algebra isomorphism of $L$ and $R$ is an algebra isomorphism of the set of rings of integer of $L$ and $R$ defined as the inverse of the equivalence of $L$ and the set of rings of integer of $L$.

NumberField.RingOfIntegers.basisdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the basis of K (from the name)

English

Let $K$ be a set. Then the basis of $K$ is a basis of $\Integer$ and the set of rings of integer of $K$ defined as $\operatorname{chooseBasis}$ applied to $\Integer$ and the set of rings of integer of $K$.

NumberField.RingOfIntegers.equivdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the equivalence of R (from the name)

English

Let $R$ be a set. Then the equivalence of $R$ is a ring isomorphism of the set of rings of integer of $K$ and $R$ defined as the ring isomorphism of the inverse of the equivalence of $K$ and the set of rings of integer of $K$.

NumberField.RingOfIntegers.mapAlgEquivdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the map algebra isomorphism of e (from the name)

English

Let $e$ be an element of $E$. Then the map algebra isomorphism of $e$ is an algebra isomorphism of the set of rings of integer of $K$ and the set of rings of integer of $L$.

NumberField.RingOfIntegers.mapAlgHomdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the algebra homomorphism of f (from the docstring)

English

Let $f$ be an element of $F$. Then the algebra homomorphism of $f$ is an algebra homomorphism of the set of rings of integer of $K$ and the set of rings of integer of $L$.

NumberField.RingOfIntegers.mapRingEquivdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the ring isomorphism of e (from the docstring)

English

Let $e$ be a ring isomorphism of $K$ and $L$. Then the ring isomorphism of $e$ is a ring isomorphism of the set of rings of integer of $K$ and the set of rings of integer of $L$.

NumberField.RingOfIntegers.mapRingHomdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the ring homomorphism of f (from the docstring)

English

Let $f$ be a ring homomorphism of $K$ and $L$. Then the ring homomorphism of $f$ is a ring homomorphism of the set of rings of integer of $K$ and the set of rings of integer of $L$.

NumberField.RingOfIntegers.restrictdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $M$ to elements of $K$ such that for all elements $x_{2}$ of $M$, $f$ applied to $x_{2}$ is integral. Let $x_{1}$ be an element of $M$. Then $\operatorname{restrict}$ applied to $f$, $h$ and $x_{1}$ is a ring of integer of $K$ defined as $f$ applied to $x_{1}$.

NumberField.RingOfIntegers.restrict_addMonoidHomdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $K$ such that for all elements $x_{2}$ of $M$, $f$ applied to $x_{2}$ is integral. Then $\mathrm{NumberField\_\_RingOfIntegers\_\_restrict\_addMonoidHom}$ applied to $f$ and $h$ is an additive monoid homomorphism of $M$ and the set of rings of integer of $K$.

NumberField.RingOfIntegers.restrict_monoidHomdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

no wording

English

Let $f$ be a monoid homomorphism of $M$ and $K$ such that for all elements $x_{2}$ of $M$, $f$ applied to $x_{2}$ is integral. Then $\mathrm{NumberField\_\_RingOfIntegers\_\_restrict\_monoidHom}$ applied to $f$ and $h$ is a monoid homomorphism of $M$ and the set of rings of integer of $K$.

NumberField.RingOfIntegers.valdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the value of x1 (from the name)

English

Let $x_{1}$ be a ring of integer of $K$. Then the value of $x_{1}$ is an element of $K$ defined as $\operatorname{algebraMap}$ applied to the set of rings of integer of $K$, $K$ and $x_{1}$.

NumberField.integralBasisdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the integral basis of K (from the name)

English

Let $K$ be a set. Then the integral basis of $K$ is a basis of $\Rational$ and $K$ defined as the localization localization of the non zero divisor of $\Integer$ and the basis of $K$.

Rat.ringOfIntegersEquivdefMathlib.NumberTheory.NumberField.Basic, function or constant

Wording

the ring (from the name)

English

The ring is a ring isomorphism of the set of rings of integer of $\Rational$ and $\Integer$ defined as the equivalence of $\Integer$.

Mathlib.NumberTheory.NumberField.CMField

NumberField.CMExtension.equivMaximalRealSubfielddefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the equivalence maximal real subfield of F and K (from the name)

English

Let $F$ and $K$ be sets. Then the equivalence maximal real subfield of $F$ and $K$ is a ring isomorphism of $F$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{maximalRealSubfield} (K)}{x_{3}})}$.

NumberField.IsCMFieldclassMathlib.NumberTheory.NumberField.CMField, predicate

Wording

no wording

English

Let $K$ be a set. Then we can say that $\operatorname{IsCMField}$ holds for $K$.

NumberField.IsCMField.complexConjdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the complex conjugate of K (from the name)

English

Let $K$ be a set. Then the complex conjugate of $K$ is an algebra isomorphism of $K$ and $K$.

NumberField.IsCMField.equivInfinitePlacedefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the equivalence infinite place of K (from the name)

English

Let $K$ be a set. Then the equivalence infinite place of $K$ is an element of $\EquivMACRoAE {\operatorname{InfinitePlace} (K)}{\operatorname{InfinitePlace} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{maximalRealSubfield} (K)}{x_{1}})})}$.

NumberField.IsCMField.indexRealUnitsdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the index of the subgroup of K (from the docstring)

English

Let $K$ be a set. Then the index of the subgroup of $K$ is a natural number defined as the index of the maximum of the real unit of $K$ and the torsion of $K$.

NumberField.IsCMField.realFundSystemdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

no wording

English

Let $K$ be a set. Let $i$ be an element of $\mathrm{Fin}$ applied to the rank of $K$. Then $\operatorname{realFundSystem}$ applied to $K$ and $i$ is a unit of the set of rings of integer of $K$.

NumberField.IsCMField.realUnitsdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the real unit of K (from the name)

English

Let $K$ be a set. Then the real unit of $K$ is a subgroup of $\UnitsMACRoAO {\operatorname{RingOfIntegers} (K)}$ defined as the range of the map of $\operatorname{toMonoidHom}$ applied to the algebra map of the set of rings of integer of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{maximalRealSubfield} (K)}{x_{1}})}$ and the set of rings of integer of $K$.

NumberField.IsCMField.ringOfIntegersComplexConjdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the ring of K (from the name)

English

Let $K$ be a set. Then the ring of $K$ is an algebra isomorphism of the set of rings of integer of $K$ and the set of rings of integer of $K$ defined as the map algebra isomorphism of the complex conjugate of $K$.

NumberField.IsCMField.unitsComplexConjdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the complex conjugation of K (from the docstring)

English

Let $K$ be a set. Then the complex conjugation of $K$ is a multiplicative equivalence of the set of units of the set of rings of integer of $K$ and the set of units of the set of rings of integer of $K$ defined as the map equivalence of the multiplicative equivalence of the ring isomorphism of the ring isomorphism of the complex conjugate of $K$.

NumberField.IsCMField.unitsMulComplexConjInvdefMathlib.NumberTheory.NumberField.CMField, function or constant

Wording

the unit multiplicative complex conjugate inverse of K (from the name)

English

Let $K$ be a set. Then the unit multiplicative complex conjugate inverse of $K$ is a monoid homomorphism of $\UnitsMACRoAO {\operatorname{RingOfIntegers} (K)}$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})}$.

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

NumberField.canonicalEmbeddingdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the canonical embedding of K (from the docstring)

English

Let $K$ be a set. Then the canonical embedding of $K$ is a ring homomorphism of $K$ and the set of functions from ring homomorphisms of $K$ and the set of complexes to complexes defined as the product of the function that maps $x_{1}$ to $x_{1}$.

NumberField.canonicalEmbedding.integerLatticedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the integer lattice of K (from the name)

English

Let $K$ be a set. Then the integer lattice of $K$ is a subring of the set of functions from ring homomorphisms of $K$ and the set of complexes to complexes defined as the map of the canonical embedding of $K$ and the range of the algebra map of the set of rings of integer of $K$ and $K$.

NumberField.canonicalEmbedding.latticeBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the lattice basis of K (from the name)

English

Let $K$ be a set. Then the lattice basis of $K$ is a basis of the set of complexes and the set of functions from ring homomorphisms of $K$ and the set of complexes to complexes.

NumberField.mixedEmbeddingdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the mixed embedding of K (from the docstring)

English

Let $K$ be a set. Then the mixed embedding of $K$ is a ring homomorphism of $K$ and the set of mixed spaces of $K$.

NumberField.mixedEmbedding.commMapdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the commutative map of K (from the name)

English

Let $K$ be a set. Then the commutative map of $K$ is a linear map of the set of functions from ring homomorphisms of $K$ and the set of complexes to complexes and the set of mixed spaces of $K$.

NumberField.mixedEmbedding.euclidean.integerLatticedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the integer lattice of K (from the name)

English

Let $K$ be a set. Then the integer lattice of $K$ is a submodule of $\Integer$ and the set of mixed spaces of $K$ defined as the preimage of the integer lattice of $K$ and $\operatorname{toLinearMap}$ applied to $\operatorname{toLinearEquiv}$ applied to $\operatorname{toMixed}$ applied to $K$.

NumberField.mixedEmbedding.euclidean.mixedSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, type

Wording

mixed space of K (from the name)

English

Let $K$ be a set. Then a mixed space of $K$ is an element of the function that maps $K$ to $\mathrm{WithLp}$ applied to $2$ and $\mathrm{Prod}$ applied to the set of Euclidean spaces of $\Real$ and $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ and the set of Euclidean spaces of the set of complexes and $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$.

NumberField.mixedEmbedding.euclidean.stdOrthonormalBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{stdOrthonormalBasis}$ applied to $K$ is an orthonormal basis of $\Real$ and the set of mixed spaces of $K$ defined as the product of the basis of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ and $\Real$ and the reindexing of the orthonormal basis of the function that maps $x_{1}$ to the orthonormal basis one and the sigma equivalence product of $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ and $\mathrm{Fin}$ applied to $2$.

NumberField.mixedEmbedding.euclidean.toMixeddefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{toMixed}$ applied to $K$ is a continuous linear equivalence of the set of mixed spaces of $K$ and the set of mixed spaces of $K$ defined as the continuous linear equivalence of the composition of the linear equivalence of $2$ and the product congruence of the linear equivalence of $2$ and the linear equivalence of $2$.

NumberField.mixedEmbedding.fractionalIdealLatticeBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the fractional ideal lattice basis of K and I (from the name)

English

Let $K$ be a set. Let $I$ be a unit of the set of fractional ideals of the non zero divisor of the set of rings of integer of $K$ and $K$. Then the fractional ideal lattice basis of $K$ and $I$ is a basis of $\Real$ and the set of mixed spaces of $K$.

NumberField.mixedEmbedding.idealLatticedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the ideal lattice of K and I (from the name)

English

Let $K$ be a set. Let $I$ be a unit of the set of fractional ideals of the non zero divisor of the set of rings of integer of $K$ and $K$. Then the ideal lattice of $K$ and $I$ is a submodule of $\Integer$ and the set of mixed spaces of $K$ defined as the range of the composition of the linear map of the integer algebra homomorphism of the mixed embedding of $K$ and $\operatorname{restrictScalars}$ applied to $\Integer$ and the subtype of the coercion to submodule of the underlying value in the base of $I$.

NumberField.mixedEmbedding.indexdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, type

Wording

index of K (from the name)

English

Let $K$ be a set. Then an index of $K$ is an element of the function that maps $K$ to $\mathrm{Sum}$ applied to $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ and $\mathrm{Fin}$ applied to $2$.

NumberField.mixedEmbedding.indexEquivdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the index equivalence of K (from the name)

English

Let $K$ be a set. Then the index equivalence of $K$ is an equivalence from the set of indexes of $K$ to the set of ring homomorphisms of $K$ and the set of complexes.

NumberField.mixedEmbedding.integerLatticedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the integer lattice of K (from the name)

English

Let $K$ be a set. Then the integer lattice of $K$ is a submodule of $\Integer$ and the set of mixed spaces of $K$ defined as the range of the linear map of the integer algebra homomorphism of the composition of the mixed embedding of $K$ and the algebra map of the set of rings of integer of $K$ and $K$.

NumberField.mixedEmbedding.latticeBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the lattice basis of K (from the name)

English

Let $K$ be a set. Then the lattice basis of $K$ is a basis of $\Real$ and the set of mixed spaces of $K$.

NumberField.mixedEmbedding.matrixToStdBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then there is a matrix of the set of indexes of $K$ and the set of complexes. Proof. Let $K$ be arbitrary. Let $x_{1}$ be arbitrary. By 1. By Matrix__diagonal. By 0. By 0. By 2. By Fin. Let $w_{8}$ be arbitrary. By w8. By NumberField__InfinitePlace__IsComplex. By Subtype. By Equiv__prodComm. By 2. By Fin. Let $w_{9}$ be arbitrary. By w9. By NumberField__InfinitePlace__IsComplex. By Subtype. By Equiv__prodComm. Let $x_{2}$ be arbitrary. By 2. By Inv__inv. By 1. By 1. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Complex__I. By Neg__neg. By Complex__I. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__of__app. By HSMul__hSMul. By Matrix__blockDiagonal. By Matrix__reindex__app. By Matrix__fromBlocks.

NumberField.mixedEmbedding.mixedSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, type

Wording

mixed space of K (from the name)

English

Let $K$ be a set. Then a mixed space of $K$ is an element of the function that maps $K$ to $\mathrm{Prod}$ applied to the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ to elements of $\Real$ and the set of functions from elements of $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ to complexes.

NumberField.mixedEmbedding.mixedSpaceOfRealSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the mixed space (from the name)

English

The mixed space is a continuous linear map of the set of real spaces of $K$ and the set of mixed spaces of $K$ defined as the product of the product of the function that maps $w$ to the projection of $w$ and the product of the function that maps $w_{1}$ to the composition of the complex and the projection of $w_{1}$.

NumberField.mixedEmbedding.negAtdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp (\SubtypeSet {w}{\operatorname{IsReal} (w)})$. Then $\operatorname{negAt}$ applied to $s$ is a continuous linear equivalence of the set of mixed spaces of $K$ and the set of mixed spaces of $K$ defined as the product congruence of the right product congruence of the function that maps $w$ to $\iteMACRoG {(\MembershipmemMACRoT {s}{w})}{\operatorname{neg} (\Real)}{\operatorname{refl} (\Real , \Real)}$ and the identity map of $\Real$ and the set of functions from elements of $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ to complexes.

NumberField.mixedEmbedding.normdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the norm (from the name)

English

The norm is a monoid with zero homomorphism of the set of mixed spaces of $K$ and $\Real$.

NumberField.mixedEmbedding.normAtAllPlacesdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a mixed space of $K$. Then there is a real space of $K$. Proof. Let $x_{1}$ be arbitrary. Let $w$ be arbitrary. By w. By x1. By NumberField__mixedEmbedding__normAtPlace__app.

NumberField.mixedEmbedding.normAtComplexPlacesdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the norm at complex place of x1 (from the name)

English

Let $x_{1}$ be a mixed space of $K$. Then the norm at complex place of $x_{1}$ is a real space of $K$ defined as the function that maps $w$ to $\mathrm{dite}$ applied to the proposition that $w$ is real, the function that maps $\mathrm{hw}$ to $\ProdfstMACRoZ {x_{1}}$ and the function that maps $\mathrm{hw1}$ to $\operatorname{normAtPlace}$ applied to $w$ and $x_{1}$.

NumberField.mixedEmbedding.normAtPlacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the norm at place of w (from the name)

English

Let $w$ be an infinite place of $K$. Then the norm at place of $w$ is a monoid with zero homomorphism of the set of mixed spaces of $K$ and $\Real$.

NumberField.mixedEmbedding.plusPartdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the plus part of A (from the name)

English

Let $A$ be an element of $\wp \operatorname{mixedSpace} (K)$. Then the plus part of $A$ is an element of $\wp \operatorname{mixedSpace} (K)$ defined as $\operatorname{inter}$ applied to $A$ and $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that for all elements $w$ of $\SubtypeSet {w_{1}}{\operatorname{IsReal} (w_{1})}$, $0 < \ProdfstMACRoZ {x_{1}}$.

NumberField.mixedEmbedding.realSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, type

Wording

real space of K (from the name)

English

Let $K$ be a set. Then a real space of $K$ is an element of the function that maps $K$ to the set of functions from infinite places of $K$ to real numbers.

NumberField.mixedEmbedding.signSetdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

the sign set of x1 (from the name)

English

Let $x_{1}$ be a mixed space of $K$. Then the sign set of $x_{1}$ is an element of $\wp (\SubtypeSet {w}{\operatorname{IsReal} (w)})$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to $\mathrm{Leq} (\ProdfstMACRoZ {x_{1}}, 0)$.

NumberField.mixedEmbedding.stdBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{stdBasis}$ applied to $K$ is a basis of $\Real$ and the set of mixed spaces of $K$ defined as the product of the basis function of $\Real$ and $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ and the reindexing of the basis of the function that maps $x_{1}$ to the basis one and the sigma equivalence product of $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ and $\mathrm{Fin}$ applied to $2$.

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

NumberField.mixedEmbedding.convexBodyLTdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

no wording

English

Let $K$ be a set. Let $f$ be a function from infinite places of $K$ to elements of $\mathrm{NNReal}$. Then $\operatorname{convexBodyLT}$ applied to $K$ and $f$ is an element of the power set of the set of mixed spaces of $K$ defined as $\operatorname{sprod}$ applied to the product of the universal set and the function that maps $w$ to the ball of $0$ and $\operatorname{toReal}$ applied to $f$ applied to $w$ and the product of the universal set and the function that maps $w_{1}$ to the ball of $0$ and $\operatorname{toReal}$ applied to $f$ applied to $w_{1}$.

NumberField.mixedEmbedding.convexBodyLT'defMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

no wording

English

Let $K$ be a set. Let $f$ be a function from infinite places of $K$ to elements of $\mathrm{NNReal}$. Let $x_{1}$ be an element of $\SubtypeSet {w}{\operatorname{IsComplex} (w)}$. Then $\operatorname{convexBodyLT'}$ applied to $K$, $f$ and $x_{1}$ is an element of $\wp \operatorname{mixedSpace} (K)$ defined as $\operatorname{sprod}$ applied to the product of the universal set and the function that maps $w$ to the ball of $0$ and $\operatorname{toReal}$ applied to $f$ applied to $w$ and the product of the universal set and the function that maps $w_{1}$ to $\iteMACRoG {(\EqtMACRoH {w_{1}}{x_{1}})}{\operatorname{ofPred} (\lambda x_{2} . \mathrm{and} (\mathrm{Lt} (\mathrm{abs} (\operatorname{re} (x_{2})), 1), \mathrm{Lt} (\mathrm{abs} (\operatorname{im} (x_{2})), \operatorname{toReal} (f (w_{1}))^ {2})))}{\operatorname{ball} (0 , \operatorname{toReal} (f (w_{1})))}$.

NumberField.mixedEmbedding.convexBodyLT'FactordefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{convexBodyLT'Factor}$ applied to $K$ is an element of $\mathrm{NNReal}$ defined as the product of $2 ^ {(\operatorname{nrRealPlaces} (K)+ 2)}$ and the exponentiation of the product to $\operatorname{nrComplexPlaces} (K)- 1$.

NumberField.mixedEmbedding.convexBodyLTFactordefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{convexBodyLTFactor}$ applied to $K$ is an element of $\mathrm{NNReal}$ defined as the product of $2 ^ {\operatorname{nrRealPlaces} (K)}$ and the exponentiation of the product to $\operatorname{nrComplexPlaces}$ applied to $K$.

NumberField.mixedEmbedding.convexBodySumdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

the convex body equal to the set of points of K and B (from the docstring)

English

Let $K$ be a set. Let $B$ be a real number. Then the convex body equal to the set of points of $K$ and $B$ is an element of the power set of the set of mixed spaces of $K$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that the convex body sum function of $x_{1}$ is less than or equal to $B$.

NumberField.mixedEmbedding.convexBodySumFactordefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

the convex body sum factor of K (from the name)

English

Let $K$ be a set. Then the convex body sum factor of $K$ is an element of $\mathrm{NNReal}$ defined as the quotient of the product of $2 ^ {\operatorname{nrRealPlaces} (K)}$ and the exponentiation of the quotient of the product and $2$ to $\operatorname{nrComplexPlaces}$ applied to $K$ and the factorial of the rank of $\Rational$ and $K$.

NumberField.mixedEmbedding.convexBodySumFundefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

the convex body sum function of x1 (from the name)

English

Let $x_{1}$ be a mixed space of $K$. Then the convex body sum function of $x_{1}$ is an element of $\Real$ defined as $\FinsetSum {\FinsetunivMACRoAC}{w}{(\operatorname{mult} (w)\times \operatorname{normAtPlace} (w , x_{1}))}$.

NumberField.mixedEmbedding.minkowskiBounddefMathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody, function or constant

Wording

the Minkowski bound of K and I (from the name)

English

Let $K$ be a set. Let $I$ be a unit of the set of fractional ideals of the non zero divisor of the set of rings of integer of $K$ and $K$. Then the Minkowski bound of $K$ and $I$ is an element of $\mathrm{ENNReal}$ defined as the product of $\operatorname{volume}$ applied to the fundamental domain of the fractional ideal lattice basis of $K$ and $I$ and the exponentiation of $2$ to the rank of $\Real$ and the set of mixed spaces of $K$.

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

NumberField.mixedEmbedding.fundamentalConedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the fundamental cone of K (from the docstring)

English

Let $K$ be a set. Then the fundamental cone of $K$ is an element of the power set of the set of mixed spaces of $K$ defined as $\operatorname{sdiff}$ applied to the preimage of $\operatorname{logMap}$ and the fundamental domain of the basis of the unit lattice of $K$ and the basis unit lattice of $K$ and $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\mathrm{Eq} (\operatorname{norm} (x_{1}), 0)$.

NumberField.mixedEmbedding.fundamentalCone.idealSetdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the ideal set of K and J (from the name)

English

Let $K$ be a set. Let $J$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (\operatorname{RingOfIntegers} (K)))}{x_{1}})}$. Then the ideal set of $K$ and $J$ is an element of $\wp \operatorname{mixedSpace} (K)$ defined as $\operatorname{inter}$ applied to the fundamental cone of $K$ and the ideal lattice of $K$ and $\operatorname{mk0}$ applied to $K$ and $J$.

NumberField.mixedEmbedding.fundamentalCone.idealSetEquivdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the ideal set equivalence of K and J (from the name)

English

Let $K$ be a set. Let $J$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (\operatorname{RingOfIntegers} (K)))}{x_{1}})}$. Then the ideal set equivalence of $K$ and $J$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{idealSet} (K , J))}{\operatorname{Elem} (\operatorname{ofPred} (\lambda a . \MembershipmemMACRoT {J}{\operatorname{preimageOfMemIntegerSet} (a)}))}$.

NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNormdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the ideal set equivalence norm of J and n (from the name)

English

Let $K$ be a set. Let $J$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (\operatorname{RingOfIntegers} (K)))}{x_{2}})}$. Let $n$ be an element of $\Natural$. Then the ideal set equivalence norm of $J$ and $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {a}{\mathrm{Eq} (\operatorname{norm} (a), n)})}{\mathrm{Prod} (\SubtypeSet {I}{\mathrm{and} (\divides {J}{I}, \mathrm{and} (\operatorname{IsPrincipal} (I), \mathrm{Eq} (\operatorname{absNorm} (I), n)))}, \SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})})}$.

NumberField.mixedEmbedding.fundamentalCone.idealSetMapdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the ideal set map of J and x1 (from the name)

English

Let $K$ be a set. Let $J$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (\operatorname{RingOfIntegers} (K)))}{x_{2}})}$. Let $x_{1}$ be an element of the ideal set of $K$ and $J$. Then the ideal set map of $J$ and $x_{1}$ is an element of the integer set of $K$.

NumberField.mixedEmbedding.fundamentalCone.intNormdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the integer norm of a (from the name)

English

Let $a$ be an element of the integer set of $K$. Then the integer norm of $a$ is a natural number defined as the absolute value of $\operatorname{norm}$ applied to $\Integer$ and the preimage of $a$.

NumberField.mixedEmbedding.fundamentalCone.integerSetdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the integer set of K (from the name)

English

Let $K$ be a set. Then the integer set of $K$ is an element of the power set of the set of mixed spaces of $K$ defined as $\operatorname{inter}$ applied to the fundamental cone of $K$ and the integer lattice of $K$.

NumberField.mixedEmbedding.fundamentalCone.integerSetEquivdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the integer set equivalence of K (from the name)

English

Let $K$ be a set. Then the integer set equivalence of $K$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{integerSet} (K))}{\mathrm{Prod} (\SubtypeSet {I}{\operatorname{IsPrincipal} (I)}, \SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})})}$.

NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNormdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the integer set equivalence norm of K and n (from the name)

English

Let $K$ be a set. Let $n$ be an element of $\Natural$. Then the integer set equivalence norm of $K$ and $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {a}{\mathrm{Eq} (\operatorname{norm} (a), n)})}{\mathrm{Prod} (\SubtypeSet {I}{\mathrm{and} (\operatorname{IsPrincipal} (I), \mathrm{Eq} (\operatorname{absNorm} (I), n))}, \SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})})}$.

NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociatesdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the integer set quotient equivalence associate of K (from the name)

English

Let $K$ be a set. Then the integer set quotient equivalence associate of $K$ is an element of $\EquivMACRoAE {\mathrm{Quotient} (\operatorname{orbitRel} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})}, \operatorname{Elem} (\operatorname{integerSet} (K))))}{\mathrm{Associates} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\operatorname{RingOfIntegers} (K))}{x_{2}})})}$.

NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociatesdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the integer set to associate of K and a (from the name)

English

Let $K$ be a set. Let $a$ be an element of the integer set of $K$. Then the integer set to associate of $K$ and $a$ is an associate of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\operatorname{RingOfIntegers} (K))}{x_{1}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\operatorname{RingOfIntegers} (K))}{x_{1}})}$ and the preimage of $a$.

NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSetdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the preimage of a (from the name)

English

Let $a$ be an element of the integer set of $K$. Then the preimage of $a$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\operatorname{RingOfIntegers} (K))}{x_{1}})}$.

NumberField.mixedEmbedding.fundamentalCone.quotIntNormdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the quotient integer norm of x1 (from the name)

English

Let $x_{1}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{2}})}$ and the set of elements of the integer set of $K$. Then the quotient integer norm of $x_{1}$ is an element of $\Natural$.

NumberField.mixedEmbedding.logMapdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone, function or constant

Wording

the map from the mixed space to x1 (from the docstring)

English

Let $x_{1}$ be a mixed space of $K$. Then the map from the mixed space to $x_{1}$ is a logarithm space of $K$ defined as the function that maps $w$ to the product of the multiplicity of $w$ and the difference between the logarithm of $\operatorname{normAtPlace}$ applied to $w$ and $x_{1}$ and the product of the logarithm of $\operatorname{norm}$ applied to $x_{1}$ and $\operatorname{inv}$ applied to the rank of $\Rational$ and $K$.

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

NumberField.mixedEmbedding.fundamentalCone.compactSetdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the compact set of K (from the name)

English

Let $K$ be a set. Then the compact set of $K$ is an element of $\wp \operatorname{realSpace} (K)$ defined as $\HSMulhSMulMACRoAL {(\SetIccMACRoP {0}{1})}{\operatorname{image} (\operatorname{toFun'} (\operatorname{expMapBasis}), \operatorname{pi} (\operatorname{univ} , \lambda w . \iteMACRoG {(\EqtMACRoH {w}{\mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_}})}{\operatorname{singleton} (0)}{(\SetIccMACRoP {0}{1})}))}$.

NumberField.mixedEmbedding.fundamentalCone.completeBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the complete basis of K (from the name)

English

Let $K$ be a set. Then the complete basis of $K$ is a basis of $\Real$ and the set of real spaces of $K$.

NumberField.mixedEmbedding.fundamentalCone.completeFamilydefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the complete family of K and x1 (from the name)

English

Let $K$ be a set. Let $x_{1}$ be an infinite place of $K$. Then the complete family of $K$ and $x_{1}$ is a real space of $K$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {x_{1}}{\mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_}}$, the function that maps $\mathrm{hi}$ and $w$ to the multiplicity of $w$ and the function that maps $\mathrm{hi1}$ to the function of the inverse of the exponential map and $\operatorname{normAtAllPlaces}$ applied to $\operatorname{mixedEmbedding}$ applied to $K$ and $\operatorname{algebraMap}$ applied to the set of rings of integer of $K$, $K$ and the underlying value in the base of $\operatorname{fundSystem}$ applied to $K$ and $\operatorname{symm}$ applied to the equivalence finite rank and $x_{1}$.

NumberField.mixedEmbedding.fundamentalCone.deriv_expMap_singledefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

no wording

English

Let $w$ be an infinite place of $K$. Let $x_{1}$ be a real number. Then $\mathrm{NumberField\_\_mixedEmbedding\_\_fundamentalCone\_\_deriv\_expMap\_single}$ applied to $w$ and $x_{1}$ is a real number defined as the product of the function of $\mathrm{NumberField\_\_mixedEmbedding\_\_fundamentalCone\_\_expMap\_single}$ applied to $w$ and $x_{1}$ and $\operatorname{inv}$ applied to the multiplicity of $w$.

NumberField.mixedEmbedding.fundamentalCone.equivFinRankdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the equivalence finite rank (from the name)

English

The equivalence finite rank is an equivalence from $\mathrm{Fin}$ applied to the rank of $K$ to $\SubtypeSet {w}{\mathrm{Neq} (w , \mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_})}$.

NumberField.mixedEmbedding.fundamentalCone.expMapdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the exponential map (from the name)

English

The exponential map is an open partial homeomorphism of the set of real spaces of $K$ and the set of real spaces of $K$ defined as the product of the function that maps $w$ to $\mathrm{NumberField\_\_mixedEmbedding\_\_fundamentalCone\_\_expMap\_single}$ applied to $w$.

NumberField.mixedEmbedding.fundamentalCone.expMapBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the exponential map basis (from the name)

English

The exponential map basis is an open partial homeomorphism of the set of real spaces of $K$ and the set of real spaces of $K$ defined as the composition open partial homeomorphism of the homeomorphism of the inverse of the equivalence function of the complete basis of $K$ and the exponential map.

NumberField.mixedEmbedding.fundamentalCone.expMap_singledefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

no wording

English

Let $w$ be an infinite place of $K$. Then $\mathrm{NumberField\_\_mixedEmbedding\_\_fundamentalCone\_\_expMap\_single}$ applied to $w$ is an open partial homeomorphism of $\Real$ and $\Real$.

NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the derivative exponential map of x1 (from the name)

English

Let $x_{1}$ be a real space of $K$. Then the derivative exponential map of $x_{1}$ is a continuous linear map of the set of real spaces of $K$ and the set of real spaces of $K$ defined as the product of the function that maps $w$ to the composition of the right scalar multiple of $1$ and $\mathrm{NumberField\_\_mixedEmbedding\_\_fundamentalCone\_\_deriv\_expMap\_single}$ applied to $w$ and $x_{1}$ applied to $w$ and the projection of $w$.

NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasisdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

the derivative exponential map basis of K and x1 (from the name)

English

Let $K$ be a set. Let $x_{1}$ be a real space of $K$. Then the derivative exponential map basis of $K$ and $x_{1}$ is a continuous linear map of the set of real spaces of $K$ and the set of real spaces of $K$ defined as the composition of the derivative exponential map of $\operatorname{symm}$ applied to the equivalence function of the complete basis of $K$ and $x_{1}$ and the continuous linear map of the inverse of the equivalence function of the complete basis of $K$.

NumberField.mixedEmbedding.fundamentalCone.normLeOnedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{normLeOne}$ applied to $K$ is an element of the power set of the set of mixed spaces of $K$ defined as $\operatorname{inter}$ applied to the fundamental cone of $K$ and $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\mathrm{Leq} (\operatorname{norm} (x_{1}), 1)$.

NumberField.mixedEmbedding.fundamentalCone.paramSetdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{paramSet}$ applied to $K$ is an element of the power set of the set of real spaces of $K$ defined as the product of the universal set and the function that maps $w$ to $\iteMACRoG {(\EqtMACRoH {w}{\mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_}})}{\operatorname{Iic} (0)}{\operatorname{Ico} (0 , 1)}$.

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

NumberField.mixedEmbedding.FDerivPolarCoordRealSymmdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the derivative polar coordinate real inverse of K and x1 (from the name)

English

Let $K$ be a set. Let $x_{1}$ be a real mixed space of $K$. Then the derivative polar coordinate real inverse of $K$ and $x_{1}$ is a continuous linear map of the set of real mixed spaces of $K$ and the set of real mixed spaces of $K$ defined as the product of the first component of the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ to elements of $\Real$ and the set of functions from elements of $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ to elements of $\mathrm{Prod}$ applied to $\Real$ and $\Real$ and the composition of the derivative of $\ProdsndMACRoAA {x_{1}}$ and the second component of the set of functions from elements of $\SubtypeSet {w_{2}}{\operatorname{IsReal} (w_{2})}$ to elements of $\Real$ and the set of functions from elements of $\SubtypeSet {w_{3}}{\operatorname{IsComplex} (w_{3})}$ to elements of $\mathrm{Prod}$ applied to $\Real$ and $\Real$.

NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the homeomorphism real mixed space polar space of K (from the name)

English

Let $K$ be a set. Then the homeomorphism real mixed space polar space of $K$ is a homeomorphism of the set of real mixed spaces of $K$ and the set of polar spaces of $K$.

NumberField.mixedEmbedding.measurableEquivRealMixedSpacePolarSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the measurable equivalence real mixed space polar space of K (from the name)

English

Let $K$ be a set. Then the measurable equivalence real mixed space polar space of $K$ is a measurable equivalence of the set of real mixed spaces of $K$ and the set of polar spaces of $K$.

NumberField.mixedEmbedding.mixedSpaceToRealMixedSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the natural homeomorphism between the mixed space of K (from the docstring)

English

Let $K$ be a set. Then the natural homeomorphism between the mixed space of $K$ is a homeomorphism of the set of mixed spaces of $K$ and the set of real mixed spaces of $K$ defined as the product congruence of the identity of the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ to elements of $\Real$ and the right product congruence of the function that maps $x_{2}$ to the homeomorphism of the equivalence real product continuous linear map.

NumberField.mixedEmbedding.polarCoorddefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the polar coordinate open partial homeomorphism between the mixed space of K (from the docstring)

English

Let $K$ be a set. Then the polar coordinate open partial homeomorphism between the mixed space of $K$ is an open partial homeomorphism of the set of mixed spaces of $K$ and the set of real mixed spaces of $K$ defined as the product of the identity on the whole space of the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ to elements of $\Real$ and the product of the function that maps $x_{2}$ to the polar coordinate.

NumberField.mixedEmbedding.polarCoordRealdefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the polar coordinate open partial homeomorphism of K (from the docstring)

English

Let $K$ be a set. Then the polar coordinate open partial homeomorphism of $K$ is an open partial homeomorphism of the set of real mixed spaces of $K$ and the set of real mixed spaces of $K$ defined as the product of the identity on the whole space of the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ to elements of $\Real$ and the product of the function that maps $x_{2}$ to the polar coordinate.

NumberField.mixedEmbedding.polarSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, type

Wording

polar space of K (from the name)

English

Let $K$ be a set. Then a polar space of $K$ is an element of the function that maps $K$ to $\mathrm{Prod}$ applied to the set of functions from infinite places of $K$ to elements of $\Real$ and the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsComplex} (w)}$ to elements of $\Real$.

NumberField.mixedEmbedding.polarSpaceCoorddefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, function or constant

Wording

the polar coordinate open partial homeomorphism between the mixed space of K (from the docstring)

English

Let $K$ be a set. Then the polar coordinate open partial homeomorphism between the mixed space of $K$ is an open partial homeomorphism of the set of mixed spaces of $K$ and the set of polar spaces of $K$ defined as the composition homeomorphism of the polar coordinate open partial homeomorphism between the mixed space of $K$ and the homeomorphism real mixed space polar space of $K$.

NumberField.mixedEmbedding.realMixedSpacedefMathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord, type

Wording

real mixed space of K (from the name)

English

Let $K$ be a set. Then a real mixed space of $K$ is an element of the function that maps $K$ to $\mathrm{Prod}$ applied to the set of functions from elements of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$ to elements of $\Real$ and the set of functions from elements of $\SubtypeSet {w_{1}}{\operatorname{IsComplex} (w_{1})}$ to elements of $\mathrm{Prod}$ applied to $\Real$ and $\Real$.

Mathlib.NumberTheory.NumberField.ClassNumber

NumberField.classNumberdefMathlib.NumberTheory.NumberField.ClassNumber, function or constant

Wording

the class number of K (from the docstring)

English

Let $K$ be a set. Then the class number of $K$ is a natural number defined as the cardinality of the set of ideal class groups of the set of rings of integer of $K$.

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

NumberField.FinitePlacedefMathlib.NumberTheory.NumberField.Completion.FinitePlace, type

Wording

finite place of K (from the name)

English

Let $K$ be a set. Then a finite place of $K$ is an element of the function that maps $K$ to $\SubtypeSet {w}{\mathrm{exists} (\operatorname{HeightOneSpectrum} (\operatorname{RingOfIntegers} (K)), \lambda v . \EqtMACRoH {\operatorname{place} (\operatorname{embedding} (v))}{w})}$.

NumberField.FinitePlace.embeddingdefMathlib.NumberTheory.NumberField.Completion.FinitePlace, function or constant

Wording

the embedding of v (from the docstring)

English

Let $v$ be a height one spectrum of $R$. Then the embedding of $v$ is a ring homomorphism of $K$ and the set of adic completions of $K$ and $v$ defined as the composition of the ring homomorphism of the inverse of the equivalence of $K$ and $v$ and the composition of the coercion ring homomorphism and the ring homomorphism of the inverse of the equivalence of the valuation of $K$ and $v$.

NumberField.FinitePlace.equivHeightOneSpectrumdefMathlib.NumberTheory.NumberField.Completion.FinitePlace, function or constant

Wording

the equivalence height one spectrum (from the name)

English

The equivalence height one spectrum is an equivalence from the set of finite places of $K$ to the set of height one spectra of the set of rings of integer of $K$ defined as $\operatorname{mk}$ applied to $\operatorname{maximalIdeal}$, $\operatorname{mk}$, $\mathrm{NumberField\_\_FinitePlace\_\_mk\_maximalIdeal}$ and $\mathrm{NumberField\_\_FinitePlace\_\_maximalIdeal\_mk}$.

NumberField.FinitePlace.maximalIdealdefMathlib.NumberTheory.NumberField.Completion.FinitePlace, function or constant

Wording

the maximal ideal of w (from the name)

English

Let $w$ be a finite place of $K$. Then the maximal ideal of $w$ is a height one spectrum of the set of rings of integer of $K$.

NumberField.FinitePlace.mkdefMathlib.NumberTheory.NumberField.Completion.FinitePlace, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of the set of rings of integer of $K$. Then $\operatorname{mk}$ applied to $v$ is a finite place of $K$ defined as the place of the embedding of $v$.

NumberField.HeightOneSpectrum.adicAbvdefMathlib.NumberTheory.NumberField.Completion.FinitePlace, function or constant

Wording

no wording

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then $\operatorname{adicAbv}$ applied to $K$ and $v$ is an absolute value of $K$ and $\Real$ defined as $\operatorname{adicAbv}$ applied to $v$ and $\mathrm{NumberField\_\_HeightOneSpectrum\_\_one\_lt\_absNorm\_nnreal}$ applied to $v$.

NumberField.IsFinitePlacedefMathlib.NumberTheory.NumberField.Completion.FinitePlace, predicate

Wording

w is a finite place (from the name)

English

Let $w$ be an absolute value of $K$ and $\Real$. Then $w$ is a finite place, if there exists a height one spectrum $v$ of the set of rings of integer of $K$, such that the place of the embedding of $v$ is equal to $w$.

Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

NumberField.InfinitePlace.CompletionstructureMathlib.NumberTheory.NumberField.Completion.InfinitePlace, type

Wording

completion of v (from the name)

English

Let $v$ be an infinite place of $K$. Then the completions of $v$ are a basic type.

NumberField.InfinitePlace.Completion.equivdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the equivalence of v (from the name)

English

Let $v$ be an infinite place of $K$. Then the equivalence of $v$ is a ring isomorphism of the set of completions of $v$ and the set of completions of $v$.

NumberField.InfinitePlace.Completion.equivCompletiondefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the equivalence completion of v (from the name)

English

Let $v$ be an infinite place of $K$. Then the equivalence completion of $v$ is an equivalence from the set of completions of $v$ to the set of completions of $v$.

NumberField.InfinitePlace.Completion.extensionEmbeddingdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the extension embedding of v (from the name)

English

Let $v$ be an infinite place of $K$. Then the extension embedding of $v$ is a ring homomorphism of the set of completions of $v$ and the set of complexes.

NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsRealdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the embedding of hv (from the docstring)

English

Assume that $v$ is real. Then the embedding of $\mathrm{hv}$ is a ring homomorphism of the set of completions of $v$ and $\Real$.

NumberField.InfinitePlace.Completion.isometryEquivCompletiondefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the isometry equivalence completion of v (from the name)

English

Let $v$ be an infinite place of $K$. Then the isometry equivalence completion of $v$ is an isometry equivalence of the set of completions of $v$ and the set of completions of $v$ defined as $\operatorname{mk}$ applied to the equivalence completion of $v$ and $\mathrm{NumberField\_\_InfinitePlace\_\_Completion\_\_isometry\_toCompletion}$ applied to $v$.

NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplexdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the isometry equivalence complex of hv (from the name)

English

Assume that $v$ is complex. Then the isometry equivalence complex of $\mathrm{hv}$ is an isometry equivalence of the set of completions of $v$ and the set of complexes defined as $\operatorname{mk}$ applied to the equivalence of the ring isomorphism of $\mathrm{hv}$ and $\mathrm{NumberField\_\_InfinitePlace\_\_Completion\_\_isometry\_extensionEmbedding}$ applied to $v$.

NumberField.InfinitePlace.Completion.isometryEquivRealOfIsRealdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

no wording

English

Assume that $v$ is real. Then $\operatorname{isometryEquivRealOfIsReal}$ applied to $\mathrm{hv}$ is an isometry equivalence of the set of completions of $v$ and $\Real$ defined as $\operatorname{mk}$ applied to the equivalence of the ring isomorphism of $\mathrm{hv}$ and $\mathrm{NumberField\_\_InfinitePlace\_\_Completion\_\_isometry\_extensionEmbeddingOfIsReal}$ applied to $\mathrm{hv}$.

NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplexdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the ring isomorphism of hv (from the docstring)

English

Assume that $v$ is complex. Then the ring isomorphism of $\mathrm{hv}$ is a ring isomorphism of the set of completions of $v$ and the set of complexes defined as the ring isomorphism of the extension embedding of $v$ and $\mathrm{NumberField\_\_InfinitePlace\_\_Completion\_\_bijective\_extensionEmbedding\_of\_isComplex}$ applied to $\mathrm{hv}$.

NumberField.InfinitePlace.Completion.ringEquivRealOfIsRealdefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the ring isomorphism of hv (from the docstring)

English

Assume that $v$ is real. Then the ring isomorphism of $\mathrm{hv}$ is a ring isomorphism of the set of completions of $v$ and $\Real$ defined as the ring isomorphism of the embedding of $\mathrm{hv}$ and $\mathrm{NumberField\_\_InfinitePlace\_\_Completion\_\_bijective\_extensionEmbeddingOfIsReal}$ applied to $\mathrm{hv}$.

NumberField.InfinitePlace.Completion.toCompletiondefMathlib.NumberTheory.NumberField.Completion.InfinitePlace, function or constant

Wording

the completion of self (from the name)

English

Let $\mathrm{self}$ be a completion of $v$. Then the completion of $\mathrm{self}$ is a completion of $v$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

NumberField.LiesOver.completionMapdefMathlib.NumberTheory.NumberField.Completion.LiesOverInstances, function or constant

Wording

the completion map of v and w (from the name)

English

Let $v$ be an infinite place of $K$. Let $w$ be an infinite place of $L$. Then the completion map of $v$ and $w$ is a ring homomorphism of the set of completions of $v$ and the set of completions of $w$.

Mathlib.NumberTheory.NumberField.Completion.Ramification

NumberField.InfinitePlace.inertiaDegdefMathlib.NumberTheory.NumberField.Completion.Ramification, function or constant

Wording

the inertia degree of w over v (from the docstring)

English

Let $v$ be an infinite place of $K$. Let $w$ be an infinite place of $L$. Then the inertia degree of $w$ over $v$ is a natural number defined as $\mathrm{dite}$ applied to $\operatorname{LiesOver}$ applied to $w$ and $v$, the function that maps $h$ to the inertia degree of the bottom and the set of completions of $v$ and the function that maps $h_{1}$ to $0$.

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

IsPrimitiveRoot.adjoinEquivRingOfIntegersdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $n$. Then $\operatorname{adjoinEquivRingOfIntegers}$ applied to $h_{3}$ is an algebra isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\Integer , \operatorname{singleton} (x_{1}))}{x_{2}})}$ and the set of rings of integer of $K$ defined as the equivalence of $K$ and the set of rings of integer of $K$.

IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePowdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $p ^ {k}$. Then $\operatorname{adjoinEquivRingOfIntegersOfPrimePow}$ applied to $h_{2}$ is an algebra isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\Integer , \operatorname{singleton} (x_{1}))}{x_{2}})}$ and the set of rings of integer of $K$ defined as the equivalence of $K$ and the set of rings of integer of $K$.

IsPrimitiveRoot.integralPowerBasisdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

the integral of h3 (from the docstring)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $n$. Then the integral of $h_{3}$ is a power basis of $\Integer$ and the set of rings of integer of $K$.

IsPrimitiveRoot.integralPowerBasisOfPrimePowdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

the integral of h2 (from the docstring)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $p ^ {k}$. Then the integral of $h_{2}$ is a power basis of $\Integer$ and the set of rings of integer of $K$.

IsPrimitiveRoot.subOneIntegralPowerBasisdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

the integral of h3 (from the docstring)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $n$. Then the integral of $h_{3}$ is a power basis of $\Integer$ and the set of rings of integer of $K$.

IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePowdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

the integral of h2 (from the docstring)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $p ^ {k}$. Then the integral of $h_{2}$ is a power basis of $\Integer$ and the set of rings of integer of $K$.

IsPrimitiveRoot.toIntegerdefMathlib.NumberTheory.NumberField.Cyclotomic.Basic, function or constant

Wording

the integer of h1 (from the name)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $k$. Then the integer of $h_{1}$ is a ring of integer of $K$ defined as $x_{1}$.

Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

IsCyclotomicExtension.Rat.galEquivZModdefMathlib.NumberTheory.NumberField.Cyclotomic.Galois, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $K$ be a set. Then $\operatorname{galEquivZMod}$ applied to $n$ and $K$ is a multiplicative equivalence of the set of algebra isomorphisms of $K$ and $K$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$.

IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChardefMathlib.NumberTheory.NumberField.Cyclotomic.Galois, function or constant

Wording

the bijection between the intermediate fields of n (from the docstring)

English

Let $n$ be a natural number. Let $K$ and $R$ be sets. Then the bijection between the intermediate fields of $n$ is an order isomorphism of the set of intermediate fields of $\Rational$ and $K$ and the set of subgroups of the set of Dirichlet characters of $R$ and $n$ defined as the composition of the intermediate field equivalence subgroup and the composition of the dual of the bijection between the subgroups of $n$ and the inverse of the dual dual of the set of subgroups of the set of Dirichlet characters of $R$ and $n$.

IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChardefMathlib.NumberTheory.NumberField.Cyclotomic.Galois, function or constant

Wording

the bijection between the subgroups of n (from the docstring)

English

Let $n$ be a natural number. Let $K$ and $R$ be sets. Then the bijection between the subgroups of $n$ is an order isomorphism of the set of subgroups of the set of algebra isomorphisms of $K$ and $K$ and the set of order duals of the set of subgroups of the set of Dirichlet characters of $R$ and $n$ defined as the composition of the map subgroup of $\operatorname{galEquivZMod}$ applied to $n$ and $K$ and the subgroup order isomorphism subgroup multiplicative characteristic of $\mathrm{ZMod}$ applied to $n$ and $R$.

Mathlib.NumberTheory.NumberField.DedekindZeta

NumberField.dedekindZetadefMathlib.NumberTheory.NumberField.DedekindZeta, function or constant

Wording

the Dedekind zeta function of K and s (from the docstring)

English

Let $K$ be a set. Let $s$ be a complex. Then the Dedekind zeta function of $K$ and $s$ is a complex defined as the series of the function that maps $n$ to the cardinality of $\SubtypeSet {I}{\mathrm{Eq} (\operatorname{absNorm} (I), n)}$ and $s$.

NumberField.dedekindZeta_residuedefMathlib.NumberTheory.NumberField.DedekindZeta, function or constant

Wording

the value of the residue at K (from the docstring)

English

Let $K$ be a set. Then the value of the residue at $K$ is a real number defined as the quotient of the product of $2 ^ {\operatorname{nrRealPlaces} (K)}$, the exponentiation of the product of $2$ and the product to $\operatorname{nrComplexPlaces}$ applied to $K$, the regulator of $K$ and the class number of $K$ and the product of the order of the torsion subgroup of $K$ and the square root of the absolute value of the absolute discriminant of $K$.

Mathlib.NumberTheory.NumberField.DirichletDensity

NumberField.Set.HasDirichletDensitydefMathlib.NumberTheory.NumberField.DirichletDensity, predicate

Wording

no wording

English

Let $S$ be an element of the power set of the set of height one spectra of the set of rings of integer of $K$. Let $x_{1}$ be a real number. Then $\operatorname{HasDirichletDensity}$ holds for $S$ and $x_{1}$, if $\operatorname{Tendsto}$ holds for the function that maps $s$ to the quotient of the prime ideal Zeta sum of $S$ and $s$ and the prime ideal Zeta sum of the universal set and $s$, $\mathrm{nhdsWithin}$ applied to $1$ and $\operatorname{Ioi}$ applied to $1$ and the neighbourhood filter of $x_{1}$.

NumberField.Set.dirichletDensitydefMathlib.NumberTheory.NumberField.DirichletDensity, function or constant

Wording

the Dirichlet density of S (from the docstring)

English

Let $S$ be an element of the power set of the set of height one spectra of the set of rings of integer of $K$. Then the Dirichlet density of $S$ is a real number defined as $\mathrm{dite}$ applied to the proposition that there exists a real number $x_{1}$, such that $\operatorname{HasDirichletDensity}$ holds for $S$ and $x_{1}$, the function that maps $h_{1}$ to $\operatorname{choose}$ applied to $h_{1}$ and the function that maps $h_{2}$ to $0$.

NumberField.Set.primeIdealZetaSumdefMathlib.NumberTheory.NumberField.DirichletDensity, function or constant

Wording

the prime ideal Zeta sum of S and s (from the name)

English

Let $S$ be an element of the power set of the set of height one spectra of the set of rings of integer of $K$. Let $s$ be a real number. Then the prime ideal Zeta sum of $S$ and $s$ is a real number defined as the sum of the function that maps $x_{1}$ to $\operatorname{absNorm} (\operatorname{asIdeal} (x_{1}))^ {\operatorname{neg} (s)}$ and $\operatorname{unconditional}$ applied to the set of elements of $S$.

Mathlib.NumberTheory.NumberField.Discriminant.Basic

NumberField.hermiteTheorem.boundOfDiscBdddefMathlib.NumberTheory.NumberField.Discriminant.Basic, function or constant

Wording

the bound of N (from the name)

English

Let $N$ be a natural number. Then the bound of $N$ is an element of $\mathrm{NNReal}$ defined as the sum of the product of $\operatorname{sqrt}$ applied to $N$ and the exponentiation of $2$ to the rank of $N$ and $1$.

NumberField.hermiteTheorem.rankOfDiscrBdddefMathlib.NumberTheory.NumberField.Discriminant.Basic, function or constant

Wording

the rank of N (from the name)

English

Let $N$ be a natural number. Then the rank of $N$ is a natural number defined as the maximum of $1$ and the floor of the quotient of the logarithm of $\frac{ 9}{4}\times N$ and the logarithm of the quotient of the product of $3$ and the product and $4$.

NumberField.rootDiscrdefMathlib.NumberTheory.NumberField.Discriminant.Basic, function or constant

Wording

the root discriminant of K (from the docstring)

English

Let $K$ be a set. Then the root discriminant of $K$ is a real number defined as the exponentiation of the absolute value of the absolute discriminant of $K$ to $\operatorname{inv}$ applied to the rank of $\Rational$ and $K$.

Mathlib.NumberTheory.NumberField.Discriminant.Defs

NumberField.discrdefMathlib.NumberTheory.NumberField.Discriminant.Defs, function or constant

Wording

the absolute discriminant of K (from the docstring)

English

Let $K$ be a set. Then the absolute discriminant of $K$ is an integer defined as $\operatorname{discr}$ applied to $\Integer$ and $\operatorname{coe}$ applied to the basis of $K$.

Mathlib.NumberTheory.NumberField.EquivReindex

NumberField.basisMatrixdefMathlib.NumberTheory.NumberField.EquivReindex, function or constant

Wording

the basis matrix of K (from the name)

English

Let $K$ be a set. Then the basis matrix of $K$ is a matrix of the set of ring homomorphisms of $K$ and the set of complexes and the set of complexes defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ to $\operatorname{latticeBasis}$ applied to $K$ and $\operatorname{equivReindex}$ applied to $K$ and $i_{1}$.

NumberField.equivReindexdefMathlib.NumberTheory.NumberField.EquivReindex, function or constant

Wording

the equivalence reindexing of K (from the name)

English

Let $K$ be a set. Then the equivalence reindexing of $K$ is an equivalence from the set of ring homomorphisms of $K$ and the set of complexes to $\operatorname{ChooseBasisIndex}$ applied to $\Integer$ and the set of rings of integer of $K$.

Mathlib.NumberTheory.NumberField.FractionalIdeal

NumberField.basisOfFractionalIdealdefMathlib.NumberTheory.NumberField.FractionalIdeal, function or constant

Wording

the basis of K and I (from the name)

English

Let $K$ be a set. Let $I$ be a unit of the set of fractional ideals of the non zero divisor of the set of rings of integer of $K$ and $K$. Then the basis of $K$ and $I$ is a basis of $\Rational$ and $K$ defined as the basis of $\operatorname{restrictScalars}$ applied to $\Integer$ and the subtype of the coercion to submodule of the underlying value in the base of $I$ and the fractional ideal basis of $K$ and the underlying value in the base of $I$.

NumberField.fractionalIdealBasisdefMathlib.NumberTheory.NumberField.FractionalIdeal, function or constant

Wording

the fractional ideal basis of K and I (from the name)

English

Let $K$ be a set. Let $I$ be a fractional ideal of the non zero divisor of the set of rings of integer of $K$ and $K$. Then the fractional ideal basis of $K$ and $I$ is a basis of $\Integer$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (I)}{x_{2}})}$ defined as $\operatorname{chooseBasis}$ applied to $\Integer$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (I)}{x_{1}})}$.

Mathlib.NumberTheory.NumberField.House

NumberField.housedefMathlib.NumberTheory.NumberField.House, function or constant

Wording

the house of x1 (from the docstring)

English

Let $x_{1}$ be an element of $K$. Then the house of $x_{1}$ is a real number defined as the norm of $\operatorname{canonicalEmbedding}$ applied to $K$ and $x_{1}$.

Mathlib.NumberTheory.NumberField.Ideal.Basic

Ideal.rootsOfUnityMapQuotdefMathlib.NumberTheory.NumberField.Ideal.Basic, function or constant

Wording

the root of I and n (from the name)

English

Let $I$ be an ideal of the set of rings of integer of $K$. Let $n$ be an element of $\Natural$. Then the root of $I$ and $n$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , \operatorname{RingOfIntegers} (K))}{x_{1}})}$ and $\UnitsMACRoAO {\operatorname{Quotient} (\operatorname{RingOfIntegers} (K), I)}$ defined as $\operatorname{domRestrict}$ applied to the map of $\operatorname{toMonoidHom}$ applied to $\operatorname{mk}$ applied to $I$ and the root of $n$ and the set of rings of integer of $K$.

Ideal.torsionMapQuotdefMathlib.NumberTheory.NumberField.Ideal.Basic, function or constant

Wording

the torsion map quotient of I (from the name)

English

Let $I$ be an ideal of the set of rings of integer of $K$. Then the torsion map quotient of $I$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})}$ and $\UnitsMACRoAO {\operatorname{Quotient} (\operatorname{RingOfIntegers} (K), I)}$ defined as $\operatorname{domRestrict}$ applied to the map of $\operatorname{toMonoidHom}$ applied to $\operatorname{mk}$ applied to $I$ and the torsion of $K$.

Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

NumberField.Ideal.primesOverSpanEquivMonicFactorsModdefMathlib.NumberTheory.NumberField.Ideal.KummerDedekind, function or constant

Wording

no wording

English

Assume that $p$ does not divide the exponent of $x_{1}$. Then $\operatorname{primesOverSpanEquivMonicFactorsMod}$ applied to $\mathrm{hp}$ is an equivalence from the set of elements of $\operatorname{primesOver}$ applied to the span of $\operatorname{singleton}$ applied to $p$ and the set of rings of integer of $K$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{monicFactorsMod} (x_{1} , p)}{x_{2}})}$.

RingOfIntegers.ZModXQuotSpanEquivQuotSpandefMathlib.NumberTheory.NumberField.Ideal.KummerDedekind, function or constant

Wording

no wording

English

Assume that $p$ does not divide the exponent of $x_{1}$. Then $\operatorname{ZModXQuotSpanEquivQuotSpan}$ applied to $\mathrm{hp}$ is a ring isomorphism of the set of quotients of the set of polynomials of $\mathrm{ZMod}$ applied to $p$ and the span of $\operatorname{singleton}$ applied to the map of the cast ring homomorphism of $\mathrm{ZMod}$ applied to $p$ and the minimal polynomial of $\Integer$ and $x_{1}$ and the set of quotients of the set of rings of integer of $K$ and the span of $\operatorname{singleton}$ applied to $p$.

RingOfIntegers.ZModXQuotSpanEquivQuotSpanPairdefMathlib.NumberTheory.NumberField.Ideal.KummerDedekind, function or constant

Wording

no wording

English

Assume that $p$ does not divide the exponent of $x_{1}$. Assume that the map of the cast ring homomorphism of $\mathrm{ZMod}$ applied to $p$ and $Q$ is an element of $\operatorname{monicFactorsMod}$ applied to $x_{1}$ and $p$. Then $\operatorname{ZModXQuotSpanEquivQuotSpanPair}$ applied to $\mathrm{hp}$ and $\mathrm{hQ}$ is a ring isomorphism of the set of quotients of the set of polynomials of $\mathrm{ZMod}$ applied to $p$ and the span of $\operatorname{singleton}$ applied to the map of the cast ring homomorphism of $\mathrm{ZMod}$ applied to $p$ and $Q$ and the set of quotients of the set of rings of integer of $K$ and the span of $\operatorname{insert}$ applied to $p$ and $\operatorname{singleton}$ applied to $\operatorname{aeval}$ applied to $x_{1}$ and $Q$.

RingOfIntegers.exponentdefMathlib.NumberTheory.NumberField.Ideal.KummerDedekind, function or constant

Wording

the exponent of x1 (from the name)

English

Let $x_{1}$ be a ring of integer of $K$. Then the exponent of $x_{1}$ is a natural number defined as $\operatorname{absNorm}$ applied to $\operatorname{under}$ applied to $\Integer$ and the conductor of $\Integer$ and $x_{1}$.

RingOfIntegers.monicFactorsModdefMathlib.NumberTheory.NumberField.Ideal.KummerDedekind, function or constant

Wording

no wording

English

Let $x_{1}$ be a ring of integer of $K$. Let $p$ be a natural number. Then $\operatorname{monicFactorsMod}$ applied to $x_{1}$ and $p$ is a finite set of the set of polynomials of $\mathrm{ZMod}$ applied to $p$ defined as the finite set of the normalized factor of the map of the cast ring homomorphism of $\mathrm{ZMod}$ applied to $p$ and the minimal polynomial of $\Integer$ and $x_{1}$.

Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

NumberField.InfiniteAdeleRingdefMathlib.NumberTheory.NumberField.InfiniteAdeleRing, type

Wording

infinite adele ring of K (from the name)

English

Let $K$ be a set. Then an infinite adele ring of $K$ is an element of the function that maps $K$ to the set of functions from infinite places $v$ of $K$ to completions of $v$.

NumberField.InfiniteAdeleRing.ofCompletiondefMathlib.NumberTheory.NumberField.InfiniteAdeleRing, function or constant

Wording

the embedding of the completion of v (from the docstring)

English

Let $v$ be an infinite place of $K$. Then the embedding of the completion of $v$ is a monoid homomorphism of the set of completions of $v$ and the set of infinite adele rings of $K$ defined as $\operatorname{mulSingle}$ applied to the set of elements of $\operatorname{Completion}$ and $v$.

NumberField.InfiniteAdeleRing.ringEquiv_mixedSpacedefMathlib.NumberTheory.NumberField.InfiniteAdeleRing, function or constant

Wording

the ring isomorphism between the infinite adele ring of K (from the docstring)

English

Let $K$ be a set. Then the ring isomorphism between the infinite adele ring of $K$ is a ring isomorphism of the set of infinite adele rings of $K$ and the set of mixed spaces of $K$.

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

NumberField.InfinitePlacedefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, type

Wording

infinite place of K (from the name)

English

Let $K$ be a set. Then an infinite place of $K$ is an element of the function that maps $K$ to $\SubtypeSet {w}{\mathrm{exists} (\mathrm{RingHom} (K , \mathrm{Complex}), \lambda x_{1} . \EqtMACRoH {\operatorname{place} (x_{1})}{w})}$.

NumberField.InfinitePlace.IsComplexdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, predicate

Wording

w is complex (from the docstring)

English

Let $w$ be an infinite place of $K$. Then $w$ is complex, if there exists a ring homomorphism $x_{1}$ of $K$ and the set of complexes, such that $x_{1}$ is not real and $\EqtMACRoH {\operatorname{mk} (x_{1})}{w}$.

NumberField.InfinitePlace.IsRealdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, predicate

Wording

w is real (from the docstring)

English

Let $w$ be an infinite place of $K$. Then $w$ is real, if there exists a ring homomorphism $x_{1}$ of $K$ and the set of complexes, such that $x_{1}$ is real and $\EqtMACRoH {\operatorname{mk} (x_{1})}{w}$.

NumberField.InfinitePlace.LiesOverdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, predicate

Wording

no wording

English

Let $w$ be an infinite place of $L$. Let $v$ be an infinite place of $K$. Then $\operatorname{LiesOver}$ holds for $w$ and $v$, if $\operatorname{LiesOver}$ holds for $w$ and $v$.

NumberField.InfinitePlace.embeddingdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

the embedding of w (from the name)

English

Let $w$ be an infinite place of $K$. Then the embedding of $w$ is a ring homomorphism of $K$ and the set of complexes.

NumberField.InfinitePlace.embedding_of_isRealdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

the embedding of hw (from the name)

English

Assume that $w$ is real. Then the embedding of $\mathrm{hw}$ is a ring homomorphism of $K$ and $\Real$.

NumberField.InfinitePlace.mkdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a ring homomorphism of $K$ and the set of complexes. Then $\operatorname{mk}$ applied to $x_{1}$ is an infinite place of $K$ defined as the place of $x_{1}$.

NumberField.InfinitePlace.mkComplexdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

the complex of x1 (from the name)

English

Let $x_{1}$ be an element of $\SubtypeSet {x_{2}}{\mathrm{not} (\operatorname{IsReal} (x_{2}))}$. Then the complex of $x_{1}$ is an element of $\SubtypeSet {w}{\operatorname{IsComplex} (w)}$.

NumberField.InfinitePlace.mkRealdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

no wording

English

$\operatorname{mkReal}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{\operatorname{IsReal} (x_{1})})}{(\SubtypeSet {w}{\operatorname{IsReal} (w)})}$.

NumberField.InfinitePlace.multdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

the multiplicity of w (from the docstring)

English

Let $w$ be an infinite place of $K$. Then the multiplicity of $w$ is an element of $\Natural$ defined as $\iteMACRoG {\operatorname{IsReal} (w)}{1}{2}$.

NumberField.InfinitePlace.nrComplexPlacesdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{nrComplexPlaces}$ applied to $K$ is an element of $\Natural$ defined as the cardinality of $\SubtypeSet {w}{\operatorname{IsComplex} (w)}$.

NumberField.InfinitePlace.nrRealPlacesdefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{nrRealPlaces}$ applied to $K$ is an element of $\Natural$ defined as the cardinality of $\SubtypeSet {w}{\operatorname{IsReal} (w)}$.

NumberField.IsInfinitePlacedefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, predicate

Wording

w is a infinite place (from the name)

English

Let $w$ be an absolute value of $K$ and $\Real$. Then $w$ is an infinite place, if there exists a ring homomorphism $x_{1}$ of $K$ and the set of complexes, such that the place of $x_{1}$ is equal to $w$.

Rat.infinitePlacedefMathlib.NumberTheory.NumberField.InfinitePlace.Basic, function or constant

Wording

the infinite place (from the name)

English

The infinite place is an infinite place of $\Rational$ defined as $\operatorname{mk}$ applied to the cast homomorphism of the set of complexes.

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

NumberField.ComplexEmbedding.ExtensiondefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, type

Wording

extension of L and x2 (from the name)

English

Let $L$ be a set. Let $x_{2}$ be a ring homomorphism of $K$ and the set of complexes. Then an extension of $L$ and $x_{2}$ is an element of the function that maps $L$ and $x_{2}$ to $\SubtypeSet {x_{4}}{\operatorname{LiesOver} (x_{4} , x_{2})}$.

NumberField.ComplexEmbedding.IsConjdefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, predicate

Wording

x3 is conjugate to x4 (from the name)

English

Let $x_{3}$ be a ring homomorphism of $K$ and the set of complexes. Let $x_{4}$ be an algebra isomorphism of $K$ and $K$. Then $x_{3}$ is conjugate to $x_{4}$, if the conjugate of $x_{3}$ is equal to the composition of $x_{3}$ and the ring homomorphism of $x_{4}$.

NumberField.ComplexEmbedding.IsMixeddefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, predicate

Wording

x3 is mixed (from the name)

English

Let $K$ be a set. Let $x_{3}$ be a ring homomorphism of $L$ and the set of complexes. Then $x_{3}$ is mixed, if the composition of $x_{3}$ and the algebra map of $K$ and $L$ is real and $x_{3}$ is not real.

NumberField.ComplexEmbedding.IsRealdefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, predicate

Wording

x1 is real (from the name)

English

Let $x_{1}$ be a ring homomorphism of $K$ and the set of complexes. Then $x_{1}$ is real, if $x_{1}$ is self-adjoint.

NumberField.ComplexEmbedding.IsReal.embeddingdefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, function or constant

Wording

the embedding of h (from the name)

English

Assume that $x_{1}$ is real. Then the embedding of $h$ is a ring homomorphism of $K$ and $\Real$.

NumberField.ComplexEmbedding.IsUnmixeddefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, predicate

Wording

x3 is unmixed (from the name)

English

Let $K$ be a set. Let $x_{3}$ be a ring homomorphism of $L$ and the set of complexes. Then $x_{3}$ is unmixed, if if the composition of $x_{3}$ and the algebra map of $K$ and $L$ is real, then $x_{3}$ is real.

NumberField.ComplexEmbedding.LiesOverclassMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, predicate

Wording

no wording

English

Let $x_{3}$ be a ring homomorphism of $L$ and the set of complexes. Let $x_{4}$ be a ring homomorphism of $K$ and the set of complexes. Then we can say that $\operatorname{LiesOver}$ holds for $x_{3}$ and $x_{4}$.

NumberField.ComplexEmbedding.conjugatedefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, function or constant

Wording

the conjugate of x1 (from the docstring)

English

Let $x_{1}$ be a ring homomorphism of $K$ and the set of complexes. Then the conjugate of $x_{1}$ is a ring homomorphism of $K$ and the set of complexes defined as the star of $x_{1}$.

NumberField.ComplexEmbedding.liftdefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, function or constant

Wording

the lift of K and x3 (from the name)

English

Let $K$ be a set. Let $x_{3}$ be a ring homomorphism of $k$ and the set of complexes. Then the lift of $K$ and $x_{3}$ is a ring homomorphism of $K$ and the set of complexes defined as $\operatorname{toRingHom}$ applied to the lift.

NumberField.ComplexEmbedding.mixedEmbeddingsOverdefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, function or constant

Wording

no wording

English

Let $L$ be a set. Let $x_{2}$ be a ring homomorphism of $K$ and the set of complexes. Then $\operatorname{mixedEmbeddingsOver}$ applied to $L$ and $x_{2}$ is an element of the power set of the set of ring homomorphisms of $L$ and the set of complexes defined as $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $\operatorname{LiesOver}$ holds for $x_{4}$ and $x_{2}$ and $x_{4}$ is mixed.

NumberField.ComplexEmbedding.unmixedEmbeddingsOverdefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, function or constant

Wording

no wording

English

Let $L$ be a set. Let $x_{2}$ be a ring homomorphism of $K$ and the set of complexes. Then $\operatorname{unmixedEmbeddingsOver}$ applied to $L$ and $x_{2}$ is an element of the power set of the set of ring homomorphisms of $L$ and the set of complexes defined as $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $\operatorname{LiesOver}$ holds for $x_{4}$ and $x_{2}$ and $x_{4}$ is unmixed.

NumberField.placedefMathlib.NumberTheory.NumberField.InfinitePlace.Embeddings, function or constant

Wording

the place of x2 (from the name)

English

Let $x_{2}$ be a ring homomorphism of $K$ and $A$. Then the place of $x_{2}$ is an absolute value of $K$ and $\Real$.

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

IsUnramifiedAtInfinitePlacesclassMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, predicate

Wording

no wording

English

Let $k$ and $K$ be sets. Then we can say that $\mathrm{IsUnramifiedAtInfinitePlaces}$ holds for $k$ and $K$.

NumberField.InfinitePlace.IsRamifieddefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, predicate

Wording

k is ramified (from the docstring)

English

Let $k$ be a set. Let $w$ be an infinite place of $K$. Then $k$ is ramified, if $k$ is not unramified.

NumberField.InfinitePlace.IsUnramifieddefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, predicate

Wording

k is unramified (from the docstring)

English

Let $k$ be a set. Let $w$ be an infinite place of $K$. Then $k$ is unramified, if the multiplicity of the preimage of $w$ and the algebra map of $k$ and $K$ is equal to the multiplicity of $w$.

NumberField.InfinitePlace.IsUnramifiedIndefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, predicate

Wording

K is unramified (from the docstring)

English

Let $K$ be a set. Let $w$ be an infinite place of $k$. Then $K$ is unramified, if for all infinite places $v$ of $K$, if the preimage of $v$ and the algebra map of $k$ and $K$ is equal to $w$, then $k$ is unramified.

NumberField.InfinitePlace.comapdefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, function or constant

Wording

the preimage of w and f (from the name)

English

Let $w$ be an infinite place of $K$. Let $f$ be a ring homomorphism of $k$ and $K$. Then the preimage of $w$ and $f$ is an infinite place of $k$.

NumberField.InfinitePlace.orbitRelEquivdefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, function or constant

Wording

the orbit relative equivalence (from the name)

English

The orbit relative equivalence is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to the set of algebra isomorphisms of $K$ and $K$ and the set of infinite places of $K$ to the set of infinite places of $k$.

NumberField.InfinitePlace.placesOverdefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, function or constant

Wording

no wording

English

Let $L$ be a set. Let $v$ be an infinite place of $K$. Then $\operatorname{placesOver}$ applied to $L$ and $v$ is an element of the power set of the set of infinite places of $L$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to $\operatorname{LiesOver}$ applied to $w$ and $v$.

NumberField.InfinitePlace.ramifiedPlacesOverdefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, function or constant

Wording

no wording

English

Let $L$ be a set. Let $v$ be an infinite place of $K$. Then $\operatorname{ramifiedPlacesOver}$ applied to $L$ and $v$ is an element of the power set of the set of infinite places of $L$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to the proposition that $\operatorname{LiesOver}$ holds for $w$ and $v$ and $K$ is ramified.

NumberField.InfinitePlace.unramifiedPlacesOverdefMathlib.NumberTheory.NumberField.InfinitePlace.Ramification, function or constant

Wording

no wording

English

Let $L$ be a set. Let $v$ be an infinite place of $K$. Then $\operatorname{unramifiedPlacesOver}$ applied to $L$ and $v$ is an element of the power set of the set of infinite places of $L$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to the proposition that $\operatorname{LiesOver}$ holds for $w$ and $v$ and $K$ is unramified.

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

NumberField.IsTotallyComplexclassMathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex, predicate

Wording

K is totally complex (from the name)

English

generation took over the time limit

NumberField.IsTotallyRealclassMathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex, predicate

Wording

K is totally real (from the name)

English

generation took over the time limit

NumberField.maximalRealSubfielddefMathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex, function or constant

Wording

the maximal real subfield of K (from the docstring)

English

Let $K$ be a set. Then the maximal real subfield of $K$ is a subfield of $K$.

Mathlib.NumberTheory.NumberField.Norm

RingOfIntegers.normdefMathlib.NumberTheory.NumberField.Norm, function or constant

Wording

the norm of K (from the name)

English

Let $K$ be a set. Then the norm of $K$ is a monoid homomorphism of the set of rings of integer of $L$ and the set of rings of integer of $K$.

Mathlib.NumberTheory.NumberField.Units.Basic

NumberField.Units.complexEmbeddingdefMathlib.NumberTheory.NumberField.Units.Basic, function or constant

Wording

the complex embedding of x1 (from the name)

English

Let $x_{1}$ be a ring homomorphism of $K$ and the set of complexes. Then the complex embedding of $x_{1}$ is a monoid homomorphism of the set of units of the set of rings of integer of $K$ and the set of units of the set of complexes defined as the composition of the map of the monoid homomorphism of $x_{1}$ and the map of $\operatorname{toMonoidHom}$ applied to the algebra map of the set of rings of integer of $K$ and $K$.

NumberField.Units.torsiondefMathlib.NumberTheory.NumberField.Units.Basic, function or constant

Wording

the torsion of K (from the name)

English

Let $K$ be a set. Then the torsion of $K$ is a subgroup of the set of units of the set of rings of integer of $K$ defined as the torsion subgroup of the set of units of the set of rings of integer of $K$.

NumberField.Units.torsionOrderdefMathlib.NumberTheory.NumberField.Units.Basic, function or constant

Wording

the order of the torsion subgroup of K (from the docstring)

English

Let $K$ be a set. Then the order of the torsion subgroup of $K$ is an element of $\Natural$ defined as the cardinality of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (K)}{x_{1}})}$.

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

NumberField.Units.basisModTorsiondefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{basisModTorsion}$ applied to $K$ is a basis of $\Integer$ and $\mathrm{Additive}$ applied to the set of quotients of the set of units of the set of rings of integer of $K$ and the torsion of $K$.

NumberField.Units.basisUnitLatticedefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the basis unit lattice of K (from the name)

English

Let $K$ be a set. Then the basis unit lattice of $K$ is a basis of $\Integer$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{unitLattice} (K)}{x_{1}})}$ defined as the map of $\operatorname{basisModTorsion}$ applied to $K$ and the logarithm embedding equivalence of $K$.

NumberField.Units.dirichletUnitTheorem.logSpacedefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, type

Wording

logarithm space of K (from the name)

English

Let $K$ be a set. Then a logarithm space of $K$ is an element of the function that maps $K$ to the set of functions from elements of $\SubtypeSet {w}{\mathrm{Neq} (w , \mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_})}$ to real numbers.

NumberField.Units.dirichletUnitTheorem.seqdefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the sequence of x1 and x2 (from the name)

English

Let $K$ be a set. Let $x_{1}$ be an infinite place of $K$. Assume that the Minkowski bound of $K$ and $1$ is less than $\operatorname{ofNNReal} (\operatorname{convexBodyLTFactor} (K))\times B$. Let $x_{2}$ be a natural number. Then the sequence of $x_{1}$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{\mathrm{Neq} (x_{3} , 0)}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_seq\_\_\_f}$ applied to $K$, $x_{1}$ and $\mathrm{hB}$.

NumberField.Units.dirichletUnitTheorem.w₀defMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

no wording

English

$\mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_}$ is an infinite place of $K$.

NumberField.Units.fundSystemdefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

no wording

English

Let $K$ be a set. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to the rank of $K$. Then $\operatorname{fundSystem}$ applied to $K$ and $x_{1}$ is a unit of the set of rings of integer of $K$ defined as $\operatorname{out}$ applied to $\operatorname{toMul}$ applied to $\operatorname{basisModTorsion}$ applied to $K$ and $x_{1}$.

NumberField.Units.logEmbeddingdefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the logarithm embedding of K (from the name)

English

Let $K$ be a set. Then the logarithm embedding of $K$ is an additive monoid homomorphism of $\mathrm{Additive}$ applied to the set of units of the set of rings of integer of $K$ and the set of logarithm spaces of $K$.

NumberField.Units.logEmbeddingEquivdefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the logarithm embedding equivalence of K (from the name)

English

Let $K$ be a set. Then the logarithm embedding equivalence of $K$ is a linear equivalence of $\mathrm{Additive}$ applied to the set of quotients of $\UnitsMACRoAO {\operatorname{RingOfIntegers} (K)}$ and the torsion of $K$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{unitLattice} (K)}{x_{1}})}$.

NumberField.Units.logEmbeddingQuotdefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the logarithm embedding quotient of K (from the name)

English

Let $K$ be a set. Then the logarithm embedding quotient of $K$ is an additive monoid homomorphism of $\mathrm{Additive}$ applied to the set of quotients of the set of units of the set of rings of integer of $K$ and the torsion of $K$ and the set of logarithm spaces of $K$.

NumberField.Units.rankdefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the rank of K (from the name)

English

Let $K$ be a set. Then the rank of $K$ is a natural number defined as the difference between the cardinality of the set of infinite places of $K$ and $1$.

NumberField.Units.unitLatticedefMathlib.NumberTheory.NumberField.Units.DirichletTheorem, function or constant

Wording

the unit lattice of K (from the name)

English

Let $K$ be a set. Then the unit lattice of $K$ is a submodule of $\Integer$ and the set of logarithm spaces of $K$ defined as the map of the integer linear map of the logarithm embedding of $K$ and the top.

Mathlib.NumberTheory.NumberField.Units.Regulator

NumberField.Units.IsMaxRankdefMathlib.NumberTheory.NumberField.Units.Regulator, predicate

Wording

u is a maximum rank (from the name)

English

Let $u$ be a function from elements of $\mathrm{Fin}$ applied to the rank of $K$ to units of the set of rings of integer of $K$. Then $u$ is a maximum rank, if $\mathrm{LinearIndependent}$ holds for $\Real$ and the function that maps $i$ to $\operatorname{logEmbedding}$ applied to $K$ and $\operatorname{ofMul}$ applied to $u$ applied to $i$.

NumberField.Units.basisOfIsMaxRankdefMathlib.NumberTheory.NumberField.Units.Regulator, function or constant

Wording

the basis of hu (from the name)

English

Assume that $u$ is a maximum rank. Then the basis of $\mathrm{hu}$ is a basis of $\Real$ and the set of logarithm spaces of $K$.

NumberField.Units.equivFinRankdefMathlib.NumberTheory.NumberField.Units.Regulator, function or constant

Wording

the equivalence finite rank of K (from the name)

English

Let $K$ be a set. Then the equivalence finite rank of $K$ is an equivalence from $\mathrm{Fin}$ applied to the rank of $K$ to $\SubtypeSet {w}{\mathrm{Neq} (w , \mathrm{NumberField\_\_Units\_\_dirichletUnitTheorem\_\_w\_u2080\_})}$.

NumberField.Units.regOfFamilydefMathlib.NumberTheory.NumberField.Units.Regulator, function or constant

Wording

the regulator of u (from the docstring)

English

Let $u$ be a function from elements of $\mathrm{Fin}$ applied to the rank of $K$ to units of the set of rings of integer of $K$. Then the regulator of $u$ is a real number defined as $\mathrm{dite}$ applied to the proposition that $u$ is a maximum rank, the function that maps $\mathrm{hu}$ to $\operatorname{covolume}$ applied to the span of $\Integer$ and the range of $\operatorname{coe}$ applied to the basis of $\mathrm{hu}$ and the volume and the function that maps $\mathrm{hu1}$ to $0$.

NumberField.Units.regulatordefMathlib.NumberTheory.NumberField.Units.Regulator, function or constant

Wording

the regulator of K (from the docstring)

English

Let $K$ be a set. Then the regulator of $K$ is a real number defined as $\operatorname{covolume}$ applied to the unit lattice of $K$ and the volume.

Mathlib.NumberTheory.Ostrowski

Rat.AbsoluteValue.padicdefMathlib.NumberTheory.Ostrowski, function or constant

Wording

the p-adic number of p (from the name)

English

Let $p$ be a natural number. Then the number ['\'p-adic_Adj\''] of $p$ is an absolute value of $\Rational$ and $\Real$.

Rat.AbsoluteValue.realdefMathlib.NumberTheory.Ostrowski, function or constant

Wording

no wording

English

$\operatorname{real}$ is an absolute value of $\Rational$ and $\Real$.

Mathlib.NumberTheory.Padics.AddChar

PadicInt.addChar_of_value_at_onedefMathlib.NumberTheory.Padics.AddChar, function or constant

Wording

the additive characteristic of r and hr (from the name)

English

Let $r$ be an element of $R$ such that $\operatorname{Tendsto}$ holds for the function that maps $x_{2}$ to $r ^ {x_{2}}$, $\operatorname{atTop}$ and the neighbourhood filter of $0$. Then the additive characteristic of $r$ and $\mathrm{hr}$ is an additive characteristic of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $R$.

PadicInt.continuousAddCharEquivdefMathlib.NumberTheory.Padics.AddChar, function or constant

Wording

the continuous additive characteristic equivalence of p and R (from the name)

English

Let $p$ be an element of $\Natural$. Let $R$ be a set. Then the continuous additive characteristic equivalence of $p$ and $R$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{\mathrm{Continuous} (\operatorname{coe} (x_{2}))})}{(\SubtypeSet {r}{\operatorname{Tendsto} (\lambda x_{3} . r ^ {x_{3}}, \operatorname{atTop} , \mathrm{nhds} (0))})}$.

PadicInt.continuousAddCharEquiv_of_norm_muldefMathlib.NumberTheory.Padics.AddChar, function or constant

Wording

the continuous additive characteristic equivalence of p and R (from the name)

English

Mathlib.NumberTheory.Padics.Complex

PadicAlgCldefMathlib.NumberTheory.Padics.Complex, type

Wording

fixed algebraic closure of p (from the docstring)

English

Let $p$ be a natural number. Then a fixed algebraic closure of $p$ is an element of the function that maps $p$ to the set of algebraic closures of the set of numbers ['\'p-adic_Adj\''] of $p$.

PadicComplexdefMathlib.NumberTheory.Padics.Complex, type

Wording

p-adic number complex of p (from the name)

English

Let $p$ be a natural number. Then a number complex ['\'p-adic_Adj\''] of $p$ is an element of the function that maps $p$ to the set of completions of the set of fixed algebraic closures of $p$.

PadicComplexIntdefMathlib.NumberTheory.Padics.Complex, function or constant

Wording

the p-adic number complex integer of p (from the name)

English

Let $p$ be a natural number. Then the number complex integer ['\'p-adic_Adj\''] of $p$ is a valuation subring of the set of number complexes ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as the valuation subring of $\operatorname{v}$.

Mathlib.NumberTheory.Padics.HeightOneSpectrum

Padic.adicCompletionEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the adic completion equivalence of R and p (from the name)

English

Let $R$ be a set. Let $p$ be a prime number. Then the adic completion equivalence of $R$ and $p$ is a continuous algebra isomorphism of the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of adic completions of $\Rational$ and $\operatorname{symm}$ applied to the prime equivalence and $p$.

PadicInt.adicCompletionIntegersEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the adic completion integer equivalence of R and p (from the name)

English

Let $R$ be a set. Let $p$ be an element of $\NatPrimesMACRoA$. Then the adic completion integer equivalence of $R$ and $p$ is a continuous algebra isomorphism of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adicCompletionIntegers} (\Rational , \operatorname{symm} (\operatorname{primesEquiv} , p))}{x_{2}})}$.

Rat.HeightOneSpectrum.adicCompletion.padicEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the p-adic number equivalence of v (from the name)

English

Let $v$ be a height one spectrum of $R$. Then the number equivalence ['\'p-adic_Adj\''] of $v$ is a continuous algebra isomorphism of the set of adic completions of $\Rational$ and $v$ and the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $\operatorname{primesEquiv}$ applied to $v$.

Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the p-adic number integer equivalence of v (from the name)

English

Let $v$ be a height one spectrum of $R$. Then the number integer equivalence ['\'p-adic_Adj\''] of $v$ is a continuous algebra isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adicCompletionIntegers} (\Rational , v)}{x_{2}})}$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $\operatorname{primesEquiv}$ applied to $v$.

Rat.HeightOneSpectrum.natGeneratordefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the natural generator of v (from the name)

English

Let $v$ be a height one spectrum of $R$. Then the natural generator of $v$ is a natural number defined as the absolute value of the generator of the map of the integer equivalence of $R$ and $\operatorname{asIdeal}$ applied to $v$.

Rat.HeightOneSpectrum.primesEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the prime equivalence (from the name)

English

The prime equivalence is an equivalence from the set of height one spectra of $R$ to $\NatPrimesMACRoA$.

Rat.HeightOneSpectrum.withValEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of $R$. Then $\operatorname{withValEquiv}$ applied to $v$ is a uniform equivalence of $\mathrm{WithVal}$ applied to the valuation of $\Rational$ and $v$ and $\mathrm{WithVal}$ applied to the number valuation ['\'\\\'p-adic_Adj\\\'\''] of $\operatorname{primesEquiv}$ applied to $v$ defined as the uniform equivalence of $\mathrm{Rat\_\_HeightOneSpectrum\_\_valuation\_equiv\_padicValuation}$ applied to $v$.

Rat.IsIntegralClosure.intEquivdefMathlib.NumberTheory.Padics.HeightOneSpectrum, function or constant

Wording

the integer equivalence of R (from the name)

English

Let $R$ be a set. Then the integer equivalence of $R$ is a ring isomorphism of $R$ and $\Integer$ defined as the composition of the inverse of the equivalence of $R$ and the ring.

Mathlib.NumberTheory.Padics.MahlerBasis

PadicInt.mahlerEquivdefMathlib.NumberTheory.Padics.MahlerBasis, function or constant

Wording

the Mahler equivalence of E (from the name)

English

Let $E$ be a set. Then the Mahler equivalence of $E$ is a linear isometry equivalence of the set of continuous maps of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $E$ and the set of zero at infty continuous maps of $\Natural$ and $E$.

PadicInt.mahlerSeriesdefMathlib.NumberTheory.Padics.MahlerBasis, function or constant

Wording

the Mahler series of a (from the name)

English

Let $a$ be a function from natural numbers to elements of $E$. Then the Mahler series of $a$ is a continuous map of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $E$ defined as the sum of the function that maps $n$ to the Mahler term of $a$ applied to $n$ and $n$ and $\operatorname{unconditional}$ applied to $\Natural$.

PadicInt.mahlerTermdefMathlib.NumberTheory.Padics.MahlerBasis, function or constant

Wording

the Mahler term of a and n (from the name)

English

Let $a$ be an element of $E$. Let $n$ be an element of $\Natural$. Then the Mahler term of $a$ and $n$ is a continuous map of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $E$ defined as $\HSMulhSMulMACRoAL {\mathrm{mahler} (n)}{\operatorname{const} (\mathrm{PadicInt} (p), a)}$.

mahlerdefMathlib.NumberTheory.Padics.MahlerBasis, function or constant

Wording

no wording

English

Let $k$ be a natural number. Then $\mathrm{mahler}$ applied to $k$ is a continuous map of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as $\operatorname{mk}$ applied to the function that maps $x$ to $\operatorname{choose}$ applied to $x$ and $k$ and $\mathrm{PadicInt\_\_continuous\_choose}$ applied to $k$.

Mathlib.NumberTheory.Padics.Measure.AmiceTransform

AbstractMeasure.amiceTransformdefMathlib.NumberTheory.Padics.Measure.AmiceTransform, function or constant

Wording

no wording

English

$\operatorname{amiceTransform}$ is a linear map of the set of abstract measures of $R$ and $R$ and the set of power series of $R$.

AbstractMeasure.amiceTransformEquivdefMathlib.NumberTheory.Padics.Measure.AmiceTransform, function or constant

Wording

no wording

English

$\operatorname{amiceTransformEquiv}$ is a linear equivalence of the set of abstract measures of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of power series of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

AbstractMeasure.invTransformdefMathlib.NumberTheory.Padics.Measure.AmiceTransform, function or constant

Wording

the inverse transform of F (from the name)

English

Let $F$ be a power series of the set of number integers ['\'p-adic_Adj\''] of $p$. Then the inverse transform of $F$ is an abstract measure of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

Mathlib.NumberTheory.Padics.Measure.Basic

AbstractMeasuredefMathlib.NumberTheory.Padics.Measure.Basic, type

Wording

abstract measure of R and E (from the name)

English

Let $X$, $R$ and $E$ be sets. Then an abstract measure of $R$ and $E$ is an element of the function that maps $X$, $R$ and $E$ to the set of continuous linear maps of the set of continuous maps of $X$ and $R$ and $E$.

AbstractMeasure.arrowCongrLeftdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

the left arrow congruence of x7 (from the name)

English

Let $x_{7}$ be a homeomorphism of $X$ and $Y$. Then the left arrow congruence of $x_{7}$ is a linear equivalence of the set of abstract measures of $R$ and $E$ and the set of abstract measures of $R$ and $E$.

AbstractMeasure.contractFstdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

no wording

English

$\operatorname{contractFst}$ is a linear map of the set of abstract measures of $R$ and $R$ and the set of linear maps of the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$ and the set of continuous maps of $Y$ and $R$ defined as the composition of $\operatorname{lcomp}$ applied to $R$, the set of continuous maps of $Y$ and $R$ and $\operatorname{toLinearMap}$ applied to the composition continuous linear map of the product swap and $\operatorname{contractSnd}$.

AbstractMeasure.contractFstCLMdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

no wording

English

$\operatorname{contractFstCLM}$ is a linear map of the set of abstract measures of $R$ and $R$ and the set of continuous linear maps of the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$ and the set of continuous maps of $Y$ and $R$ defined as the composition of $\operatorname{lcomp}$ applied to the set of continuous maps of $Y$ and $R$ and the composition continuous linear map of the product swap and $\operatorname{contractSndCLM}$.

AbstractMeasure.contractSnddefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

no wording

English

$\operatorname{contractSnd}$ is a linear map of the set of abstract measures of $R$ and $R$ and the set of linear maps of the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$ and the set of continuous maps of $X$ and $R$.

AbstractMeasure.contractSndCLMdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

no wording

English

$\operatorname{contractSndCLM}$ is a linear map of the set of abstract measures of $R$ and $R$ and the set of continuous linear maps of the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$ and the set of continuous maps of $X$ and $R$.

AbstractMeasure.diracdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

the Dirac of R and x3 (from the name)

English

Let $R$ be a set. Let $x_{3}$ be an element of $X$. Then the Dirac of $R$ and $x_{3}$ is an abstract measure of $R$ and $R$ defined as $\operatorname{symm}$ applied to the continuous linear map equivalence and the evaluation continuous linear map of $R$ and $x_{3}$.

AbstractMeasure.mapdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a continuous map of $X$ and $Y$. Then the map of $f$ is a linear map of the set of abstract measures of $R$ and $E$ and the set of abstract measures of $R$ and $E$.

AbstractMeasure.prodMkdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

the product (from the name)

English

The product is a linear map of the set of abstract measures of $R$ and $R$ and the set of linear maps of the set of abstract measures of $R$ and $R$ and the set of abstract measures of $R$ and $R$ defined as the composition of $\operatorname{llcomp}$ applied to $R$, the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$, the set of continuous maps of $Y$ and $R$ and $R$ and $\operatorname{contractFstCLM}$.

AbstractMeasure.prodMk'defMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

the product (from the name)

English

The product is a linear map of the set of abstract measures of $R$ and $R$ and the set of linear maps of the set of abstract measures of $R$ and $R$ and the set of abstract measures of $R$ and $R$ defined as the flip of the composition of $\operatorname{llcomp}$ applied to $R$, the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$, the set of continuous maps of $X$ and $R$ and $R$ and $\operatorname{contractSndCLM}$.

AbstractMeasure.toCLMEquivdefMathlib.NumberTheory.Padics.Measure.Basic, function or constant

Wording

the continuous linear map equivalence (from the name)

English

The continuous linear map equivalence is a linear equivalence of the set of abstract measures of $R$ and $E$ and the set of continuous linear maps of the set of continuous maps of $X$ and $R$ and $E$ defined as the identity map of $R$ and the set of abstract measures of $R$ and $E$.

Mathlib.NumberTheory.Padics.Measure.Monoid

AbstractMeasure.convolveFunRightdefMathlib.NumberTheory.Padics.Measure.Monoid, function or constant

Wording

no wording

English

$\operatorname{convolveFunRight}$ is a linear map of the set of abstract measures of $R$ and $R$ and the set of linear maps of the set of continuous maps of $G$ and $R$ and the set of continuous maps of $G$ and $R$.

AbstractMeasure.diracHomdefMathlib.NumberTheory.Padics.Measure.Monoid, function or constant

Wording

the Dirac map (from the docstring)

English

The Dirac map is a monoid homomorphism of $G$ and the set of abstract measures of $R$ and $R$.

AbstractMeasure.monoidAlgebraHomdefMathlib.NumberTheory.Padics.Measure.Monoid, function or constant

Wording

the canonical homomorphism from the monoid algebra (from the docstring)

English

The canonical homomorphism from the monoid algebra is an algebra homomorphism of the set of monoid algebras of $R$ and $G$ and the set of abstract measures of $R$ and $R$ defined as $\operatorname{lift}$ applied to $R$, the set of abstract measures of $R$ and $R$, $G$ and the Dirac map.

Mathlib.NumberTheory.Padics.PadicIntegers

Padic.liftdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the lift of x and hx (from the name)

English

Let $x$ be a number ['\'\\\'p-adic_Adj\\\'\''] of $p$ such that the norm of $x$ is less than or equal to $1$. Then the lift of $x$ and $\mathrm{hx}$ is a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as $x$.

PadicIntdefMathlib.NumberTheory.Padics.PadicIntegers, type

Wording

p-adic number integer of p (from the name)

English

Let $p$ be an element of $\Natural$. Then a number integer ['\'p-adic_Adj\''] of $p$ is an element of the function that maps $p$ to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{subring} (p)}{x})}$.

PadicInt.Coe.ringHomdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the ring homomorphism (from the name)

English

The ring homomorphism is a ring homomorphism of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as the subtype of the subring of $p$.

PadicInt.invdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the inverse of z (from the docstring)

English

Let $z$ be a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the inverse of $z$ is a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$.

PadicInt.mkUnitsdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the unit of h (from the name)

English

Assume that the norm of $u$ is equal to $1$. Then the unit of $h$ is a unit of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as $\operatorname{mk}$ applied to $u$, the inverse of $u$, $\mathrm{PadicInt\_\_mul\_inv}$ applied to $h$ and $\mathrm{PadicInt\_\_inv\_mul}$ applied to $h$.

PadicInt.ofIntSeqdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the p-adic number integer of seq and h (from the name)

English

Let $\mathrm{seq}$ be a function from natural numbers to integers such that $\mathrm{IsCauSeq}$ holds for $\mathrm{padicNorm}$ applied to $p$ and the function that maps $n$ to $\mathrm{seq}$ applied to $n$. Then the number integer ['\'p-adic_Adj\''] of $\mathrm{seq}$ and $h$ is a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as $\operatorname{mk}$ applied to $\operatorname{equiv}$ and the function that maps $n$ to $\mathrm{seq}$ applied to $n$.

PadicInt.subringdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the subring of p (from the name)

English

Let $p$ be a natural number. Then the subring of $p$ is a subring of the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

PadicInt.unitCoeffdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the unit coefficient of hx (from the name)

English

Assume that $x \neq 0$. Then the unit coefficient of $\mathrm{hx}$ is a unit of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

PadicInt.valuationdefMathlib.NumberTheory.Padics.PadicIntegers, function or constant

Wording

the valuation of x (from the name)

English

Let $x$ be a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the valuation of $x$ is a natural number defined as $\operatorname{toNat}$ applied to the valuation of $x$.

Mathlib.NumberTheory.Padics.PadicNorm

padicNormdefMathlib.NumberTheory.Padics.PadicNorm, function or constant

Wording

the p-adic number norm of p and q (from the name)

English

Let $p$ be an element of $\Natural$. Let $q$ be an element of $\Rational$. Then the number norm ['\'p-adic_Adj\''] of $p$ and $q$ is an element of $\Rational$ defined as $\iteMACRoG {\mathrm{Eq} (q , 0)}{0}{(p ^ {\operatorname{neg} (\mathrm{padicValRat} (p , q))})}$.

Mathlib.NumberTheory.Padics.PadicNumbers

Int.padicValuationdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the p-adic number valuation of p (from the name)

English

Let $p$ be a natural number. Then the number valuation ['\'p-adic_Adj\''] of $p$ is a valuation of $\Integer$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as the preimage of the cast ring homomorphism of $\Rational$ and the number valuation ['\'p-adic_Adj\''] of $p$.

PadicdefMathlib.NumberTheory.Padics.PadicNumbers, type

Wording

p-adic number of p (from the name)

English

Let $p$ be a natural number. Then a number ['\'p-adic_Adj\''] of $p$ is an element of the function that maps $p$ to $\operatorname{Cauchy}$ applied to $\mathrm{padicNorm}$ applied to $p$.

Padic.addValuationdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the additive valuation (from the name)

English

The additive valuation is an additive valuation of the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\mathrm{WithTop}$ applied to $\Integer$ defined as $\operatorname{of}$ applied to $\operatorname{addValuationDef}$, $\mathrm{Padic\_\_AddValuation\_\_map\_zero}$, $\mathrm{Padic\_\_AddValuation\_\_map\_one}$, $\mathrm{Padic\_\_AddValuation\_\_map\_add}$ and $\mathrm{Padic\_\_AddValuation\_\_map\_mul}$.

Padic.addValuationDefdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the additive valuation of x (from the name)

English

Let $x$ be a number ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the additive valuation of $x$ is an element of $\mathrm{WithTop}$ applied to $\Integer$ defined as $\iteMACRoG {(\EqtMACRoH {x}{0})}{\operatorname{top}}{\operatorname{some} (\operatorname{valuation} (x))}$.

Padic.limSeqdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the limit sequence of f and x (from the name)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\operatorname{coe}$ applied to the number norm ['\'\\\'p-adic_Adj\\\'\'']. Let $x$ be a natural number. Then the limit sequence of $f$ and $x$ is a rational number.

Padic.mkdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

no wording

English

Let $x$ be a number sequence ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then $\operatorname{mk}$ applied to $x$ is a number ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as $\operatorname{mk'}$ applied to $x$.

Padic.mulValuationdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the multiplicative valuation (from the name)

English

The multiplicative valuation is a valuation of the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$.

Padic.ratNormdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the rational number norm of q (from the name)

English

Let $q$ be a number ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the rational number norm of $q$ is a rational number defined as $\operatorname{choose}$ applied to $\mathrm{Padic\_\_padicNormE\_\_is\_rat}$ applied to $q$.

Padic.valuationdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the valuation of x (from the name)

English

Let $x$ be a number ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the valuation of $x$ is an integer.

PadicSeqdefMathlib.NumberTheory.Padics.PadicNumbers, type

Wording

p-adic number sequence of p (from the name)

English

Let $p$ be a natural number. Then a number sequence ['\'p-adic_Adj\''] of $p$ is an element of the function that maps $p$ to $\mathrm{CauSeq}$ applied to $\Rational$ and $\mathrm{padicNorm}$ applied to $p$.

PadicSeq.normdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the norm of f (from the name)

English

Let $f$ be a number sequence ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the norm of $f$ is a rational number defined as $\mathrm{dite}$ applied to $\operatorname{Equiv}$ applied to $f$ and $0$, the function that maps $\mathrm{hf}$ to $0$ and the function that maps $\mathrm{hf1}$ to the number norm ['\'p-adic_Adj\''] of $p$ and the stationary point of $\mathrm{hf1}$.

PadicSeq.stationaryPointdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the stationary point of hf (from the name)

English

Assume that it is not the case that $\operatorname{Equiv}$ holds for $f$ and $0$. Then the stationary point of $\mathrm{hf}$ is a natural number defined as $\operatorname{choose}$ applied to $\operatorname{stationary}$ applied to $\mathrm{hf}$.

PadicSeq.valuationdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the valuation of f (from the name)

English

Let $f$ be a number sequence ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the valuation of $f$ is an integer defined as $\mathrm{dite}$ applied to $\operatorname{Equiv}$ applied to $f$ and $0$, the function that maps $\mathrm{hf}$ to $0$ and the function that maps $\mathrm{hf1}$ to the number value rational number ['\'p-adic_Adj\''] of $p$ and the stationary point of $\mathrm{hf1}$.

Rat.padicValuationdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the p-adic number valuation of p (from the name)

English

Let $p$ be a natural number. Then the number valuation ['\'p-adic_Adj\''] of $p$ is a valuation of $\Rational$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$.

padicNormEdefMathlib.NumberTheory.Padics.PadicNumbers, function or constant

Wording

the p-adic number norm (from the name)

English

The number norm ['\'p-adic_Adj\''] is an absolute value of the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\Rational$.

Mathlib.NumberTheory.Padics.PadicVal.Basic

padicValIntdefMathlib.NumberTheory.Padics.PadicVal.Basic, function or constant

Wording

the p-adic number value integer of p and z (from the name)

English

Let $p$ be a natural number. Let $z$ be an integer. Then the number value integer ['\'p-adic_Adj\''] of $p$ and $z$ is a natural number defined as $\padicValNatMACRoL {p}{\IntnatAbsMACRoY {z}}$.

padicValRatdefMathlib.NumberTheory.Padics.PadicVal.Basic, function or constant

Wording

the p-adic number value rational number of p and q (from the name)

English

Let $p$ be a natural number. Let $q$ be a rational number. Then the number value rational number ['\'p-adic_Adj\''] of $p$ and $q$ is an integer defined as the difference between the number value integer ['\'p-adic_Adj\''] of $p$ and $\operatorname{num}$ applied to $q$ and $\padicValNatMACRoL {p}{\operatorname{den} (q)}$.

Mathlib.NumberTheory.Padics.RingHoms

PadicInt.apprdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

no wording

English

Let $x$ be a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$. Let $x_{1}$ be a natural number. Then $\operatorname{appr}$ applied to $x$ and $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{PadicInt\_\_appr\_\_\_f}$ and $x$.

PadicInt.liftdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

the lift of f_compat (from the name)

English

Assume that for all natural numbers $k_{1}$ and $k_{2}$, for all elements $\mathrm{hk}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (k_{1} , k_{2})$, the composition of the cast homomorphism of $\mathrm{pow\_dvd\_pow}$ applied to $p$ and $\mathrm{hk}$ and $\mathrm{ZMod}$ applied to $p ^ {k_{1}}$ and $f$ applied to $k_{2}$ is equal to $f$ applied to $k_{1}$. Then the lift of $\mathrm{f\_compat}$ is a ring homomorphism of $R$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{limNthHom}$ applied to $\mathrm{f\_compat}$ and $\mathrm{PadicInt\_\_limNthHom\_one}$ applied to $\mathrm{f\_compat}$ and $\mathrm{PadicInt\_\_limNthHom\_mul}$ applied to $\mathrm{f\_compat}$, $\mathrm{PadicInt\_\_limNthHom\_zero}$ applied to $\mathrm{f\_compat}$ and $\mathrm{PadicInt\_\_limNthHom\_add}$ applied to $\mathrm{f\_compat}$.

PadicInt.limNthHomdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

the limit nth homomorphism of f_compat and r (from the name)

English

Assume that for all natural numbers $k_{1}$ and $k_{2}$, for all elements $\mathrm{hk}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (k_{1} , k_{2})$, the composition of the cast homomorphism of $\mathrm{pow\_dvd\_pow}$ applied to $p$ and $\mathrm{hk}$ and $\mathrm{ZMod}$ applied to $p ^ {k_{1}}$ and $f$ applied to $k_{2}$ is equal to $f$ applied to $k_{1}$. Let $r$ be an element of $R$. Then the limit nth homomorphism of $\mathrm{f\_compat}$ and $r$ is a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as the number integer ['\'p-adic_Adj\''] of $\operatorname{nthHom}$ applied to $r$ and $\mathrm{PadicInt\_\_isCauSeq\_nthHom}$ applied to $\mathrm{f\_compat}$ and $r$.

PadicInt.modPartdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

no wording

English

Let $p$ be a natural number. Let $r$ be a rational number. Then $\operatorname{modPart}$ applied to $p$ and $r$ is an integer defined as the remainder of the product of $\operatorname{num}$ applied to $r$ and the greatest common divisor of $\operatorname{den}$ applied to $r$ and $p$ modulo $p$.

PadicInt.nthHomdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

the nth homomorphism of k and r (from the name)

English

Let $f$ be a function from natural numbers $k$ to ring homomorphisms of $R$ and $\mathrm{ZMod}$ applied to $p ^ {k}$. Let $r$ be an element of $R$. Let $x_{1}$ be a natural number. Then the nth homomorphism of $f$ and $r$ is an integer defined as the function that maps $x_{1}$ to the value of $k$ applied to $r$ and $f$.

PadicInt.nthHomSeqdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

the nth homomorphism sequence of f_compat and r (from the name)

English

PadicInt.residueFielddefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

the residue field (from the name)

English

The residue field is a ring isomorphism of the set of residue fields of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\mathrm{ZMod}$ applied to $p$.

PadicInt.toZModdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

no wording

English

$\operatorname{toZMod}$ is a ring homomorphism of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\mathrm{ZMod}$ applied to $p$.

PadicInt.toZModHomdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

no wording

English

Let $v$ be a natural number. Let $f$ be a function from number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ to natural numbers such that for all number integers ['\'\\\'\\\\\\\'p-adic_Adj\\\\\\\'\\\'\''] $x_{1}$ of $p$, $x_{1} - f (x_{1})$ is an element of the span of $\operatorname{singleton}$ applied to $v$. Assume that for all number integers ['\'\\\'\\\\\\\'p-adic_Adj\\\\\\\'\\\'\''] $x$ of $p$, for all natural numbers $a$ and $b$, if $x - a$ is an element of the span of $\operatorname{singleton}$ applied to $v$, then if $x - b$ is an element of the span of $\operatorname{singleton}$ applied to $v$, then $\EqtMACRoH {a}{b}$. Then $\operatorname{toZModHom}$ applied to $v$, $f$, $\mathrm{f\_spec}$ and $\mathrm{f\_congr}$ is a ring homomorphism of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\mathrm{ZMod}$ applied to $v$.

PadicInt.toZModPowdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{toZModPow}$ applied to $n$ is a ring homomorphism of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and $\mathrm{ZMod}$ applied to $p ^ {n}$.

PadicInt.zmodReprdefMathlib.NumberTheory.Padics.RingHoms, function or constant

Wording

the integer modulo representation of x (from the name)

English

Let $x$ be a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$. Then the integer modulo representation of $x$ is a natural number.

Mathlib.NumberTheory.Padics.WithVal

Padic.withValRingEquivdefMathlib.NumberTheory.Padics.WithVal, function or constant

Wording

no wording

English

$\operatorname{withValRingEquiv}$ is a ring isomorphism of the set of completions of the number valuation ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

Padic.withValUniformEquivdefMathlib.NumberTheory.Padics.WithVal, function or constant

Wording

no wording

English

$\operatorname{withValUniformEquiv}$ is a uniform equivalence of the set of completions of the number valuation ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of numbers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

PadicInt.withValIntegersRingEquivdefMathlib.NumberTheory.Padics.WithVal, function or constant

Wording

no wording

English

$\operatorname{withValIntegersRingEquiv}$ is a ring isomorphism of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{integer} (\operatorname{Completion} (\operatorname{padicValuation} (p)))}{x})}$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

PadicInt.withValIntegersUniformEquivdefMathlib.NumberTheory.Padics.WithVal, function or constant

Wording

no wording

English

$\operatorname{withValIntegersUniformEquiv}$ is a uniform equivalence of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{integer} (\operatorname{Completion} (\operatorname{padicValuation} (p)))}{x})}$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

Mathlib.NumberTheory.Pell

Pell.IsFundamentaldefMathlib.NumberTheory.Pell, predicate

Wording

a is a fundamental (from the name)

English

Let $a$ be a solution of $d$. Then $a$ is a fundamental, if $1 < \mathrm{Pell\_\_Solution\_u2081\_\_\_x} (a)$, $0 < \mathrm{Pell\_\_Solution\_u2081\_\_\_y} (a)$ and for all solutions $b$ of $d$, if $1 < \mathrm{Pell\_\_Solution\_u2081\_\_\_x} (b)$, then $\mathrm{Pell\_\_Solution\_u2081\_\_\_x} (a)\leq \mathrm{Pell\_\_Solution\_u2081\_\_\_x} (b)$.

Pell.Solution₁defMathlib.NumberTheory.Pell, type

Wording

solution of d (from the name)

English

Let $d$ be an integer. Then a solution of $d$ is an element of the function that maps $d$ to $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{unitary} (\mathrm{Zsqrtd} (d))}{x})}$.

Pell.Solution₁.mkdefMathlib.NumberTheory.Pell, function or constant

Wording

no wording

English

Let $x$ and $y$ be integers such that $x ^ {2}- d \times y ^ {2}= 1$. Then $\mathrm{Pell\_\_Solution\_u2081\_\_\_mk}$ applied to $x$, $y$ and $\mathrm{prop}$ is a solution of $d$ defined as $\operatorname{mk}$ applied to $x$ and $y$.

Pell.Solution₁.xdefMathlib.NumberTheory.Pell, function or constant

Wording

no wording

English

Let $a$ be a solution of $d$. Then $\mathrm{Pell\_\_Solution\_u2081\_\_\_x}$ applied to $a$ is an integer defined as the real part of $a$.

Pell.Solution₁.ydefMathlib.NumberTheory.Pell, function or constant

Wording

no wording

English

Let $a$ be a solution of $d$. Then $\mathrm{Pell\_\_Solution\_u2081\_\_\_y}$ applied to $a$ is an integer defined as the imaginary part of $a$.

Mathlib.NumberTheory.PellMatiyasevic

Pell.IsPelldefMathlib.NumberTheory.PellMatiyasevic, predicate

Wording

x is a Pell (from the name)

English

Let $x$ be an element of $\mathrm{Zsqrtd}$ applied to $d$. Then we can say that $x$ is a Pell.

Pell.azdefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

no wording

English

Let $a$ be a natural number. Then $\operatorname{az}$ applied to $a$ is an integer defined as $a$.

Pell.pelldefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

the Pell of a1 and x (from the name)

English

Assume that $1 < a$. Let $x$ be a natural number. Then the Pell of $a_{1}$ and $x$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Pell\_\_pell\_\_\_f}$ applied to $a_{1}$.

Pell.pellZddefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

no wording

English

Assume that $1 < a$. Let $n$ be a natural number. Then $\operatorname{pellZd}$ applied to $a_{1}$ and $n$ is an element of $\mathrm{Zsqrtd}$ applied to $\mathrm{\_private\_\_Mathlib\_\_NumberTheory\_\_PellMatiyasevic\_\_0\_\_Pell\_\_d}$ applied to $a_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{xn}$ applied to $a_{1}$ and $n$ and $\operatorname{yn}$ applied to $a_{1}$ and $n$.

Pell.xndefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

no wording

English

Assume that $1 < a$. Let $n$ be a natural number. Then $\operatorname{xn}$ applied to $a_{1}$ and $n$ is a natural number defined as the first element of the Pell of $a_{1}$ and $n$.

Pell.xzdefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

no wording

English

Assume that $1 < a$. Let $n$ be a natural number. Then $\operatorname{xz}$ applied to $a_{1}$ and $n$ is an integer defined as $\operatorname{xn}$ applied to $a_{1}$ and $n$.

Pell.yndefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

no wording

English

Assume that $1 < a$. Let $n$ be a natural number. Then $\operatorname{yn}$ applied to $a_{1}$ and $n$ is a natural number defined as the second element of the Pell of $a_{1}$ and $n$.

Pell.yzdefMathlib.NumberTheory.PellMatiyasevic, function or constant

Wording

no wording

English

Assume that $1 < a$. Let $n$ be a natural number. Then $\operatorname{yz}$ applied to $a_{1}$ and $n$ is an integer defined as $\operatorname{yn}$ applied to $a_{1}$ and $n$.

Mathlib.NumberTheory.PrimeCounting

Nat.primeCountingdefMathlib.NumberTheory.PrimeCounting, function or constant

Wording

the prime counting of n (from the name)

English

Let $n$ be a natural number. Then the prime counting of $n$ is a natural number defined as the prime counting of $n + 1$.

Nat.primeCounting'defMathlib.NumberTheory.PrimeCounting, function or constant

Wording

the prime counting of x (from the name)

English

Let $x$ be a natural number. Then the prime counting of $x$ is a natural number defined as the count of the proposition that $\mathrm{prime}$ and $x$.

Nat.primesBelowdefMathlib.NumberTheory.PrimeCounting, function or constant

Wording

no wording

English

Let $n$ be an element of $\Natural$. Then $\operatorname{primesBelow}$ applied to $n$ is a finite set of $\Natural$ defined as $\FinsetFilter {p}{\mathrm{prime} (p)}{\FinsetrangeMACRoN {n}}$.

Nat.primesLEdefMathlib.NumberTheory.PrimeCounting, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{primesLE}$ applied to $n$ is a finite set of $\Natural$ defined as $\operatorname{primesBelow}$ applied to $n + 1$.

Mathlib.NumberTheory.Primorial

primorialdefMathlib.NumberTheory.Primorial, function or constant

Wording

no wording

English

Let $n$ be an element of $\Natural$. Then $\mathrm{primorial}$ applied to $n$ is an element of $\Natural$ defined as $\FinsetProd {(\FinsetFilter {p}{\mathrm{prime} (p)}{\FinsetrangeMACRoN {(n + 1)}})}{p_{1}}{p_{1}}$.

Mathlib.NumberTheory.PythagoreanTriples

PythagoreanTripledefMathlib.NumberTheory.PythagoreanTriples, predicate

Wording

no wording

English

Let $x$, $y$ and $z$ be integers. Then $\mathrm{PythagoreanTriple}$ holds for $x$, $y$ and $z$, if $x \times x + y \times y = z \times z$.

PythagoreanTriple.IsClassifieddefMathlib.NumberTheory.PythagoreanTriples, predicate

Wording

h is classified (from the name)

English

Assume that $\mathrm{PythagoreanTriple}$ holds for $x$, $y$ and $z$. Then $h$ is classified, if there exist integers $k$, $m$ and $n$, such that $x = k \times (m ^ {2}- n ^ {2})$ and $y = k \times (2 \times m \times n)$ or $x = k \times (2 \times m \times n)$ and $y = k \times (m ^ {2}- n ^ {2})$ and $\operatorname{gcd} (m , n)= 1$.

PythagoreanTriple.IsPrimitiveClassifieddefMathlib.NumberTheory.PythagoreanTriples, predicate

Wording

no wording

English

Assume that $\mathrm{PythagoreanTriple}$ holds for $x$, $y$ and $z$. Then $\operatorname{IsPrimitiveClassified}$ holds for $h$, if there exist elements $m$ and $n$ of $\Integer$, such that $x = m ^ {2}- n ^ {2}$ and $y = 2 \times m \times n$ or $x = 2 \times m \times n$ and $y = m ^ {2}- n ^ {2}$, $\operatorname{gcd} (m , n)= 1$ and $\HModhModMACRoF {m}{2}= 0$ and $\HModhModMACRoF {n}{2}= 1$ or $\HModhModMACRoF {m}{2}= 1$ and $\HModhModMACRoF {n}{2}= 0$.

circleEquivGendefMathlib.NumberTheory.PythagoreanTriples, function or constant

Wording

the circle equivalence generator of hk (from the name)

English

Assume that for all elements $x_{1}$ of $K$, $1 + x_{1} ^ {2}\neq 0$. Then the circle equivalence generator of $\mathrm{hk}$ is an equivalence from $K$ to $\SubtypeSet {p}{\mathrm{and} (\EqtMACRoH {(\ProdfstMACRoZ {p}^ {2}+ \ProdsndMACRoAA {p}^ {2})}{1}, \mathrm{Neq} (\ProdsndMACRoAA {p}, \operatorname{neg} (1)))}$.

Mathlib.NumberTheory.RamificationInertia.Galois

Ideal.inertiaDegIndefMathlib.NumberTheory.RamificationInertia.Galois, function or constant

Wording

no wording

English

Let $p$ be an ideal of $A$. Let $B$ be a set. Then $\operatorname{inertiaDegIn}$ applied to $p$ and $B$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that there exists an ideal $P$ of $B$, such that $P$ is prime and $\operatorname{LiesOver}$ holds for $P$ and $p$, the function that maps $h$ to the inertia degree of $\operatorname{choose}$ applied to $h$ and $A$ and the function that maps $h_{1}$ to $0$.

Ideal.ramificationIdxIndefMathlib.NumberTheory.RamificationInertia.Galois, function or constant

Wording

no wording

English

Let $p$ be an ideal of $A$. Let $B$ be a set. Then $\operatorname{ramificationIdxIn}$ applied to $p$ and $B$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that there exists an ideal $P$ of $B$, such that $P$ is prime and $\operatorname{LiesOver}$ holds for $P$ and $p$, the function that maps $h$ to the ramification index of $\operatorname{choose}$ applied to $h$ and $A$ and the function that maps $h_{1}$ to $0$.

Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Ideal.IsDecompositionRingclassMathlib.NumberTheory.RamificationInertia.HilbertTheory, predicate

Wording

P is a decomposition ring (from the name)

English

Let $G$ and $R$ be sets. Let $P$ be an ideal of $B$. Then we can say that $P$ is a decomposition ring.

Ideal.IsInertiaRingclassMathlib.NumberTheory.RamificationInertia.HilbertTheory, predicate

Wording

P is a inertia ring (from the name)

English

Let $G$ and $R$ be sets. Let $P$ be an ideal of $B$. Then we can say that $P$ is an inertia ring.

IsDecompositionFieldclassMathlib.NumberTheory.RamificationInertia.HilbertTheory, predicate

Wording

P is a decomposition field (from the name)

English

Let $K$, $L$ and $D$ be sets. Let $P$ be an ideal of $B$. Then we can say that $P$ is a decomposition field.

IsDecompositionField.ringEquivdefMathlib.NumberTheory.RamificationInertia.HilbertTheory, function or constant

Wording

the ring isomorphism of P (from the name)

English

Let $K$, $L$, $D$ and $\mathrm{D'}$ be sets. Let $P$ be an ideal of $B$. Then the ring isomorphism of $P$ is a ring isomorphism of $D$ and $\mathrm{D'}$ defined as the ring isomorphism of $\mathrm{D'}$ and $L$.

IsInertiaFieldclassMathlib.NumberTheory.RamificationInertia.HilbertTheory, predicate

Wording

P is a inertia field (from the name)

English

Let $K$, $L$ and $E$ be sets. Let $P$ be an ideal of $B$. Then we can say that $P$ is an inertia field.

IsInertiaField.ringEquivdefMathlib.NumberTheory.RamificationInertia.HilbertTheory, function or constant

Wording

the ring isomorphism of P (from the name)

English

Let $K$, $L$, $E$ and $\mathrm{E'}$ be sets. Let $P$ be an ideal of $B$. Then the ring isomorphism of $P$ is a ring isomorphism of $E$ and $\mathrm{E'}$ defined as the ring isomorphism of $\mathrm{E'}$ and $L$.

Mathlib.NumberTheory.RamificationInertia.Ramification

Ideal.ramificationIdx'defMathlib.NumberTheory.RamificationInertia.Ramification, function or constant

Wording

the ramification index of P over p (from the docstring)

English

Let $p$ be an ideal of $R$. Let $P$ be an ideal of $S$. Then the ramification index of $P$ over $p$ is a natural number defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that the map of the algebra map of $R$ and $S$ and $p$ is less than or equal to $P ^ {n}$.

Mathlib.NumberTheory.RatFunc.Ostrowski

RatFunc.uniformizingPolynomialdefMathlib.NumberTheory.RatFunc.Ostrowski, function or constant

Wording

no wording

English

Assume that $v (\operatorname{X})\leq 1$. Then $\operatorname{uniformizingPolynomial}$ applied to $\mathrm{hle}$ is a polynomial of $K$.

RatFunc.valuationIdealdefMathlib.NumberTheory.RatFunc.Ostrowski, function or constant

Wording

the maximal ideal of hle (from the docstring)

English

Assume that $v (\operatorname{X})\leq 1$. Then the maximal ideal of $\mathrm{hle}$ is a height one spectrum of the set of polynomials of $K$.

Mathlib.NumberTheory.Rayleigh

beattySeqdefMathlib.NumberTheory.Rayleigh, function or constant

Wording

the Beatty sequence of r and x (from the name)

English

Let $r$ be a real number. Let $x$ be an integer. Then the Beatty sequence of $r$ and $x$ is an integer defined as the floor of $x \times r$.

beattySeq'defMathlib.NumberTheory.Rayleigh, function or constant

Wording

the Beatty sequence of r and x (from the name)

English

Let $r$ be a real number. Let $x$ be an integer. Then the Beatty sequence of $r$ and $x$ is an integer defined as $\operatorname{ceil} (x \times r)- 1$.

Mathlib.NumberTheory.Real.GoldenRatio

Real.fibRecdefMathlib.NumberTheory.Real.GoldenRatio, function or constant

Wording

the recurrence relation satisfied by the Fibonacci sequence (from the docstring)

English

The recurrence relation satisfied by the Fibonacci sequence is a linear recurrence of $x$ defined as $\operatorname{mk}$ applied to $2$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$.

Real.goldenConjdefMathlib.NumberTheory.Real.GoldenRatio, function or constant

Wording

the conjugate of the golden ratio (from the docstring)

English

The conjugate of the golden ratio is a real number defined as the quotient of the difference between $1$ and the square root of $5$ and $2$.

Real.goldenRatiodefMathlib.NumberTheory.Real.GoldenRatio, function or constant

Wording

the golden ratio (from the docstring)

English

The golden ratio is a real number defined as the quotient of the sum of $1$ and the square root of $5$ and $2$.

Mathlib.NumberTheory.Real.Irrational

IrrationaldefMathlib.NumberTheory.Real.Irrational, predicate

Wording

x is irrational (from the docstring)

English

Let $x$ be a real number. Then $x$ is irrational, if $x$ is not an element of the range of $\operatorname{cast}$.

Mathlib.NumberTheory.SelbergSieve

BoundingSievestructureMathlib.NumberTheory.SelbergSieve, type

Wording

no wording

English

The elements of $\mathrm{BoundingSieve}$ are a basic type.

BoundingSieve.IsUpperMoebiusdefMathlib.NumberTheory.SelbergSieve, predicate

Wording

no wording

English

Let $\mathrm{muPlus}$ be a function from elements of $\Natural$ to elements of $\Real$. Then $\operatorname{IsUpperMoebius}$ holds for $\mathrm{muPlus}$, if for all elements $n$ of $\Natural$, $\iteMACRoG {\mathrm{Eq} (n , 1)}{1}{0}\leq \FinsetSum {\operatorname{divisors} (n)}{d}{\mathrm{muPlus} (d)}$.

BoundingSieve.errSumdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the error term in the upper bound on muPlus (from the docstring)

English

Let $\mathrm{muPlus}$ be a function from elements of $\Natural$ to elements of $\Real$. Then the error term in the upper bound on $\mathrm{muPlus}$ is an element of $\Real$ defined as $\FinsetSum {\operatorname{divisors} (\operatorname{prodPrimes} (s))}{d}{(\mathrm{abs} (\mathrm{muPlus} (d))\times \mathrm{abs} (\operatorname{rem} (d)))}$.

BoundingSieve.lambdaSquareddefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

no wording

English

Let $\mathrm{weights}$ be a function from elements of $\Natural$ to elements of $\Real$. Let $x$ be an element of $\Natural$. Then $\operatorname{lambdaSquared}$ applied to $\mathrm{weights}$ and $x$ is an element of $\Real$ defined as $\FinsetSum {\operatorname{divisors} (x)}{d_{1}}{(\FinsetSum {\operatorname{divisors} (x)}{d_{2}}{(\iteMACRoG {\mathrm{Eq} (x , \NatlcmMACRoX {d_{1}}{d_{2}})}{(\mathrm{weights} (d_{1})\times \mathrm{weights} (d_{2}))}{0})})}$.

BoundingSieve.mainSumdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the main term in the upper bound on muPlus (from the docstring)

English

Let $\mathrm{muPlus}$ be a function from elements of $\Natural$ to elements of $\Real$. Then the main term in the upper bound on $\mathrm{muPlus}$ is an element of $\Real$ defined as $\FinsetSum {\operatorname{divisors} (\operatorname{prodPrimes} (s))}{d}{(\mathrm{muPlus} (d)\times \operatorname{nu} (s , d))}$.

BoundingSieve.multSumdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

no wording

English

Let $d$ be an element of $\Natural$. Then $\operatorname{multSum}$ applied to $d$ is an element of $\Real$ defined as $\FinsetSum {\operatorname{support} (s)}{n}{(\iteMACRoG {(\divides {d}{n})}{\operatorname{weights} (s , n)}{0})}$.

BoundingSieve.nudefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{BoundingSieve}$. Then $\operatorname{nu}$ applied to $\mathrm{self}$ is an arithmetic function of $\Real$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

BoundingSieve.prodPrimesdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the product prime of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{BoundingSieve}$. Then the product prime of $\mathrm{self}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

BoundingSieve.remdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

no wording

English

Let $d$ be a natural number. Then $\operatorname{rem}$ applied to $d$ is a real number defined as the difference between $\operatorname{multSum}$ applied to $d$ and the product of $\operatorname{nu}$ applied to $s$ and $d$ and the total mass of $s$.

BoundingSieve.selbergTermsdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

no wording

English

$\operatorname{selbergTerms}$ is an arithmetic function of $\Real$ defined as $\operatorname{pmul}$ applied to $\operatorname{nu}$ applied to $s$ and the product prime factor of the function that maps $p$ to $\operatorname{inv}$ applied to $1 - \operatorname{nu} (s , p)$.

BoundingSieve.siftedSumdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the sifted sum (from the name)

English

The sifted sum is an element of $\Real$ defined as $\FinsetSum {\operatorname{support} (s)}{d}{(\iteMACRoG {(\NatCoprimeMACRoC {\operatorname{prodPrimes} (s)}{d})}{\operatorname{weights} (s , d)}{0})}$.

BoundingSieve.supportdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the support of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{BoundingSieve}$. Then the support of $\mathrm{self}$ is a finite set of $\Natural$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

BoundingSieve.totalMassdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the total mass of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{BoundingSieve}$. Then the total mass of $\mathrm{self}$ is a real number defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

BoundingSieve.weightsdefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{BoundingSieve}$. Let $x$ be a natural number. Then $\operatorname{weights}$ applied to $\mathrm{self}$ and $x$ is a real number defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x$.

SelbergSievestructureMathlib.NumberTheory.SelbergSieve, type

Wording

no wording

English

The elements of $\mathrm{SelbergSieve}$ are a basic type.

SelbergSieve.leveldefMathlib.NumberTheory.SelbergSieve, function or constant

Wording

the level of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{SelbergSieve}$. Then the level of $\mathrm{self}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.NumberTheory.SmoothNumbers

Nat.equivProdNatFactoredNumbersdefMathlib.NumberTheory.SmoothNumbers, function or constant

Wording

the equivalence product natural factored number of hp and hs (from the name)

English

Assume that $p$ is prime. Assume that $p$ is not an element of $s$. Then the equivalence product natural factored number of $\mathrm{hp}$ and $\mathrm{hs}$ is an equivalence from $\mathrm{Prod}$ applied to $\Natural$ and the set of elements of the factored number of $s$ to the set of elements of the factored number of $\operatorname{insert}$ applied to $p$ and $s$.

Nat.equivProdNatSmoothNumbersdefMathlib.NumberTheory.SmoothNumbers, function or constant

Wording

the equivalence product natural smooth number of hp (from the name)

English

Assume that $p$ is prime. Then the equivalence product natural smooth number of $\mathrm{hp}$ is an equivalence from $\mathrm{Prod}$ applied to $\Natural$ and the set of elements of the smooth number of $p$ to the set of elements of the smooth number of $p + 1$.

Nat.factoredNumbersdefMathlib.NumberTheory.SmoothNumbers, function or constant

Wording

the factored number of s (from the name)

English

Let $s$ be a finite set of $\Natural$. Then the factored number of $s$ is an element of $\wp \Natural$ defined as $\operatorname{ofPred}$ applied to the function that maps $m$ to the proposition that $m \neq 0$ and for all natural numbers $p$, if $p$ is an element of the prime factorization of $m$, then $p$ is an element of $s$.

Nat.roughNumbersUpTodefMathlib.NumberTheory.SmoothNumbers, function or constant

Wording

no wording

English

Let $N$ and $k$ be elements of $\Natural$. Then $\operatorname{roughNumbersUpTo}$ applied to $N$ and $k$ is a finite set of $\Natural$ defined as $\FinsetFilter {n}{\mathrm{and} (\mathrm{Neq} (n , 0), \mathrm{not} (\MembershipmemMACRoT {\operatorname{smoothNumbers} (k)}{n}))}{\FinsetrangeMACRoN {(N + 1)}}$.

Nat.smoothNumbersdefMathlib.NumberTheory.SmoothNumbers, function or constant

Wording

the smooth number of n (from the name)

English

Let $n$ be a natural number. Then the smooth number of $n$ is an element of $\wp \Natural$ defined as $\operatorname{ofPred}$ applied to the function that maps $m$ to the proposition that $m \neq 0$ and for all natural numbers $p$, if $p$ is an element of the prime factorization of $m$, then $p < n$.

Nat.smoothNumbersUpTodefMathlib.NumberTheory.SmoothNumbers, function or constant

Wording

no wording

English

Let $N$ and $k$ be elements of $\Natural$. Then $\operatorname{smoothNumbersUpTo}$ applied to $N$ and $k$ is a finite set of $\Natural$ defined as $\FinsetFilter {n}{(\MembershipmemMACRoT {\operatorname{smoothNumbers} (k)}{n})}{\FinsetrangeMACRoN {(N + 1)}}$.

Mathlib.NumberTheory.Transcendental.Liouville.Basic

LiouvilledefMathlib.NumberTheory.Transcendental.Liouville.Basic, predicate

Wording

x is a Liouville (from the name)

English

Let $x$ be a real number. Then $x$ is a Liouville, if for all natural numbers $n$, there exist integers $a$ and $b$, such that $1 < b$, $x \neq \frac{ a}{b}$ and the absolute value of $x - \frac{ a}{b}$ is less than $\frac{ 1}{b ^ {n}}$.

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

LiouvilleNumber.partialSumdefMathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber, function or constant

Wording

the partial sum of m and k (from the name)

English

Let $m$ be a real number. Let $k$ be a natural number. Then the partial sum of $m$ and $k$ is a real number defined as $\FinsetSum {\FinsetrangeMACRoN {(k + 1)}}{i}{(\frac{ 1}{m ^ {i !}})}$.

LiouvilleNumber.remainderdefMathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber, function or constant

Wording

the remainder of m and k (from the name)

English

Let $m$ be a real number. Let $k$ be a natural number. Then the remainder of $m$ and $k$ is a real number defined as the sum of the function that maps $i$ to $\frac{ 1}{m ^ {(i + (k + 1))!}}$ and $\operatorname{unconditional}$ applied to $\Natural$.

liouvilleNumberdefMathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber, function or constant

Wording

the Liouville number of m (from the name)

English

Let $m$ be a real number. Then the Liouville number of $m$ is a real number defined as the sum of the function that maps $i$ to $\frac{ 1}{m ^ {i !}}$ and $\operatorname{unconditional}$ applied to $\Natural$.

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

LiouvilleWithdefMathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith, predicate

Wording

no wording

English

Let $p$ and $x$ be real numbers. Then $\mathrm{LiouvilleWith}$ holds for $p$ and $x$, if there exists a real number $C$, such that $\operatorname{Frequently}$ holds for the function that maps $n$ to the proposition that there exists an integer $m$, such that $x \neq \frac{ m}{n}$ and the absolute value of $x - \frac{ m}{n}$ is less than $\frac{ C}{n ^ {p}}$ and $\operatorname{atTop}$.

Mathlib.NumberTheory.TsumDivisorsAntidiagonal

divisorsAntidiagonalFactorsdefMathlib.NumberTheory.TsumDivisorsAntidiagonal, function or constant

Wording

the divisor antidiagonal factor of n and x (from the name)

English

Let $n$ be an element of $\PNatMACRoAD$. Let $x$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{divisorsAntidiagonal} (\operatorname{val} (n))}{x_{1}})}$. Then the divisor antidiagonal factor of $n$ and $x$ is an element of $\mathrm{Prod}$ applied to $\PNatMACRoAD$ and $\PNatMACRoAD$ defined as $\ProdmkMACRoU {\ProdfstMACRoZ {x}}{\ProdsndMACRoAA {x}}$.

sigmaAntidiagonalEquivProddefMathlib.NumberTheory.TsumDivisorsAntidiagonal, function or constant

Wording

the sigma antidiagonal equivalence product (from the name)

English

The sigma antidiagonal equivalence product is an element of $\EquivMACRoAE {\Sigma (\lambda n . \SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{divisorsAntidiagonal} (\operatorname{val} (n))}{x})})}{\mathrm{Prod} (\PNatMACRoAD , \PNatMACRoAD)}$.

Mathlib.NumberTheory.WellApproximable

addWellApproximabledefMathlib.NumberTheory.WellApproximable, function or constant

Wording

no wording

English

Let $A$ be a set. Let $x_{1}$ be a function from natural numbers to real numbers. Then $\mathrm{addWellApproximable}$ applied to $A$ and $x_{1}$ is an element of $\wp A$ defined as $\operatorname{blimsup}$ applied to the function that maps $n$ to $\mathrm{approxAddOrderOf}$ applied to $A$, $n$ and $x_{1}$ applied to $n$, $\operatorname{atTop}$ and the function that maps $n_{1}$ to $\mathrm{Lt} (0 , n_{1})$.

approxAddOrderOfdefMathlib.NumberTheory.WellApproximable, function or constant

Wording

no wording

English

Let $A$ be a set. Let $n$ be a natural number. Let $x_{1}$ be a real number. Then $\mathrm{approxAddOrderOf}$ applied to $A$, $n$ and $x_{1}$ is an element of $\wp A$ defined as the thickening of $x_{1}$ and $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the additive order of $y$ is equal to $n$.

approxOrderOfdefMathlib.NumberTheory.WellApproximable, function or constant

Wording

no wording

English

Let $A$ be a set. Let $n$ be a natural number. Let $x_{1}$ be a real number. Then $\mathrm{approxOrderOf}$ applied to $A$, $n$ and $x_{1}$ is an element of $\wp A$ defined as the thickening of $x_{1}$ and $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the order of $y$ is equal to $n$.

wellApproximabledefMathlib.NumberTheory.WellApproximable, function or constant

Wording

no wording

English

Let $A$ be a set. Let $x_{1}$ be a function from natural numbers to real numbers. Then $\mathrm{wellApproximable}$ applied to $A$ and $x_{1}$ is an element of $\wp A$ defined as $\operatorname{blimsup}$ applied to the function that maps $n$ to $\mathrm{approxOrderOf}$ applied to $A$, $n$ and $x_{1}$ applied to $n$, $\operatorname{atTop}$ and the function that maps $n_{1}$ to $\mathrm{Lt} (0 , n_{1})$.

Mathlib.NumberTheory.ZetaValues

bernoulliFourierCoeffdefMathlib.NumberTheory.ZetaValues, function or constant

Wording

the Bernoulli Fourier coefficient of k and n (from the name)

English

Let $k$ be a natural number. Let $n$ be an integer. Then the Bernoulli Fourier coefficient of $k$ and $n$ is a complex.

bernoulliFundefMathlib.NumberTheory.ZetaValues, function or constant

Wording

the function of k and x (from the docstring)

English

Let $k$ be a natural number. Let $x$ be a real number. Then the function of $k$ and $x$ is a real number defined as the evaluation of $x$ and the map of the algebra map of $\Rational$ and $\Real$ and $\operatorname{bernoulli}$ applied to $k$.

periodizedBernoullidefMathlib.NumberTheory.ZetaValues, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $x$ be a unit circle. Then $\mathrm{periodizedBernoulli}$ applied to $k$ and $x$ is a real number defined as $\operatorname{liftIco}$ applied to $1$, $0$, $\mathrm{bernoulliFun}$ applied to $k$ and $x$.