ADEInequality.AdefMathlib.NumberTheory.ADEInequality, function or constantEnglish
Let $r$ be a positive natural number. Then $\operatorname{A}$ applied to $r$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{A'}$ applied to $1$ and $r$.
ADEInequality.A'defMathlib.NumberTheory.ADEInequality, function or constantEnglish
Let $q$ and $r$ be positive natural numbers. Then $\operatorname{A'}$ applied to $q$ and $r$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{insert}$ applied to $1$ and $\operatorname{insert}$ applied to $q$ and $\operatorname{singleton}$ applied to $r$.
ADEInequality.AdmissibledefMathlib.NumberTheory.ADEInequality, predicateWording
pqr is admissible (from the name)
English
Let $\mathrm{pqr}$ be a multiset of $\PNatMACRoAD$. Then $\mathrm{pqr}$ is admissible, if there exists a positive natural number $q$ such that there exists a positive natural number $r$ such that $\EqtMACRoH {\operatorname{A'} (q , r)}{\mathrm{pqr}}$, there exists a positive natural number $r_{1}$ such that $\EqtMACRoH {\operatorname{D'} (r_{1})}{\mathrm{pqr}}$, $\EqtMACRoH {\operatorname{E'} (3)}{\mathrm{pqr}}$, $\EqtMACRoH {\operatorname{E'} (4)}{\mathrm{pqr}}$ or $\EqtMACRoH {\operatorname{E'} (5)}{\mathrm{pqr}}$.
ADEInequality.D'defMathlib.NumberTheory.ADEInequality, function or constantEnglish
Let $r$ be a positive natural number. Then $\operatorname{D'}$ applied to $r$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{insert}$ applied to $2$ and $\operatorname{insert}$ applied to $2$ and $\operatorname{singleton}$ applied to $r$.
ADEInequality.E'defMathlib.NumberTheory.ADEInequality, function or constantEnglish
Let $r$ be a positive natural number. Then $\operatorname{E'}$ applied to $r$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{insert}$ applied to $2$ and $\operatorname{insert}$ applied to $3$ and $\operatorname{singleton}$ applied to $r$.
ADEInequality.E6defMathlib.NumberTheory.ADEInequality, function or constantEnglish
$\operatorname{E6}$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{E'}$ applied to $3$.
ADEInequality.E7defMathlib.NumberTheory.ADEInequality, function or constantEnglish
$\operatorname{E7}$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{E'}$ applied to $4$.
ADEInequality.E8defMathlib.NumberTheory.ADEInequality, function or constantEnglish
$\operatorname{E8}$ is a multiset of $\PNatMACRoAD$ defined as $\operatorname{E'}$ applied to $5$.
ADEInequality.sumInvdefMathlib.NumberTheory.ADEInequality, function or constantWording
the sum inverse of pqr (from the name)
English
Let $\mathrm{pqr}$ be a multiset of $\PNatMACRoAD$. Then the sum inverse of $\mathrm{pqr}$ is a rational number defined as the sum of the map of the function that maps $x$ to $\operatorname{inv}$ applied to the value of $x$ and $\mathrm{pqr}$.
Nat.IsAlmostPrimedefMathlib.NumberTheory.AlmostPrime, predicateEnglish
Let $k$ and $n$ be natural numbers. Then $\operatorname{IsAlmostPrime}$ holds for $k$ and $n$, if $n \neq 0$ and $\operatorname{cardFactors} (n)= k$.
Nat.IsAtMostAlmostPrimedefMathlib.NumberTheory.AlmostPrime, predicateEnglish
Let $k$ and $n$ be natural numbers. Then $\operatorname{IsAtMostAlmostPrime}$ holds for $k$ and $n$, if $n \neq 0$ and $\operatorname{cardFactors} (n)\leq k$.
Nat.IsSemiprimedefMathlib.NumberTheory.AlmostPrime, predicateEnglish
Let $n$ be a natural number. Then $\operatorname{IsSemiprime}$ holds for $n$, if $\operatorname{IsAlmostPrime}$ holds for $2$ and $n$.
ArithmeticFunction.carmichaeldefMathlib.NumberTheory.ArithmeticFunction.Carmichael, function or constantWording
the Carmichael function (from the docstring)
English
The Carmichael function is an arithmetic function of $\Natural$.
ArithmeticFunctiondefMathlib.NumberTheory.ArithmeticFunction.Defs, typeWording
arithmetic function of R (from the name)
English
Let $R$ be a set. Then an arithmetic function of $R$ is an element of the function that maps $R$ to the set of zero homomorphisms of $\Natural$ and $R$.
ArithmeticFunction.IsMultiplicativedefMathlib.NumberTheory.ArithmeticFunction.Defs, predicateWording
f is multiplicative (from the name)
English
Let $f$ be an arithmetic function of $R$. Then $f$ is multiplicative, if $\EqtMACRoH {f (1)}{1}$ and for all natural numbers $m$, for all natural numbers $n$, if $m$ and $n$ are coprime, then $\EqtMACRoH {f (m \times n)}{f (m)\times f (n)}$.
ArithmeticFunction.dirichletInversedefMathlib.NumberTheory.ArithmeticFunction.Defs, function or constantWording
the Dirichlet inverse of f and hf (from the name)
English
Let $f$ be a function from natural numbers to elements of $R$ such that $f$ applied to $1$ is invertible. Then the Dirichlet inverse of $f$ and $\mathrm{hf}$ is an arithmetic function of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{dirichletInverseFun}$ applied to $f$ and $\mathrm{ArithmeticFunction\_\_dirichletInverseFun\_apply\_zero}$ applied to $f$ and $\mathrm{hf}$.
ArithmeticFunction.dirichletInverseFundefMathlib.NumberTheory.ArithmeticFunction.Defs, function or constantWording
the Dirichlet inverse function of f and n (from the name)
English
Let $f$ be a function from natural numbers to elements of $R$ such that $f$ applied to $1$ is invertible. Let $n$ be a natural number. Then the Dirichlet inverse function of $f$ and $n$ is an element of $R$.
ArithmeticFunction.natToArithmeticFunctiondefMathlib.NumberTheory.ArithmeticFunction.Defs, function or constantEnglish
Let $x_{1}$ be an arithmetic function of $\Natural$. Then $\operatorname{natToArithmeticFunction}$ applied to $x_{1}$ is an arithmetic function of $R$.
ArithmeticFunction.ofIntdefMathlib.NumberTheory.ArithmeticFunction.Defs, function or constantWording
the arithmetic function of x1 (from the name)
English
Let $x_{1}$ be an arithmetic function of $\Integer$. Then the arithmetic function of $x_{1}$ is an arithmetic function of $R$.
ArithmeticFunction.eulerProductdefMathlib.NumberTheory.ArithmeticFunction.LFunction, function or constantWording
the Euler product of f (from the docstring)
English
Let $f$ be a function from elements of $x$ to arithmetic functions of $R$. Then the Euler product of $f$ is an arithmetic function of $R$ defined as $\mathrm{tprod}$ applied to the function that maps $i$ to $f$ applied to $i$ and $\operatorname{unconditional}$ applied to $x$.
ArithmeticFunction.ofPowerSeriesdefMathlib.NumberTheory.ArithmeticFunction.LFunction, function or constantWording
the arithmetic function corresponding to the Dirichlet series of q (from the docstring)
English
Let $q$ be a natural number. Then the arithmetic function corresponding to the Dirichlet series of $q$ is an algebra homomorphism of the set of power series of $R$ and the set of arithmetic functions of $R$.
ArithmeticFunction.liouvilledefMathlib.NumberTheory.ArithmeticFunction.Liouville, function or constantWording
the Liouville function (from the docstring)
English
The Liouville function is an arithmetic function of $\Integer$.
ArithmeticFunction.bigproddvddefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantEnglish
generation took over the time limit
ArithmeticFunction.cardDistinctFactorsdefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantWording
the cardinality distinct factor (from the name)
English
The cardinality distinct factor is an arithmetic function of $\Natural$.
ArithmeticFunction.cardFactorsdefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantWording
the cardinality factor (from the name)
English
The cardinality factor is an arithmetic function of $\Natural$.
ArithmeticFunction.iddefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantWording
the identity (from the name)
English
The identity is an arithmetic function of $\Natural$.
ArithmeticFunction.powdefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantWording
the power of k (from the name)
English
Let $k$ be a natural number. Then the power of $k$ is an arithmetic function of $\Natural$ defined as $\operatorname{ppow}$ applied to the identity and $k$.
ArithmeticFunction.prodPrimeFactorsdefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantWording
the product prime factor of f (from the name)
English
Let $f$ be a function from natural numbers to elements of $R$. Then the product prime factor of $f$ is an arithmetic function of $R$.
ArithmeticFunction.sigmadefMathlib.NumberTheory.ArithmeticFunction.Misc, function or constantWording
the sigma of k (from the name)
English
Let $k$ be a natural number. Then the sigma of $k$ is an arithmetic function of $\Natural$.
ArithmeticFunction.moebiusdefMathlib.NumberTheory.ArithmeticFunction.Moebius, function or constantEnglish
$\operatorname{moebius}$ is an arithmetic function of $\Integer$.
ArithmeticFunction.zetaUnitdefMathlib.NumberTheory.ArithmeticFunction.Moebius, function or constantWording
the Zeta unit (from the name)
English
The Zeta unit is a unit of the set of arithmetic functions of $R$.
ArithmeticFunction.logdefMathlib.NumberTheory.ArithmeticFunction.VonMangoldt, function or constantWording
the logarithm (from the name)
English
The logarithm is an arithmetic function of $\Real$.
ArithmeticFunction.vonMangoldtdefMathlib.NumberTheory.ArithmeticFunction.VonMangoldt, function or constantEnglish
$\operatorname{vonMangoldt}$ is an arithmetic function of $\Real$.
ArithmeticFunction.pdivdefMathlib.NumberTheory.ArithmeticFunction.Zeta, function or constantEnglish
Let $f$ and $g$ be arithmetic functions of $R$. Then $\operatorname{pdiv}$ applied to $f$ and $g$ is an arithmetic function of $R$.
ArithmeticFunction.pmuldefMathlib.NumberTheory.ArithmeticFunction.Zeta, function or constantEnglish
Let $f$ and $g$ be arithmetic functions of $R$. Then $\operatorname{pmul}$ applied to $f$ and $g$ is an arithmetic function of $R$.
ArithmeticFunction.ppowdefMathlib.NumberTheory.ArithmeticFunction.Zeta, function or constantEnglish
Let $f$ be an arithmetic function of $R$. Let $k$ be a natural number. Then $\operatorname{ppow}$ applied to $f$ and $k$ is an arithmetic function of $R$.
ArithmeticFunction.zetadefMathlib.NumberTheory.ArithmeticFunction.Zeta, function or constantWording
the Zeta (from the name)
English
The Zeta is an arithmetic function of $\Natural$.
bernoullidefMathlib.NumberTheory.Bernoulli, function or constantEnglish
Let $n$ be a natural number. Then $\mathrm{bernoulli}$ applied to $n$ is a rational number defined as $\operatorname{neg} (1)^ {n}\times \mathrm{bernoulli'} (n)$.
bernoulli'defMathlib.NumberTheory.Bernoulli, function or constantEnglish
Let $n$ be a natural number. Then $\mathrm{bernoulli'}$ applied to $n$ is a rational number.
bernoulli'PowerSeriesdefMathlib.NumberTheory.Bernoulli, function or constantWording
the exponential generating function for the Bernoulli numbers of A (from the docstring)
English
Let $A$ be a set. Then the exponential generating function for the Bernoulli numbers of $A$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{algebraMap}$ applied to $\Rational$, $A$ and $\frac{ \mathrm{bernoulli'} (n)}{n !}$.
bernoulliPowerSeriesdefMathlib.NumberTheory.Bernoulli, function or constantWording
the exponential generating function for the Bernoulli numbers of A (from the docstring)
English
Let $A$ be a set. Then the exponential generating function for the Bernoulli numbers of $A$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{algebraMap}$ applied to $\Rational$, $A$ and $\frac{ \mathrm{bernoulli} (n)}{n !}$.
Polynomial.bernoullidefMathlib.NumberTheory.BernoulliPolynomials, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{bernoulli}$ applied to $n$ is a polynomial of $\Rational$ defined as $\FinsetSum {\FinsetrangeMACRoN {(n + 1)}}{i}{\operatorname{monomial} (n - i , \mathrm{bernoulli} (i)\times \operatorname{choose} (n , i))}$.
Nat.IsCarmichaeldefMathlib.NumberTheory.CarmichaelNumber, predicateEnglish
Let $n$ be a natural number. Then $\operatorname{IsCarmichael}$ holds for $n$, if $2 < n$, $n$ is not prime and for all natural numbers $b$, if $b$ and $n$ are coprime, then $\operatorname{ProbablePrime}$ holds for $n$ and $b$.
Chebyshev.psidefMathlib.NumberTheory.Chebyshev, function or constantEnglish
Let $x$ be an element of $\Real$. Then $\operatorname{psi}$ applied to $x$ is an element of $\Real$ defined as $\FinsetSum {(\FinsetIocMACRoAI {0}{\operatorname{floor} (x)})}{n}{\operatorname{vonMangoldt} (n)}$.
Chebyshev.thetadefMathlib.NumberTheory.Chebyshev, function or constantWording
the sum of x (from the docstring)
English
Let $x$ be an element of $\Real$. Then the sum of $x$ is an element of $\Real$ defined as $\FinsetSum {(\FinsetFilter {p}{\mathrm{prime} (p)}{(\FinsetIocMACRoAI {0}{\operatorname{floor} (x)})})}{p_{1}}{\operatorname{log} (p_{1})}$.
Nat.lcmUptodefMathlib.NumberTheory.Chebyshev, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{lcmUpto}$ applied to $n$ is a natural number defined as the least common multiple of $\FinsetIccMACRoAH {1}{n}$ and $\mathrm{id}$.
AbsoluteValue.absIsAdmissibledefMathlib.NumberTheory.ClassNumber.AdmissibleAbs, function or constantWording
the admissible absolute value (from the docstring)
English
The admissible absolute value is an element of $\operatorname{IsAdmissible}$ applied to the absolute value defined as $\operatorname{mk}$ applied to $\mathrm{AbsoluteValue\_\_abs\_isEuclidean}$, the function that maps $x$ to $\operatorname{ceil}$ applied to $\frac{ 1}{x}$ and the function that maps $n$, $x_{1}$, $h$, $x_{2}$ and $\mathrm{hb}$ to $\mathrm{AbsoluteValue\_\_exists\_partition\_int}$ applied to $n$, $h$ and $\mathrm{hb}$.
AbsoluteValue.IsAdmissiblestructureMathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue, typeEnglish
Let $\mathrm{abv}$ be an absolute value of $R$ and $\Integer$. Then the elements of $\operatorname{IsAdmissible}$ applied to $\mathrm{abv}$ are a basic type.
AbsoluteValue.IsAdmissible.carddefMathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue, function or constantWording
the cardinality of self and x1 (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{IsAdmissible}$ applied to $\mathrm{abv}$. Let $x_{1}$ be a real number. Then the cardinality of $\mathrm{self}$ and $x_{1}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.
Polynomial.cardPowDegreeIsAdmissibledefMathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree, function or constantWording
the admissible absolute value (from the docstring)
English
The admissible absolute value is an element of $\operatorname{IsAdmissible}$ applied to the cardinality power degree defined as $\operatorname{mk}$ applied to $\mathrm{Polynomial\_\_cardPowDegree\_isEuclidean}$, the function that maps $x_{2}$ to the exponentiation of the cardinality of $\mathrm{Fq}$ to $\operatorname{ceil}$ applied to the quotient of $\operatorname{neg}$ applied to the logarithm of $x_{2}$ and the logarithm of the cardinality of $\mathrm{Fq}$ and the function that maps $n$, $x_{3}$, $h$, $x_{4}$ and $\mathrm{hb}$ to $\mathrm{Polynomial\_\_exists\_partition\_polynomial}$ applied to $n$, $h$ and $\mathrm{hb}$.
ClassGroup.cardMdefMathlib.NumberTheory.ClassNumber.Finite, function or constantWording
the cardinality of bS and adm (from the name)
English
Let $\mathrm{bS}$ be a basis of $R$ and $S$. Let $\mathrm{adm}$ be an element of $\operatorname{IsAdmissible}$ applied to $\mathrm{abv}$. Then the cardinality of $\mathrm{bS}$ and $\mathrm{adm}$ is a natural number defined as the exponentiation of the cardinality of $\mathrm{adm}$ and the exponentiation of the norm bound of $\mathrm{abv}$ and $\mathrm{bS}$ to the quotient of $\operatorname{neg}$ applied to $1$ and the cardinality of $x_{3}$ to the cardinality of $x_{3}$.
ClassGroup.distinctElemsdefMathlib.NumberTheory.ClassNumber.Finite, function or constantEnglish
Let $\mathrm{bS}$ be a basis of $R$ and $S$. Let $\mathrm{adm}$ be an element of $\operatorname{IsAdmissible}$ applied to $\mathrm{abv}$. Then $\operatorname{distinctElems}$ applied to $\mathrm{bS}$ and $\mathrm{adm}$ is an embedding of $\mathrm{Fin}$ applied to the successor of the cardinality of $\mathrm{bS}$ and $\mathrm{adm}$ and $R$ defined as the composition of the value embedding and the natural embedding of $R$.
ClassGroup.finsetApproxdefMathlib.NumberTheory.ClassNumber.Finite, function or constantEnglish
Let $\mathrm{bS}$ be a basis of $R$ and $S$. Let $\mathrm{adm}$ be an element of $\operatorname{IsAdmissible}$ applied to $\mathrm{abv}$. Then $\operatorname{finsetApprox}$ applied to $\mathrm{bS}$ and $\mathrm{adm}$ is a finite set of $R$ defined as $\operatorname{erase}$ applied to the forward image of the universal set under the function that maps $\mathrm{xy}$ to $\operatorname{distinctElems} (\mathrm{bS} , \mathrm{adm} , \ProdfstMACRoZ {\mathrm{xy}})- \operatorname{distinctElems} (\mathrm{bS} , \mathrm{adm} , \ProdsndMACRoAA {\mathrm{xy}})$ and $0$.
ClassGroup.mkMMemdefMathlib.NumberTheory.ClassNumber.Finite, function or constantWording
the membership of adm and J (from the name)
English
Let $\mathrm{bS}$ be a basis of $R$ and $S$. Let $\mathrm{adm}$ be an element of $\operatorname{IsAdmissible}$ applied to $\mathrm{abv}$. Let $J$ be an element of $\SubtypeSet {J_{1}}{(\MembershipmemMACRoT {J_{1}}{\operatorname{algebraMap} (R , S , \FinsetProd {\operatorname{finsetApprox} (\mathrm{bS} , \mathrm{adm})}{m}{m})})}$. Then the membership of $\mathrm{adm}$ and $J$ is an ideal class group of $S$ defined as $\operatorname{mk0}$ applied to $J$.
ClassGroup.normBounddefMathlib.NumberTheory.ClassNumber.Finite, function or constantWording
the norm bound of abv and bS (from the name)
English
Let $\mathrm{abv}$ be an absolute value of $R$ and $\Integer$. Let $\mathrm{bS}$ be a basis of $R$ and $S$. Then the norm bound of $\mathrm{abv}$ and $\mathrm{bS}$ is an integer.
FunctionField.classNumberdefMathlib.NumberTheory.ClassNumber.FunctionField, function or constantWording
the class number of Fq and F (from the docstring)
English
Let $\mathrm{Fq}$ and $F$ be sets. Then the class number of $\mathrm{Fq}$ and $F$ is an element of $\Natural$ defined as the cardinality of the set of ideal class groups of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ringOfIntegers} (\mathrm{Fq} , F)}{x_{5}})}$.
CyclotomicFielddefMathlib.NumberTheory.Cyclotomic.Basic, typeWording
cyclotomic field of n and K (from the name)
English
Let $n$ be a natural number. Let $K$ be a set. Then a cyclotomic field of $n$ and $K$ is an element of the function that maps $n$ and $K$ to the set of splitting fields of $\operatorname{cyclotomic}$ applied to $n$ and $K$.
CyclotomicRingdefMathlib.NumberTheory.Cyclotomic.Basic, typeWording
cyclotomic ring of A and K (from the name)
English
Let $n$ be a natural number. Let $A$ and $K$ be sets. Then a cyclotomic ring of $A$ and $K$ is an element of the function that maps $n$, $A$ and $K$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{adjoin} (A , \operatorname{ofPred} (\lambda b . \EqtMACRoH {(b ^ {n})}{1}))}{x_{3}})}$.
IsCyclotomicExtensionclassMathlib.NumberTheory.Cyclotomic.Basic, predicateWording
S is a cyclotomic extension (from the name)
English
Let $S$ be an element of $\wp \Natural$. Let $A$ and $B$ be sets. Then we can say that $S$ is a cyclotomic extension.
IsCyclotomicExtension.algEquivdefMathlib.NumberTheory.Cyclotomic.Basic, function or constantWording
the algebra isomorphism of S (from the name)
English
Let $S$ be an element of $\wp \Natural$. Let $K$, $L$ and $\mathrm{L'}$ be sets. Then the algebra isomorphism of $S$ is an algebra isomorphism of $L$ and $\mathrm{L'}$.
cyclotomicCharacterdefMathlib.NumberTheory.Cyclotomic.CyclotomicCharacter, function or constantWording
the cyclotomic character of L and p (from the name)
English
Let $L$ be a set. Let $p$ be a natural number. Then the cyclotomic character of $L$ and $p$ is a monoid homomorphism of the set of ring isomorphisms of $L$ and $L$ and the set of units of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.
cyclotomicCharacter.toFundefMathlib.NumberTheory.Cyclotomic.CyclotomicCharacter, function or constantWording
the underlying function of the cyclotomic character of p and g (from the docstring)
English
Let $p$ be a natural number. Let $g$ be a ring isomorphism of $L$ and $L$. Then the underlying function of the cyclotomic character of $p$ and $g$ is a number integer ['\'\\\'p-adic_Adj\\\'\''] of $p$.
modularCyclotomicCharacterdefMathlib.NumberTheory.Cyclotomic.CyclotomicCharacter, function or constantWording
the modular cyclotomic character of L and hn (from the name)
English
Let $L$ be a set such that $\operatorname{card} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , L)}{x_{1}})})= n$. Then the modular cyclotomic character of $L$ and $\mathrm{hn}$ is a monoid homomorphism of the set of ring isomorphisms of $L$ and $L$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$ defined as the composition of the monoid homomorphism of the map equivalence of the multiplicative equivalence of the ring isomorphism congruence of $\mathrm{hn}$ and the modular cyclotomic character of $L$ and $n$.
modularCyclotomicCharacter'defMathlib.NumberTheory.Cyclotomic.CyclotomicCharacter, function or constantWording
the modular cyclotomic character of L and n (from the name)
English
Let $L$ be a set. Let $n$ be an element of $\Natural$. Then the modular cyclotomic character of $L$ and $n$ is a monoid homomorphism of the set of ring isomorphisms of $L$ and $L$ and $\UnitsMACRoAO {\mathrm{ZMod} (\operatorname{card} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , L)}{x_{1}})}))}$ defined as the homomorphism unit of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $n$ and $\operatorname{id}$ applied to $n$ and $\operatorname{comp}$ applied to $n$.
modularCyclotomicCharacter.toFundefMathlib.NumberTheory.Cyclotomic.CyclotomicCharacter, function or constantWording
the modular cyclotomic character of n and g (from the name)
English
Let $n$ be an element of $\Natural$. Let $g$ be a ring isomorphism of $L$ and $L$. Then the modular cyclotomic character of $n$ and $g$ is an element of $\mathrm{ZMod}$ applied to the cardinality of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , L)}{x_{1}})}$ defined as $\operatorname{aux}$ applied to $g$ and $n$.
IsCyclotomicExtension.autEquivPowdefMathlib.NumberTheory.Cyclotomic.Gal, function or constantWording
the automorphism equivalence power of L and h3 (from the name)
English
Let $L$ be a set. Assume that $\operatorname{cyclotomic}$ applied to $n$ and $K$ is irreducible. Then the automorphism equivalence power of $L$ and $h_{3}$ is a multiplicative equivalence of the set of algebra isomorphisms of $L$ and $L$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$.
IsCyclotomicExtension.fromZetaAutdefMathlib.NumberTheory.Cyclotomic.Gal, function or constantEnglish
Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $n$. Assume that $\operatorname{cyclotomic}$ applied to $n$ and $K$ is irreducible. Then $\operatorname{fromZetaAut}$ applied to $h_{2}$ and $h_{4}$ is an algebra isomorphism of $L$ and $L$.
galCyclotomicEquivUnitsZModdefMathlib.NumberTheory.Cyclotomic.Gal, function or constantEnglish
Assume that $\operatorname{cyclotomic}$ applied to $n$ and $K$ is irreducible. Then $\mathrm{galCyclotomicEquivUnitsZMod}$ applied to $h_{2}$ is a multiplicative equivalence of $\operatorname{Gal}$ applied to $\operatorname{cyclotomic}$ applied to $n$ and $K$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$ defined as the composition of the inverse of the automorphism congruence of the algebra isomorphism of $L$ and $\operatorname{cyclotomic}$ applied to $n$ and $K$ and the automorphism equivalence power of $L$ and $h_{2}$.
galXPowEquivUnitsZModdefMathlib.NumberTheory.Cyclotomic.Gal, function or constantEnglish
Assume that $\operatorname{cyclotomic}$ applied to $n$ and $K$ is irreducible. Then $\mathrm{galXPowEquivUnitsZMod}$ applied to $h_{2}$ is a multiplicative equivalence of $\operatorname{Gal}$ applied to $\operatorname{X} ^ {n}- 1$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$ defined as the composition of the inverse of the automorphism congruence of the algebra isomorphism of $L$ and $\operatorname{X} ^ {n}- 1$ and the automorphism equivalence power of $L$ and $h_{2}$.
IsCyclotomicExtension.zetadefMathlib.NumberTheory.Cyclotomic.PrimitiveRoots, function or constantWording
the Zeta of n (from the name)
English
Let $n$ be a natural number. Let $A$ and $B$ be sets. Then the Zeta of $n$ is an element of $B$.
IsPrimitiveRoot.embeddingsEquivPrimitiveRootsdefMathlib.NumberTheory.Cyclotomic.PrimitiveRoots, function or constantWording
the embedding equivalence primitive root of C and hirr (from the name)
English
Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{3}$ and $n$. Let $C$ be a set. Assume that $\operatorname{cyclotomic}$ applied to $n$ and $K$ is irreducible. Then the embedding equivalence primitive root of $C$ and $\mathrm{hirr}$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (L , C)}{(\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{primitiveRoots} (n , C)}{x_{6}})})}$.
IsPrimitiveRoot.powerBasisdefMathlib.NumberTheory.Cyclotomic.PrimitiveRoots, function or constantWording
the power basis of K and h3 (from the name)
English
Let $K$ be a set. Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{3}$ and $n$. Then the power basis of $K$ and $h_{3}$ is a power basis of $K$ and $L$.
IsPrimitiveRoot.subOnePowerBasisdefMathlib.NumberTheory.Cyclotomic.PrimitiveRoots, function or constantWording
the difference one power basis of K and h3 (from the name)
English
Let $K$ be a set. Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{3}$ and $n$. Then the difference one power basis of $K$ and $h_{3}$ is a power basis of $K$ and $L$.
DiophdefMathlib.NumberTheory.Dioph, predicateEnglish
Let $S$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow \Natural)$. Then $\mathrm{Dioph}$ holds for $S$, if there exists a set $x_{1}$, such that there exists a polynomial $p$ of $\mathrm{Sum}$ applied to $x$ and $x_{1}$, such that for all functions $v$ from elements of $x$ to natural numbers, $v$ is an element of $S$, if and only if there exists a function $t$ from elements of $x_{1}$ to natural numbers, such that $p (\operatorname{elim} (v , t))= 0$.
Dioph.DiophFndefMathlib.NumberTheory.Dioph, predicateEnglish
Let $f$ be a function from functions from elements of $x$ to natural numbers to natural numbers. Then $\operatorname{DiophFn}$ holds for $f$, if $\mathrm{Dioph}$ holds for $\operatorname{ofPred}$ applied to the function that maps $v$ to $\mathrm{Eq} (f (\operatorname{comp} (v , \operatorname{some})), v (\operatorname{none}))$.
Dioph.DiophPFundefMathlib.NumberTheory.Dioph, predicateEnglish
Let $f$ be a function of the set of functions from elements of $x$ to natural numbers and $\Natural$. Then $\operatorname{DiophPFun}$ holds for $f$, if $\mathrm{Dioph}$ holds for $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that $\ProdmkMACRoU {\operatorname{comp} (v , \operatorname{some})}{v (\operatorname{none})}$ is an element of the graph of $f$.
IsPolyinductiveMathlib.NumberTheory.Dioph, predicateWording
x1 is a polynomial (from the name)
English
Let $x_{1}$ be a function from functions from elements of $x$ to natural numbers to integers. Then we can say that $x_{1}$ is a polynomial.
IsPoly.belowinductiveMathlib.NumberTheory.Dioph, predicateEnglish
Assume that $x_{1}$ is a polynomial. Then we can say that $\operatorname{below}$ holds for $t$.
PolydefMathlib.NumberTheory.Dioph, typeWording
polynomial of x (from the name)
English
Let $x$ be a set. Then a polynomial of $x$ is an element of the function that maps $x$ to $\SubtypeSet {f}{\mathrm{IsPoly} (f)}$.
Poly.constdefMathlib.NumberTheory.Dioph, function or constantWording
the constant function with value of n (from the docstring)
English
Let $n$ be an integer. Then the constant function with value of $n$ is a polynomial of $x$ defined as the function that maps $x_{1}$ to $n$.
Poly.mapdefMathlib.NumberTheory.Dioph, function or constantWording
the map of f and g (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a polynomial of $x$. Then the map of $f$ and $g$ is a polynomial of $x_{1}$ defined as the function that maps $v$ to $g$ applied to $\operatorname{comp}$ applied to $v$ and $f$.
Poly.projdefMathlib.NumberTheory.Dioph, function or constantWording
the projection of i (from the name)
English
Let $i$ be an element of $x$. Then the projection of $i$ is a polynomial of $x$ defined as the function that maps $x_{1}$ to $x_{1}$ applied to $i$.
Poly.sumsqdefMathlib.NumberTheory.Dioph, function or constantEnglish
Let $x_{1}$ be a list of polynomials of $x$. Then $\operatorname{sumsq}$ applied to $x_{1}$ is a polynomial of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Poly\_\_sumsq\_\_\_f}$.
Real.ContfracLegendre.AssdefMathlib.NumberTheory.DiophantineApproximation.Basic, predicateEnglish
Let $x$ be an element of $\Real$. Let $u$ and $v$ be integers. Then $\operatorname{Ass}$ holds for $x$, $u$ and $v$, if $u$ is coprime to $v$, if $v = 1$, then $\operatorname{neg} (\frac{ 1}{2})< x - u$ and the absolute value of $x - \frac{ u}{v}$ is less than $\operatorname{inv}$ applied to $v \times (2 \times v - 1)$.
Real.convergentdefMathlib.NumberTheory.DiophantineApproximation.Basic, function or constantEnglish
Let $x$ be a real number. Let $x_{1}$ be a natural number. Then $\operatorname{convergent}$ applied to $x$ and $x_{1}$ is a rational number defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Real\_\_convergent\_\_\_f}$ and $x$.
DirichletCharacterdefMathlib.NumberTheory.DirichletCharacter.Basic, typeWording
Dirichlet character of R and n (from the name)
English
Let $R$ be a set. Let $n$ be a natural number. Then a Dirichlet character of $R$ and $n$ is an element of the function that maps $R$ and $n$ to the set of multiplicative characteristics of $\mathrm{ZMod}$ applied to $n$ and $R$.
DirichletCharacter.EvendefMathlib.NumberTheory.DirichletCharacter.Basic, predicateWording
x1 is even (from the docstring)
English
Let $x_{1}$ be a Dirichlet character of $S$ and $m$. Then $x_{1}$ is even, if $\EqtMACRoH {x_{1} (\operatorname{neg} (1))}{1}$.
DirichletCharacter.FactorsThroughdefMathlib.NumberTheory.DirichletCharacter.Basic, predicateEnglish
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Let $d$ be a natural number. Then $\operatorname{FactorsThrough}$ holds for $x_{1}$ and $d$, if there exists an element $h$ of $\divides {d}{n}$, such that there exists a Dirichlet character $x_{2}$ of $R$ and $d$, such that $\EqtMACRoH {x_{1}}{\operatorname{changeLevel} (h , x_{2})}$.
DirichletCharacter.FactorsThrough.χ₀defMathlib.NumberTheory.DirichletCharacter.Basic, function or constantEnglish
Assume that $\operatorname{FactorsThrough}$ holds for $x_{1}$ and $d$. Then $\mathrm{DirichletCharacter\_\_FactorsThrough\_\_\_u3c7\_\_u2080\_}$ applied to $h$ is a Dirichlet character of $R$ and $d$.
DirichletCharacter.IsPrimitivedefMathlib.NumberTheory.DirichletCharacter.Basic, predicateWording
x1 is primitive (from the docstring)
English
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Then $x_{1}$ is primitive, if the conductor of $x_{1}$ is equal to $n$.
DirichletCharacter.OdddefMathlib.NumberTheory.DirichletCharacter.Basic, predicateWording
x1 is odd (from the docstring)
English
Let $x_{1}$ be a Dirichlet character of $S$ and $m$. Then $x_{1}$ is odd, if $\EqtMACRoH {x_{1} (\operatorname{neg} (1))}{\operatorname{neg} (1)}$.
DirichletCharacter.annihilatordefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the annihilator of R and H (from the docstring)
English
Let $R$ be a set. Let $H$ be an element of $\wp \UnitsMACRoAO {\mathrm{ZMod} (n)}$. Then the annihilator of $R$ and $H$ is a subgroup of the set of Dirichlet characters of $R$ and $n$ defined as the multiplicative kernel of the restriction of the map of the coercion homomorphism of $\mathrm{ZMod}$ applied to $n$ and the closure of $H$ and $R$.
DirichletCharacter.changeLeveldefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the change level of hm (from the name)
English
Assume that $n$ divides $m$. Then the change level of $\mathrm{hm}$ is a monoid homomorphism of the set of Dirichlet characters of $R$ and $n$ and the set of Dirichlet characters of $R$ and $m$.
DirichletCharacter.conductordefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the conductor of x1 (from the name)
English
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Then the conductor of $x_{1}$ is a natural number defined as the infimum of the conductor set of $x_{1}$.
DirichletCharacter.conductorSetdefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the conductor set of x1 (from the name)
English
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Then the conductor set of $x_{1}$ is an element of $\wp \Natural$ defined as $\operatorname{ofPred}$ applied to the function that maps $d$ to $\operatorname{FactorsThrough}$ applied to $x_{1}$ and $d$.
DirichletCharacter.muldefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the product of x1 and x2 (from the name)
English
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Let $x_{2}$ be a Dirichlet character of $R$ and $m$. Then the product of $x_{1}$ and $x_{2}$ is a Dirichlet character of $R$ and $\NatlcmMACRoX {n}{m}$ defined as $\operatorname{changeLevel} (\mathrm{Nat\_\_dvd\_lcm\_left} (n , m), x_{1})\times \operatorname{changeLevel} (\mathrm{Nat\_\_dvd\_lcm\_right} (n , m), x_{2})$.
DirichletCharacter.primitiveCharacterdefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the primitive character of x1 (from the name)
English
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Then the primitive character of $x_{1}$ is a Dirichlet character of $R$ and the conductor of $x_{1}$.
DirichletCharacter.primitive_muldefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the primitive product of x1 and x2 (from the name)
English
Let $x_{1}$ be a Dirichlet character of $R$ and $n$. Let $x_{2}$ be a Dirichlet character of $R$ and $m$. Then the primitive product of $x_{1}$ and $x_{2}$ is a Dirichlet character of $R$ and the conductor of the product of $x_{1}$ and $x_{2}$ defined as the primitive character of the product of $x_{1}$ and $x_{2}$.
DirichletCharacter.subgroupOfCoprimeConductordefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the subgroup of d (from the name)
English
Let $d$ be a natural number. Then the subgroup of $d$ is a subgroup of the set of Dirichlet characters of $R$ and $n$.
DirichletCharacter.subgroupOfPrimitiveMapToOnedefMathlib.NumberTheory.DirichletCharacter.Basic, function or constantWording
the subgroup of n and p (from the name)
English
Let $R$ be a set. Let $n$ and $p$ be natural numbers. Then the subgroup of $n$ and $p$ is a subgroup of the set of Dirichlet characters of $R$ and $n$.
Int.divisorsdefMathlib.NumberTheory.Divisors, function or constantWording
the set of divisors of z (from the name)
English
Let $z$ be an integer. Then the set of divisors of $z$ is a finite set of $\Integer$.
Int.divisorsAntidiagdefMathlib.NumberTheory.Divisors, function or constantEnglish
Let $z$ be an integer. Then $\operatorname{divisorsAntidiag}$ applied to $z$ is a finite set of $\mathrm{Prod}$ applied to $\Integer$ and $\Integer$.
Nat.PerfectdefMathlib.NumberTheory.Divisors, predicateWording
n is perfect (from the docstring)
English
Let $n$ be an element of $\Natural$. Then $n$ is perfect, if $\FinsetSum {\operatorname{properDivisors} (n)}{i}{i}= n$ and $0 < n$.
Nat.divisorsdefMathlib.NumberTheory.Divisors, function or constantWording
the set of divisors of n (by hand)
English
Let $n$ be a natural number. Then the set of divisors of $n$ is a finite set of $\Natural$ defined as $\FinsetFilter {d}{(\divides {d}{n})}{(\FinsetIcoMACRoO {1}{(n + 1)})}$.
Nat.divisorsAntidiagonaldefMathlib.NumberTheory.Divisors, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{divisorsAntidiagonal}$ applied to $n$ is a finite set of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$.
Nat.divisorsAntidiagonalListdefMathlib.NumberTheory.Divisors, function or constantWording
the divisor antidiagonal list of n (from the name)
English
Let $n$ be a natural number. Then the divisor antidiagonal list of $n$ is a list of elements of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\operatorname{filterMap}$ applied to the function that maps $x$ to $\iteMACRoG {\mathrm{Eq} (x \times \frac{ n}{x}, n)}{\operatorname{some} (\ProdmkMACRoU {x}{(\frac{ n}{x})})}{\operatorname{none}}$ and $\operatorname{range'}$ applied to $1$, $n$ and $1$.
Nat.properDivisorsdefMathlib.NumberTheory.Divisors, function or constantWording
the set of proper divisors of n (by hand)
English
Let $n$ be a natural number. Then the set of proper divisors of $n$ is a finite set of $\Natural$ defined as $\FinsetFilter {d}{(\divides {d}{n})}{(\FinsetIcoMACRoO {1}{n})}$.
IsEllipticDvdSequencedefMathlib.NumberTheory.EllipticDivisibilitySequence, predicateWording
W is a elliptic divisibility sequence (from the name)
English
Let $W$ be a function from integers to elements of $R$. Then $W$ is an elliptic divisibility sequence, if $W$ is an elliptic sequence and $W$ is a divisibility sequence.
IsEllipticNetdefMathlib.NumberTheory.EllipticDivisibilitySequence, predicateWording
W is a elliptic net (from the name)
English
Let $W$ be a function from integers to elements of $R$. Then $W$ is an elliptic net, if for all integers $p$, $q$, $r$ and $s$, the relation of $r$ and $s$ is equal to $0$.
IsEllipticNet.atomdefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantWording
the atom of a and b (from the name)
English
Let $W$ be a function from integers to elements of $R$. Let $a$ and $b$ be integers. Then the atom of $a$ and $b$ is an element of $R$ defined as $W (\operatorname{tdiv} (a + b , 2))\times W (\operatorname{tdiv} (a - b , 2))$.
IsEllipticNet.atomReldefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantWording
the atom relation of c and d (from the name)
English
Let $W$ be a function from integers to elements of $R$. Let $a$, $b$, $c$ and $d$ be integers. Then the atom relation of $c$ and $d$ is an element of $R$ defined as the sum of the difference between the product of the atom of $a$ and $b$ and the atom of $c$ and $d$ and the product of the atom of $a$ and $c$ and the atom of $b$ and $d$ and the product of the atom of $a$ and $d$ and the atom of $b$ and $c$.
IsEllipticNet.reldefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantWording
the relation of r and s (from the name)
English
Let $W$ be a function from integers to elements of $R$. Let $p$, $q$, $r$ and $s$ be integers. Then the relation of $r$ and $s$ is an element of $R$ defined as $W (p + q + s)\times W (p - q)\times W (r + s)\times W (r)- W (p + r + s)\times W (p - r)\times W (q + s)\times W (q)+ W (q + r + s)\times W (q - r)\times W (p + s)\times W (p)$.
IsEllipticSequencedefMathlib.NumberTheory.EllipticDivisibilitySequence, predicateWording
W is a elliptic sequence (from the name)
English
Let $W$ be a function from integers to elements of $R$. Then $W$ is an elliptic sequence, if for all integers $p$, $q$ and $r$, the relation of $r$ and $0$ is equal to $0$.
complEDSdefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $b$, $c$ and $d$ be elements of $R$. Let $k$ and $n$ be integers. Then $\mathrm{complEDS}$ applied to $b$, $c$, $d$, $k$ and $n$ is an element of $R$ defined as $\operatorname{sign} (n)\times \mathrm{complEDS'} (b , c , d , k , \IntnatAbsMACRoY {n})$.
complEDS'defMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $b$, $c$ and $d$ be elements of $R$. Let $k$ be an integer. Let $x_{1}$ be a natural number. Then $\mathrm{complEDS'}$ applied to $b$, $c$, $d$, $k$ and $x_{1}$ is an element of $R$.
complEDSRecdefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $\mathrm{zero}$ be an element of $P$ applied to $0$. Let $\mathrm{one}$ be an element of $P$ applied to $1$. Let $\mathrm{even}$ be a function from natural numbers $m_{1}$ and elements of $P$ applied to $m_{1} + 1$ to elements of $P$ applied to $2 \times (m_{1} + 1)$. Let $\mathrm{odd}$ be a function from natural numbers $m$ and elements of $P$ applied to $m + 1$ and elements of $P$ applied to $m + 2$ to elements of $P$ applied to $2 \times (m + 1)+ 1$. Let $n$ be an element of $\Natural$. Then $\mathrm{complEDSRec}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $m_{1}$, $\mathrm{even}$, $m$, $\mathrm{odd}$ and $n$ is an element of $P$ applied to $n$.
complEDSRec'defMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $\mathrm{zero}$ be an element of $P$ applied to $0$. Let $\mathrm{one}$ be an element of $P$ applied to $1$. Let $\mathrm{even}$ be a function from natural numbers $m_{1}$ and functions from natural numbers $k_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k_{1} , 2 \times (m_{1} + 1))$ to elements of $P$ applied to $k_{1}$ to elements of $P$ applied to $2 \times (m_{1} + 1)$. Let $\mathrm{odd}$ be a function from natural numbers $m$ and functions from elements $k$ of $\Natural$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k , 2 \times (m + 1)+ 1)$ to elements of $P$ applied to $k$ to elements of $P$ applied to $2 \times (m + 1)+ 1$. Let $n$ be a natural number. Then $\mathrm{complEDSRec'}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $m_{1}$, $\mathrm{even}$, $m$, $\mathrm{odd}$ and $n$ is an element of $P$ applied to $n$ defined as the function that maps $\mathrm{odd}$ and $n$ to $\operatorname{evenOddStrongRec}$ applied to the function that maps $x$ to $\operatorname{casesAuxOn}$ applied to $x$, the function that maps $h$ to $\mathrm{zero}$ and the function that maps $x_{1}$ and $h_{1}$ to $m_{1}$ applied to $x_{1}$ and $h_{1}$, the function that maps $x_{2}$ to $\operatorname{casesAuxOn}$ applied to $x_{2}$, the function that maps $h_{2}$ to $\mathrm{one}$ and the function that maps $x_{3}$ and $h_{3}$ to $\mathrm{even}$ applied to $x_{3}$ and $h_{3}$, $m$, $\mathrm{odd}$ and $n$.
complEDS₂defMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $b$, $c$ and $d$ be elements of $R$. Let $k$ be an element of $\Integer$. Then $\mathrm{complEDS\_u2082\_}$ applied to $b$, $c$, $d$ and $k$ is an element of $R$ defined as $(\mathrm{preNormEDS} (b ^ {4}, c , d , k - 1)^ {2}\times \mathrm{preNormEDS} (b ^ {4}, c , d , k + 2)- \mathrm{preNormEDS} (b ^ {4}, c , d , k - 2)\times \mathrm{preNormEDS} (b ^ {4}, c , d , k + 1)^ {2})\times \iteMACRoG {\mathrm{even} (k)}{1}{b}$.
normEDSdefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $b$, $c$ and $d$ be elements of $R$. Let $n$ be an element of $\Integer$. Then $\mathrm{normEDS}$ applied to $b$, $c$, $d$ and $n$ is an element of $R$ defined as $\mathrm{preNormEDS} (b ^ {4}, c , d , n)\times \iteMACRoG {\mathrm{even} (n)}{b}{1}$.
normEDSRecdefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $\mathrm{zero}$ be an element of $P$ applied to $0$. Let $\mathrm{one}$ be an element of $P$ applied to $1$. Let $\mathrm{two}$ be an element of $P$ applied to $2$. Let $\mathrm{three}$ be an element of $P$ applied to $3$. Let $\mathrm{four}$ be an element of $P$ applied to $4$. Let $\mathrm{even}$ be a function from elements $m_{1}$ of $\Natural$ and elements of $P$ applied to $m_{1} + 1$ and elements of $P$ applied to $m_{1} + 2$ and elements of $P$ applied to $m_{1} + 3$ and elements of $P$ applied to $m_{1} + 4$ and elements of $P$ applied to $m_{1} + 5$ to elements of $P$ applied to $2 \times (m_{1} + 3)$. Let $\mathrm{odd}$ be a function from elements $m$ of $\Natural$ and elements of $P$ applied to $m + 1$ and elements of $P$ applied to $m + 2$ and elements of $P$ applied to $m + 3$ and elements of $P$ applied to $m + 4$ to elements of $P$ applied to $2 \times (m + 2)+ 1$. Let $n$ be an element of $\Natural$. Then $\mathrm{normEDSRec}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $\mathrm{two}$, $\mathrm{three}$, $\mathrm{four}$, $m_{1}$, $\mathrm{even}$, $m$, $\mathrm{odd}$ and $n$ is an element of $P$ applied to $n$.
normEDSRec'defMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $\mathrm{zero}$ be an element of $P$ applied to $0$. Let $\mathrm{one}$ be an element of $P$ applied to $1$. Let $\mathrm{two}$ be an element of $P$ applied to $2$. Let $\mathrm{three}$ be an element of $P$ applied to $3$. Let $\mathrm{four}$ be an element of $P$ applied to $4$. Let $\mathrm{even}$ be a function from natural numbers $m_{1}$ and functions from natural numbers $k_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k_{1} , 2 \times (m_{1} + 3))$ to elements of $P$ applied to $k_{1}$ to elements of $P$ applied to $2 \times (m_{1} + 3)$. Let $\mathrm{odd}$ be a function from natural numbers $m$ and functions from elements $k$ of $\Natural$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k , 2 \times (m + 2)+ 1)$ to elements of $P$ applied to $k$ to elements of $P$ applied to $2 \times (m + 2)+ 1$. Let $n$ be a natural number. Then $\mathrm{normEDSRec'}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $\mathrm{two}$, $\mathrm{three}$, $\mathrm{four}$, $m_{1}$, $\mathrm{even}$, $m$, $\mathrm{odd}$ and $n$ is an element of $P$ applied to $n$ defined as the function that maps $\mathrm{odd}$ and $n$ to $\operatorname{evenOddStrongRec}$ applied to the function that maps $x$ to $\operatorname{casesAuxOn}$ applied to $x$, the function that maps $h$ to $\mathrm{zero}$ and the function that maps $x_{1}$ to $\operatorname{casesAuxOn}$ applied to $x_{1}$, the function that maps $h_{1}$ to $\mathrm{two}$ and the function that maps $x_{2}$ to $\operatorname{casesAuxOn}$ applied to $x_{2}$, the function that maps $h_{2}$ to $\mathrm{four}$ and the function that maps $x_{3}$ and $h_{3}$ to $m_{1}$ applied to $x_{3}$ and $h_{3}$, the function that maps $x_{4}$ to $\operatorname{casesAuxOn}$ applied to $x_{4}$, the function that maps $h_{4}$ to $\mathrm{one}$ and the function that maps $x_{5}$ to $\operatorname{casesAuxOn}$ applied to $x_{5}$, the function that maps $h_{5}$ to $\mathrm{three}$ and the function that maps $x_{6}$ and $h_{6}$ to $\mathrm{even}$ applied to $x_{6}$ and $h_{6}$, $m$, $\mathrm{odd}$ and $n$.
preNormEDSdefMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $b$, $c$ and $d$ be elements of $R$. Let $n$ be an integer. Then $\mathrm{preNormEDS}$ applied to $b$, $c$, $d$ and $n$ is an element of $R$ defined as $\operatorname{sign} (n)\times \mathrm{preNormEDS'} (b , c , d , \IntnatAbsMACRoY {n})$.
preNormEDS'defMathlib.NumberTheory.EllipticDivisibilitySequence, function or constantEnglish
Let $b$, $c$ and $d$ be elements of $R$. Let $x_{1}$ be a natural number. Then $\mathrm{preNormEDS'}$ applied to $b$, $c$, $d$ and $x_{1}$ is an element of $R$.
dirichletSummandHomdefMathlib.NumberTheory.EulerProduct.DirichletLSeries, function or constantWording
the Dirichlet summand homomorphism of x and hs (from the name)
English
Let $x$ be a Dirichlet character of the set of complexes and $n$. Assume that $s \neq 0$. Then the Dirichlet summand homomorphism of $x$ and $\mathrm{hs}$ is a monoid with zero homomorphism of $\Natural$ and the set of complexes.
riemannZetaSummandHomdefMathlib.NumberTheory.EulerProduct.DirichletLSeries, function or constantWording
the Riemann Zeta summand homomorphism of hs (from the name)
English
Assume that $s \neq 0$. Then the Riemann Zeta summand homomorphism of $\mathrm{hs}$ is a monoid with zero homomorphism of $\Natural$ and the set of complexes.
FermatLastTheoremdefMathlib.NumberTheory.FLT.Basic, predicateEnglish
$\mathrm{FermatLastTheorem}$, if for all natural numbers $n$, if $n \geq 3$, then $\mathrm{FermatLastTheoremFor}$ holds for $n$.
FermatLastTheoremFordefMathlib.NumberTheory.FLT.Basic, predicateEnglish
Let $n$ be a natural number. Then $\mathrm{FermatLastTheoremFor}$ holds for $n$, if $\mathrm{FermatLastTheoremWith}$ holds for $\Natural$ and $n$.
FermatLastTheoremWithdefMathlib.NumberTheory.FLT.Basic, predicateEnglish
Let $R$ be a set. Let $n$ be a natural number. Then $\mathrm{FermatLastTheoremWith}$ holds for $R$ and $n$, if for all elements $a$, $b$ and $c$ of $R$, if $a \neq 0$, then if $b \neq 0$, then if $c \neq 0$, then $a ^ {n}+ b ^ {n}\neq c ^ {n}$.
FermatLastTheoremWith'defMathlib.NumberTheory.FLT.Basic, predicateEnglish
Let $R$ be a set. Let $n$ be a natural number. Then $\mathrm{FermatLastTheoremWith'}$ holds for $R$ and $n$, if for all elements $a$, $b$ and $c$ of $R$, if $a \neq 0$, then if $b \neq 0$, then if $c \neq 0$, then if $\EqtMACRoH {a ^ {n}+ b ^ {n}}{c ^ {n}}$, then there exist elements $d$, $\mathrm{a'}$, $\mathrm{b'}$ and $\mathrm{c'}$ of $R$, such that $\EqtMACRoH {a}{\mathrm{a'} \times d}$, $\EqtMACRoH {b}{\mathrm{b'} \times d}$, $\EqtMACRoH {c}{\mathrm{c'} \times d}$, $\mathrm{a'}$ is a unit, $\mathrm{b'}$ is a unit and $\mathrm{c'}$ is a unit.
Fermat42defMathlib.NumberTheory.FLT.Four, predicateEnglish
Let $a$, $b$ and $c$ be integers. Then $\mathrm{Fermat42}$ holds for $a$, $b$ and $c$, if $a \neq 0$, $b \neq 0$ and $a ^ {4}+ b ^ {4}= c ^ {2}$.
Fermat42.MinimaldefMathlib.NumberTheory.FLT.Four, predicateEnglish
Let $a$, $b$ and $c$ be integers. Then $\operatorname{Minimal}$ holds for $a$, $b$ and $c$, if $\mathrm{Fermat42}$ holds for $a$, $b$ and $c$ and for all integers $a_{1}$, for all integers $b_{1}$, for all integers $c_{1}$, if $\mathrm{Fermat42}$ holds for $a_{1}$, $b_{1}$ and $c_{1}$, then $\IntnatAbsMACRoY {c}\leq \IntnatAbsMACRoY {c_{1}}$.
Nat.AbundantdefMathlib.NumberTheory.FactorisationProperties, predicateWording
n is abundant (from the name)
English
Let $n$ be an element of $\Natural$. Then $n$ is abundant, if $n < \FinsetSum {\operatorname{properDivisors} (n)}{i}{i}$.
Nat.DeficientdefMathlib.NumberTheory.FactorisationProperties, predicateWording
n is deficient (from the name)
English
Let $n$ be an element of $\Natural$. Then $n$ is deficient, if $\FinsetSum {\operatorname{properDivisors} (n)}{i}{i}< n$.
Nat.PseudoperfectdefMathlib.NumberTheory.FactorisationProperties, predicateWording
n is pseudoperfect (from the name)
English
Let $n$ be a natural number. Then $n$ is pseudoperfect, if $0 < n$ and there exists a finite set $s$ of $\Natural$ such that $s$ is less than or equal to the set of proper divisors of $n$ and $\FinsetSum {s}{i}{i}= n$.
Nat.WeirddefMathlib.NumberTheory.FactorisationProperties, predicateEnglish
Let $n$ be a natural number. Then $\operatorname{Weird}$ holds for $n$, if $n$ is abundant and $n$ is not pseudoperfect.
Nat.abundancyIndexdefMathlib.NumberTheory.FactorisationProperties, function or constantEnglish
Let $n$ be an element of $\Natural$. Then $\operatorname{abundancyIndex}$ applied to $n$ is an element of $\Rational$ defined as $\frac{ \FinsetSum {\operatorname{divisors} (n)}{i}{i}}{n}$.
Nat.fermatNumberdefMathlib.NumberTheory.Fermat, function or constantWording
the Fermat number of n (from the name)
English
Let $n$ be a natural number. Then the Fermat number of $n$ is a natural number defined as $2 ^ {2 ^ {n}}+ 1$.
Nat.FermatPspdefMathlib.NumberTheory.FermatPsp, predicateEnglish
Let $n$ and $b$ be natural numbers. Then $\operatorname{FermatPsp}$ holds for $n$ and $b$, if $\operatorname{ProbablePrime}$ holds for $n$ and $b$, $n$ is not prime and $1 < n$.
Nat.ProbablePrimedefMathlib.NumberTheory.FermatPsp, predicateEnglish
Let $n$ and $b$ be natural numbers. Then $\operatorname{ProbablePrime}$ holds for $n$ and $b$, if $n$ divides $b ^ {(n - 1)}- 1$.
FrobeniusNumberdefMathlib.NumberTheory.FrobeniusNumber, predicateEnglish
Let $n$ be a natural number. Let $s$ be an element of $\wp \Natural$. Then $\mathrm{FrobeniusNumber}$ holds for $n$ and $s$, if $\mathrm{IsGreatest}$ holds for $\operatorname{ofPred}$ applied to the function that maps $k$ to the proposition that $k$ is not an element of the closure of $s$ and $n$.
Nat.setGcddefMathlib.NumberTheory.FrobeniusNumber, function or constantWording
the set greatest common divisor of s (from the name)
English
Let $s$ be an element of $\wp \Natural$. Then the set greatest common divisor of $s$ is a natural number defined as the absolute value of the generator of the span of the image of $\mathrm{instNatCastInt}$ and $s$.
FunctionFielddefMathlib.NumberTheory.FunctionField, predicateWording
K is a function field with respect to F (from the name)
English
Let $F$ and $K$ be sets. Then $K$ is a function field with respect to $F$, if $\mathrm{FiniteDimensional}$ holds for the set of rational number functions of $F$ and $K$.
FunctionField.ringOfIntegersdefMathlib.NumberTheory.FunctionField, function or constantWording
the ring of F and K (from the name)
English
Let $F$ and $K$ be sets. Then the ring of $F$ and $K$ is a subalgebra of the set of polynomials of $F$ and $K$ defined as the integral closure of the set of polynomials of $F$ and $K$.
Int.IsFundamentalDiscrdefMathlib.NumberTheory.FundamentalDiscriminant, predicateEnglish
Let $D$ be an integer. Then $\operatorname{IsFundamentalDiscr}$ holds for $D$, if $\HModhModMACRoF {D}{4}= 0$ or $\HModhModMACRoF {D}{4}= 1$, for all integers $x$, if $D$ is equal to the product of $4$ and $x$, then $4$ does not divide $x$ and $\HModhModMACRoF {x}{4}\neq 1$ and for all natural numbers $p$, if $p$ is prime, then if $p$ is odd, then $p ^ {2}$ does not divide $D$.
gaussSumdefMathlib.NumberTheory.GaussSum, function or constantWording
the Gauss sum of x3 and x4 (from the name)
English
Let $x_{3}$ be a multiplicative characteristic of $R$ and $\mathrm{R'}$. Let $x_{4}$ be an additive characteristic of $R$ and $\mathrm{R'}$. Then the Gauss sum of $x_{3}$ and $x_{4}$ is an element of $\mathrm{R'}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{a}{(x_{3} (a)\times x_{4} (a))}$.
harmonicdefMathlib.NumberTheory.Harmonic.Defs, function or constantEnglish
Let $x$ be a natural number. Then $\mathrm{harmonic}$ applied to $x$ is a rational number defined as $\FinsetSum {\FinsetrangeMACRoN {x}}{i}{\operatorname{inv} (i + 1)}$.
Real.eulerMascheroniConstantdefMathlib.NumberTheory.Harmonic.EulerMascheroni, function or constantEnglish
$\operatorname{eulerMascheroniConstant}$ is a real number defined as $\operatorname{limUnder}$ applied to $\operatorname{atTop}$ and $\operatorname{eulerMascheroniSeq}$.
Real.eulerMascheroniSeqdefMathlib.NumberTheory.Harmonic.EulerMascheroni, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{eulerMascheroniSeq}$ applied to $n$ is a real number defined as the difference between $\operatorname{cast}$ applied to $\mathrm{harmonic}$ applied to $n$ and the logarithm of $n + 1$.
Real.eulerMascheroniSeq'defMathlib.NumberTheory.Harmonic.EulerMascheroni, function or constantEnglish
Let $n$ be an element of $\Natural$. Then $\operatorname{eulerMascheroniSeq'}$ applied to $n$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Eq} (n , 0)}{2}{(\operatorname{cast} (\mathrm{harmonic} (n))- \operatorname{log} (n))}$.
riemannZeta₀defMathlib.NumberTheory.Harmonic.ZetaAsymp, function or constantWording
the Riemann Zeta of s (from the name)
English
Let $s$ be a complex. Then the Riemann Zeta of $s$ is a complex defined as $\iteMACRoG {(\EqtMACRoH {s}{1})}{\operatorname{ofReal} (\operatorname{eulerMascheroniConstant})}{(\mathrm{riemannZeta} (s)- \operatorname{inv} (s - 1))}$.
riemannZeta₁defMathlib.NumberTheory.Harmonic.ZetaAsymp, function or constantWording
the Riemann Zeta of s (from the name)
English
Let $s$ be a complex. Then the Riemann Zeta of $s$ is a complex defined as the sum of $1$ and the product of $s - 1$ and the Riemann Zeta of $s$.
HeckeCosetdefMathlib.NumberTheory.HeckeRing.Defs, typeEnglish
Let $x_{1}$ be a submonoid of $G$. Let $x_{2}$ and $x_{3}$ be subgroups of $G$. Then an element of $\mathrm{HeckeCoset}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is an element of the function that maps $x_{1}$, $x_{2}$ and $x_{3}$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$.
HeckeCoset.mkdefMathlib.NumberTheory.HeckeRing.Defs, function or constantEnglish
Let $x_{2}$ and $x_{3}$ be subgroups of $G$. Let $g$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {x_{1}}{x_{4}})}$. Then $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$ and $g$ is an element of $\mathrm{HeckeCoset}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ and $g$.
HeckeCosetModuledefMathlib.NumberTheory.HeckeRing.Defs, typeEnglish
Let $x_{1}$ be a submonoid of $G$. Let $x_{2}$ and $x_{3}$ be subgroups of $G$. Let $Z$ be a set. Then an element of $\mathrm{HeckeCosetModule}$ applied to $x_{1}$, $x_{2}$, $x_{3}$ and $Z$ is an element of the function that maps $x_{1}$, $x_{2}$, $x_{3}$ and $Z$ to $\FinsuppMACRoQ {\mathrm{HeckeCoset} (x_{1} , x_{2} , x_{3})}{Z}$.
HeckeCosetModule.ofdefMathlib.NumberTheory.HeckeRing.Defs, function or constantEnglish
$\operatorname{of}$ is an element of $\EquivMACRoAE {(\FinsuppMACRoQ {\mathrm{HeckeCoset} (x_{1} , x_{2} , x_{3})}{Z})}{\mathrm{HeckeCosetModule} (x_{1} , x_{2} , x_{3} , Z)}$ defined as the identity of $\FinsuppMACRoQ {\mathrm{HeckeCoset} (x_{1} , x_{2} , x_{3})}{Z}$.
HeckeRingdefMathlib.NumberTheory.HeckeRing.Defs, typeEnglish
Let $x_{1}$ be a submonoid of $G$. Let $H$ be a subgroup of $G$. Let $Z$ be a set. Then an element of $\mathrm{HeckeRing}$ applied to $x_{1}$, $H$ and $Z$ is an element of the function that maps $x_{1}$, $H$ and $Z$ to $\mathrm{HeckeCosetModule}$ applied to $x_{1}$, $H$, $H$ and $Z$.
IsHeckeTripleclassMathlib.NumberTheory.HeckeRing.Defs, predicateEnglish
Let $x_{1}$ be a submonoid of $G$. Let $x_{2}$ and $x_{3}$ be subgroups of $G$. Then we can say that $\mathrm{IsHeckeTriple}$ holds for $x_{1}$, $x_{2}$ and $x_{3}$.
Finsupp.logHeightdefMathlib.NumberTheory.Height.Basic, function or constantWording
the logarithmic height of x3 (from the docstring)
English
Let $x_{3}$ be an element of $\FinsuppMACRoQ {x_{2}}{K}$. Then the logarithmic height of $x_{3}$ is a real number defined as the logarithm of the multiplicative height of $\operatorname{coe}$ applied to $x_{3}$.
Finsupp.mulHeightdefMathlib.NumberTheory.Height.Basic, function or constantWording
the multiplicative height of x3 (from the docstring)
English
Let $x_{3}$ be an element of $\FinsuppMACRoQ {x_{2}}{K}$. Then the multiplicative height of $x_{3}$ is a real number defined as the multiplicative height of the function that maps $i$ to $x_{3}$ applied to $i$.
Height.AdmissibleAbsValuesclassMathlib.NumberTheory.Height.Basic, predicateEnglish
Let $K$ be a set. Then we can say that $\operatorname{AdmissibleAbsValues}$ holds for $K$.
Height.AdmissibleAbsValues.archAbsValdefMathlib.NumberTheory.Height.Basic, function or constantEnglish
$\operatorname{archAbsVal}$ is a multiset of the set of absolute values of $K$ and $\Real$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Height.AdmissibleAbsValues.nonarchAbsValdefMathlib.NumberTheory.Height.Basic, function or constantEnglish
$\operatorname{nonarchAbsVal}$ is an element of the power set of the set of absolute values of $K$ and $\Real$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Height.logHeightdefMathlib.NumberTheory.Height.Basic, function or constantWording
the logarithmic height of x3 (from the docstring)
English
Let $x_{3}$ be a function from elements of $x_{2}$ to elements of $K$. Then the logarithmic height of $x_{3}$ is a real number defined as the logarithm of the multiplicative height of $x_{3}$.
Height.logHeight₁defMathlib.NumberTheory.Height.Basic, function or constantWording
the logarithmic height of x2 (from the docstring)
English
Let $x_{2}$ be an element of $K$. Then the logarithmic height of $x_{2}$ is a real number defined as the logarithm of the multiplicative height of $x_{2}$.
Height.mulHeightdefMathlib.NumberTheory.Height.Basic, function or constantWording
the multiplicative height of x3 (from the docstring)
English
Let $x_{3}$ be a function from elements of $x_{2}$ to elements of $K$. Then the multiplicative height of $x_{3}$ is an element of $\Real$ defined as $\iteMACRoG {(\EqtMACRoH {x_{3}}{0})}{1}{(\operatorname{prod} (\operatorname{map} (\lambda v . \mathrm{iSup} (\lambda i . v (x_{3} (i))), \operatorname{archAbsVal}))\times \mathrm{finprod} (\lambda v_{1} . \mathrm{iSup} (\lambda i_{1} . \operatorname{val} (v_{1} , x_{3} (i_{1})))))}$.
Height.mulHeight₁defMathlib.NumberTheory.Height.Basic, function or constantWording
the multiplicative height of x2 (from the docstring)
English
Let $x_{2}$ be an element of $K$. Then the multiplicative height of $x_{2}$ is a real number defined as the product of the product of the map of the function that maps $v$ to $\MaxmaxMACRoAF {v (x_{2})}{1}$ and $\operatorname{archAbsVal}$ and $\mathrm{finprod}$ applied to the function that maps $v_{1}$ to $\MaxmaxMACRoAF {\operatorname{val} (v_{1} , x_{2})}{1}$.
Height.totalWeightdefMathlib.NumberTheory.Height.Basic, function or constantEnglish
Let $K$ be a set. Then $\operatorname{totalWeight}$ applied to $K$ is a natural number defined as the cardinality of $\operatorname{archAbsVal}$.
WeierstrassCurve.Affine.Point.naiveHeightdefMathlib.NumberTheory.Height.EllipticCurve, function or constantWording
the naive height of P (from the name)
English
Let $P$ be a point of $W$. Then the naive height of $P$ is a real number defined as the logarithmic height of $\operatorname{xRep}$ applied to $P$.
Height.mulHeightBounddefMathlib.NumberTheory.Height.MvPolynomial, function or constantWording
the multiplicative height bound of p (from the name)
English
Let $p$ be a function from elements of $x_{2}$ to multivariate polynomials of $x_{1}$ and $K$. Then the multiplicative height bound of $p$ is a real number defined as the product of the product of the map of the function that maps $v$ to the supremum of the function that maps $j$ to the sum of the coefficient of $p$ applied to $j$ and the function that maps $x_{4}$ and $c$ to $v$ applied to $c$ and $\operatorname{archAbsVal}$ and $\mathrm{finprod}$ applied to the function that maps $v_{1}$ to the supremum of the function that maps $j_{1}$ to the maximum of the supremum of the function that maps $s$ to $\operatorname{val}$ applied to $v_{1}$ and $\operatorname{coeff}$ applied to $p$ applied to $j_{1}$ and $s$ and $1$.
NumberField.absLogHeight₁defMathlib.NumberTheory.Height.NumberField, function or constantWording
the absolute logarithmic height of x1 (from the docstring)
English
Let $x_{1}$ be an element of $K$. Then the absolute logarithmic height of $x_{1}$ is a real number defined as the logarithm of the absolute multiplicative height of $x_{1}$.
NumberField.absMulHeight₁defMathlib.NumberTheory.Height.NumberField, function or constantWording
the absolute multiplicative height of x1 (from the docstring)
English
Let $x_{1}$ be an element of $K$. Then the absolute multiplicative height of $x_{1}$ is a real number defined as $\mathrm{dite}$ applied to the proposition that $x_{1}$ is integral, the function that maps $\mathrm{hx}$ to the exponentiation of the multiplicative height of the generator of $\Rational$ and $x_{1}$ to $\operatorname{inv}$ applied to the rank of $\Rational$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\Rational , \operatorname{singleton} (x_{1}))}{x_{2}})}$ and the function that maps $\mathrm{hx1}$ to $1$.
NumberField.multisetInfinitePlacedefMathlib.NumberTheory.Height.NumberField, function or constantWording
the multiset infinite place of K (from the name)
English
Let $K$ be a set. Then the multiset infinite place of $K$ is a multiset of the set of absolute values of $K$ and $\Real$ defined as $\operatorname{bind}$ applied to the value of the universal set and the function that maps $v$ to $\operatorname{replicate}$ applied to the multiplicity of $v$ and $v$.
Projectivization.logHeightdefMathlib.NumberTheory.Height.Projectivization, function or constantWording
the logarithmic height of x3 (from the docstring)
English
Let $x_{3}$ be a projectivization of $K$ and the set of functions from elements of $x_{2}$ to elements of $K$. Then the logarithmic height of $x_{3}$ is a real number.
Projectivization.mulHeightdefMathlib.NumberTheory.Height.Projectivization, function or constantWording
the multiplicative height of x3 (from the docstring)
English
Let $x_{3}$ be a projectivization of $K$ and the set of functions from elements of $x_{2}$ to elements of $K$. Then the multiplicative height of $x_{3}$ is a real number.
jacobiSumdefMathlib.NumberTheory.JacobiSum.Basic, function or constantWording
the Jacobi sum of x3 and x4 (from the name)
English
Let $x_{3}$ and $x_{4}$ be multiplicative characteristics of $R$ and $\mathrm{R'}$. Then the Jacobi sum of $x_{3}$ and $x_{4}$ is an element of $\mathrm{R'}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{x_{5}}{(x_{3} (x_{5})\times x_{4} (1 - x_{5}))}$.
KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMkdefMathlib.NumberTheory.KummerDedekind, function or constantWording
the normalized factor map equivalence normalized factor minimum polynomial of #3 and #4 (from the name)
English
Assume that $I$ is maximal. Assume that $I$ is distinct from the bottom. Assume that the maximum of the preimage of the conductor of $R$ and $x_{3}$ under the algebra map of $R$ and $S$ and $I$ is equal to the top. Assume that $x_{3}$ is integral. Then the normalized factor map equivalence normalized factor minimum polynomial of $\mathrm{hx}$ and $\mathrm{hx'}$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $J$ to the proposition that $J$ is an element of the normalized factor of the map of the algebra map of $R$ and $S$ and $I$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $d$ to the proposition that $d$ is an element of the normalized factor of the map of $\operatorname{mk}$ applied to $I$ and the minimal polynomial of $R$ and $x_{3}$.
KummerDedekind.quotMapEquivQuotQuotMapdefMathlib.NumberTheory.KummerDedekind, function or constantWording
the quotient map equivalence quotient quotient map of hx and #2 (from the name)
English
Assume that the maximum of the preimage of the conductor of $R$ and $x_{3}$ under the algebra map of $R$ and $S$ and $I$ is equal to the top. Assume that $x_{3}$ is integral. Then the quotient map equivalence quotient quotient map of $\mathrm{hx}$ and $\mathrm{hx'}$ is a ring isomorphism of the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $I$ and the set of quotients of the set of polynomials of the set of quotients of $R$ and $I$ and the span of $\operatorname{singleton}$ applied to the map of $\operatorname{mk}$ applied to $I$ and the minimal polynomial of $R$ and $x_{3}$.
IsStrongFEPairstructureMathlib.NumberTheory.LSeries.AbstractFuncEq, predicateEnglish
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then we can say that $\mathrm{IsStrongFEPair}$ holds for $P$.
WeakFEPairstructureMathlib.NumberTheory.LSeries.AbstractFuncEq, typeEnglish
Let $E$ be a set. Then the elements of $\mathrm{WeakFEPair}$ applied to $E$ are a basic type.
WeakFEPair.fdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Let $x_{2}$ be a real number. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
WeakFEPair.f_modifdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Let $x_{2}$ be an element of $\Real$. Then $\mathrm{WeakFEPair\_\_f\_modif}$ applied to $P$ and $x_{2}$ is an element of $E$ defined as $\mathrm{plus} (\operatorname{indicator} (\lambda x_{2} . \operatorname{f} (P , x_{2})- \mathrm{WeakFEPair\_\_f\_u2080\_} (P)), \operatorname{indicator} (\lambda x_{3} . \operatorname{f} (P , x_{3})- \HSMulhSMulMACRoAL {(\mathrm{WeakFEPair\_\_\_u3b5\_} (P)\times \operatorname{ofReal} (x_{3} ^ {\operatorname{neg} (\operatorname{k} (P))}))}{\mathrm{WeakFEPair\_\_g\_u2080\_} (P)}), x_{2})$.
WeakFEPair.f₀defMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then $\mathrm{WeakFEPair\_\_f\_u2080\_}$ applied to $\mathrm{self}$ is an element of $E$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.
WeakFEPair.gdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Let $x_{2}$ be a real number. Then $\operatorname{g}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $E$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
WeakFEPair.g_modifdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Let $x_{2}$ be an element of $\Real$. Then $\mathrm{WeakFEPair\_\_g\_modif}$ applied to $P$ and $x_{2}$ is an element of $E$ defined as $\mathrm{plus} (\operatorname{indicator} (\lambda x_{2} . \operatorname{g} (P , x_{2})- \mathrm{WeakFEPair\_\_g\_u2080\_} (P)), \operatorname{indicator} (\lambda x_{3} . \operatorname{g} (P , x_{3})- \HSMulhSMulMACRoAL {(\operatorname{inv} (\mathrm{WeakFEPair\_\_\_u3b5\_} (P))\times \operatorname{ofReal} (x_{3} ^ {\operatorname{neg} (\operatorname{k} (P))}))}{\mathrm{WeakFEPair\_\_f\_u2080\_} (P)}), x_{2})$.
WeakFEPair.g₀defMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then $\mathrm{WeakFEPair\_\_g\_u2080\_}$ applied to $\mathrm{self}$ is an element of $E$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.
WeakFEPair.kdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then $\operatorname{k}$ applied to $\mathrm{self}$ is a real number defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
WeakFEPair.symmdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantWording
the inverse of P (from the name)
English
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then the inverse of $P$ is an element of $\mathrm{WeakFEPair}$ applied to $E$.
WeakFEPair.toStrongFEPairdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then $\operatorname{toStrongFEPair}$ applied to $P$ is an element of $\mathrm{WeakFEPair}$ applied to $E$.
WeakFEPair.ΛdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Let $s$ be a complex. Then $\mathrm{WeakFEPair\_\_\_u39b\_}$ applied to $P$ and $s$ is an element of $E$ defined as $\mathrm{WeakFEPair\_\_\_u39b\_\_u2080\_} (P , s)- \HSMulhSMulMACRoAL {(\frac{ 1}{s})}{\mathrm{WeakFEPair\_\_f\_u2080\_} (P)}- \HSMulhSMulMACRoAL {(\frac{ \mathrm{WeakFEPair\_\_\_u3b5\_} (P)}{\operatorname{ofReal} (\operatorname{k} (P))- s})}{\mathrm{WeakFEPair\_\_g\_u2080\_} (P)}$.
WeakFEPair.Λ₀defMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $P$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Let $x_{2}$ be a complex. Then $\mathrm{WeakFEPair\_\_\_u39b\_\_u2080\_}$ applied to $P$ and $x_{2}$ is an element of $E$ defined as $\mathrm{mellin}$ applied to $\mathrm{WeakFEPair\_\_f\_modif}$ applied to $P$ and $x_{2}$.
WeakFEPair.εdefMathlib.NumberTheory.LSeries.AbstractFuncEq, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WeakFEPair}$ applied to $E$. Then $\mathrm{WeakFEPair\_\_\_u3b5\_}$ applied to $\mathrm{self}$ is a complex defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
LSeriesdefMathlib.NumberTheory.LSeries.Basic, function or constantWording
the series of f and s (from the name)
English
Let $f$ be a function from natural numbers to complexes. Let $s$ be a complex. Then the series of $f$ and $s$ is a complex defined as the sum of the function that maps $n$ to $\operatorname{term}$ applied to $f$, $s$ and $n$ and $\operatorname{unconditional}$ applied to $\Natural$.
LSeries.deltadefMathlib.NumberTheory.LSeries.Basic, function or constantWording
the delta of n (from the name)
English
Let $n$ be a natural number. Then the delta of $n$ is a complex defined as $\iteMACRoG {\mathrm{Eq} (n , 1)}{1}{0}$.
LSeriesHasSumdefMathlib.NumberTheory.LSeries.Basic, predicateEnglish
Let $f$ be a function from natural numbers to complexes. Let $s$ and $a$ be complexes. Then $\mathrm{LSeriesHasSum}$ holds for $f$, $s$ and $a$, if $\mathrm{HasSum}$ holds for $\operatorname{term}$ applied to $f$ and $s$, $a$ and $\operatorname{unconditional}$ applied to $\Natural$.
LSeriesSummabledefMathlib.NumberTheory.LSeries.Basic, predicateEnglish
Let $f$ be a function from natural numbers to complexes. Let $s$ be a complex. Then $\mathrm{LSeriesSummable}$ holds for $f$ and $s$, if $\operatorname{term}$ applied to $f$ and $s$ is summable with respect to $\operatorname{unconditional}$ applied to $\Natural$.
LSeries.abscissaOfAbsConvdefMathlib.NumberTheory.LSeries.Convergence, function or constantWording
the abscissa of f (from the docstring)
English
Let $f$ be a function from natural numbers to complexes. Then the abscissa of $f$ is an element of $\mathrm{EReal}$ defined as the infimum of the image of $\operatorname{toEReal}$ and $\operatorname{ofPred}$ applied to the function that maps $x$ to $\mathrm{LSeriesSummable}$ applied to $f$ and the natural inclusion of the real numbers into the complex numbers of $x$.
LSeries.convolutiondefMathlib.NumberTheory.LSeries.Convolution, function or constantWording
the convolution of g and x1 (from the name)
English
Let $f$ and $g$ be functions from natural numbers to elements of $R$. Let $x_{1}$ be a natural number. Then the convolution of $g$ and $x_{1}$ is an element of $R$ defined as the coercion of the product of the arithmetic function of $f$ and the arithmetic function of $g$ and $x_{1}$.
toArithmeticFunctiondefMathlib.NumberTheory.LSeries.Convolution, function or constantWording
the arithmetic function of f (from the name)
English
Let $f$ be a function from natural numbers to elements of $R$. Then the arithmetic function of $f$ is an arithmetic function of $R$.
LSeries.logMuldefMathlib.NumberTheory.LSeries.Deriv, function or constantWording
the logarithm product of f and n (from the name)
English
Let $f$ be a function from natural numbers to complexes. Let $n$ be a natural number. Then the logarithm product of $f$ and $n$ is a complex defined as the product of the logarithm of $n$ and $f$ applied to $n$.
DirichletCharacter.LFunctiondefMathlib.NumberTheory.LSeries.DirichletContinuation, function or constantWording
the unique meromorphic function of x and s (from the docstring)
English
Let $x$ be a Dirichlet character of the set of complexes and $N$. Let $s$ be a complex. Then the unique meromorphic function of $x$ and $s$ is a complex defined as the unique meromorphic function of $\operatorname{coe}$ applied to $x$ and $s$.
DirichletCharacter.LFunctionTrivChardefMathlib.NumberTheory.LSeries.DirichletContinuation, function or constantWording
the function trivial characteristic of N and s (from the name)
English
Let $N$ be a natural number. Let $s$ be a complex. Then the function trivial characteristic of $N$ and $s$ is a complex defined as the unique meromorphic function of $1$ and $s$.
DirichletCharacter.LFunctionTrivChar₁defMathlib.NumberTheory.LSeries.DirichletContinuation, function or constantWording
the function trivial characteristic of n and x (from the name)
English
Let $n$ be an element of $\Natural$. Let $x$ be a complex. Then the function trivial characteristic of $n$ and $x$ is a complex defined as $\operatorname{update}$ applied to the function that maps $s$ to $(s - 1)\times \operatorname{LFunctionTrivChar} (n , s)$, $1$, $\FinsetProd {\operatorname{primeFactors} (n)}{p}{(1 - \operatorname{inv} (p))}$ and $x$.
DirichletCharacter.completedLFunctiondefMathlib.NumberTheory.LSeries.DirichletContinuation, function or constantWording
the completed function of x and s (from the name)
English
Let $x$ be a Dirichlet character of the set of complexes and $N$. Let $s$ be a complex. Then the completed function of $x$ and $s$ is a complex defined as the completed function of $\operatorname{coe}$ applied to $x$ and $s$.
DirichletCharacter.gammaFactordefMathlib.NumberTheory.LSeries.DirichletContinuation, function or constantWording
the Gamma factor of x and s (from the name)
English
Let $x$ be a Dirichlet character of the set of complexes and $N$. Let $s$ be a complex. Then the Gamma factor of $x$ and $s$ is a complex defined as $\iteMACRoG {\operatorname{Even} (x)}{\mathrm{Complex\_\_Gamma\_u211d\_} (s)}{\mathrm{Complex\_\_Gamma\_u211d\_} (s + 1)}$.
DirichletCharacter.rootNumberdefMathlib.NumberTheory.LSeries.DirichletContinuation, function or constantWording
the root number of x (from the name)
English
Let $x$ be a Dirichlet character of the set of complexes and $N$. Then the root number of $x$ is a complex defined as $\frac{ \frac{ \mathrm{gaussSum} (x , \operatorname{stdAddChar})}{\operatorname{I} ^ {\iteMACRoG {\operatorname{Even} (x)}{0}{1}}}}{N ^ {\frac{ 1}{2}}}$.
hardyZdefMathlib.NumberTheory.LSeries.HardyZ, function or constantEnglish
Let $t$ be a real number. Then $\mathrm{hardyZ}$ applied to $t$ is a real number defined as the quotient of the real part of the completed Riemann Zeta of the sum of $\frac{ 1}{2}$ and the product of the natural inclusion of the real numbers into the complex numbers of $t$ and $\operatorname{I}$ and the norm of the Gamma of the sum of $\frac{ 1}{2}$ and the product of the natural inclusion of the real numbers into the complex numbers of $t$ and $\operatorname{I}$.
HurwitzZeta.expZetadefMathlib.NumberTheory.LSeries.HurwitzZeta, function or constantWording
the exponential Zeta of a and s (from the name)
English
Let $a$ be a unit circle. Let $s$ be a complex. Then the exponential Zeta of $a$ and $s$ is a complex defined as the sum of $\operatorname{cosZeta}$ applied to $a$ and $s$ and the product of $\operatorname{I}$ and the sin Zeta of $a$ and $s$.
HurwitzZeta.hurwitzZetadefMathlib.NumberTheory.LSeries.HurwitzZeta, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\operatorname{hurwitzZeta}$ applied to $a$ and $s$ is a complex defined as $\operatorname{hurwitzZetaEven} (a , s)+ \operatorname{hurwitzZetaOdd} (a , s)$.
HurwitzZeta.completedCosZetadefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\operatorname{completedCosZeta}$ applied to $a$ and $s$ is a complex defined as the quotient of $\mathrm{WeakFEPair\_\_\_u39b\_}$ applied to the inverse of $\operatorname{hurwitzEvenFEPair}$ applied to $a$ and $\frac{ s}{2}$ and $2$.
HurwitzZeta.completedCosZeta₀defMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\mathrm{HurwitzZeta\_\_completedCosZeta\_u2080\_}$ applied to $a$ and $s$ is a complex defined as the quotient of $\mathrm{WeakFEPair\_\_\_u39b\_\_u2080\_}$ applied to the inverse of $\operatorname{hurwitzEvenFEPair}$ applied to $a$ and $\frac{ s}{2}$ and $2$.
HurwitzZeta.completedHurwitzZetaEvendefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\operatorname{completedHurwitzZetaEven}$ applied to $a$ and $s$ is a complex defined as $\frac{ \mathrm{WeakFEPair\_\_\_u39b\_} (\operatorname{hurwitzEvenFEPair} (a), \frac{ s}{2})}{2}$.
HurwitzZeta.completedHurwitzZetaEven₀defMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\mathrm{HurwitzZeta\_\_completedHurwitzZetaEven\_u2080\_}$ applied to $a$ and $s$ is a complex defined as $\frac{ \mathrm{WeakFEPair\_\_\_u39b\_\_u2080\_} (\operatorname{hurwitzEvenFEPair} (a), \frac{ s}{2})}{2}$.
HurwitzZeta.cosKerneldefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $x$ be a real number. Then $\operatorname{cosKernel}$ applied to $a$ and $x$ is a real number.
HurwitzZeta.cosZetadefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $a_{1}$ be a complex. Then $\operatorname{cosZeta}$ applied to $a$ and $a_{1}$ is a complex defined as $\operatorname{update}$ applied to the function that maps $s$ to the quotient of $\operatorname{completedCosZeta}$ applied to $a$ and $s$ and the Gamma of $s$, $0$, $\frac{ \operatorname{neg} (1)}{2}$ and $a_{1}$.
HurwitzZeta.evenKerneldefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantWording
the even kernel of a and x (from the name)
English
Let $a$ be a unit circle. Let $x$ be a real number. Then the even kernel of $a$ and $x$ is a real number.
HurwitzZeta.hurwitzEvenFEPairdefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Then $\operatorname{hurwitzEvenFEPair}$ applied to $a$ is an element of $\mathrm{WeakFEPair}$ applied to the set of complexes.
HurwitzZeta.hurwitzZetaEvendefMathlib.NumberTheory.LSeries.HurwitzZetaEven, function or constantEnglish
Let $a$ be a unit circle. Let $a_{1}$ be a complex. Then $\operatorname{hurwitzZetaEven}$ applied to $a$ and $a_{1}$ is a complex defined as $\operatorname{update}$ applied to the function that maps $s$ to the quotient of $\operatorname{completedHurwitzZetaEven}$ applied to $a$ and $s$ and the Gamma of $s$, $0$, $\iteMACRoG {(\EqtMACRoH {a}{0})}{(\frac{ \operatorname{neg} (1)}{2})}{0}$ and $a_{1}$.
HurwitzZeta.completedHurwitzZetaOdddefMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\operatorname{completedHurwitzZetaOdd}$ applied to $a$ and $s$ is a complex defined as $\frac{ \mathrm{WeakFEPair\_\_\_u39b\_} (\operatorname{hurwitzOddFEPair} (a), \frac{ s + 1}{2})}{2}$.
HurwitzZeta.completedSinZetadefMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantWording
the completed sin Zeta of a and s (from the name)
English
Let $a$ be a unit circle. Let $s$ be a complex. Then the completed sin Zeta of $a$ and $s$ is a complex defined as the quotient of $\mathrm{WeakFEPair\_\_\_u39b\_}$ applied to the inverse of $\operatorname{hurwitzOddFEPair}$ applied to $a$ and $\frac{ s + 1}{2}$ and $2$.
HurwitzZeta.hurwitzOddFEPairdefMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantEnglish
Let $a$ be a unit circle. Then $\operatorname{hurwitzOddFEPair}$ applied to $a$ is an element of $\mathrm{WeakFEPair}$ applied to the set of complexes.
HurwitzZeta.hurwitzZetaOdddefMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantEnglish
Let $a$ be a unit circle. Let $s$ be a complex. Then $\operatorname{hurwitzZetaOdd}$ applied to $a$ and $s$ is a complex defined as the quotient of $\operatorname{completedHurwitzZetaOdd}$ applied to $a$ and $s$ and the Gamma of $s + 1$.
HurwitzZeta.jacobiTheta₂''defMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantWording
the Jacobi theta of z and x (from the name)
English
Let $z$ and $x$ be complexes. Then the Jacobi theta of $z$ and $x$ is a complex defined as the product of the exponential of the product of the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$, $z ^ {2}$ and $x$ and the sum of the quotient of the Jacobi theta of $z \times x$ and $x$ and the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product and $\operatorname{I}$ and the product of $z$ and the Jacobi theta of $z \times x$ and $x$.
HurwitzZeta.oddKerneldefMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantWording
the odd kernel of a and x (from the name)
English
Let $a$ be a unit circle. Let $x$ be a real number. Then the odd kernel of $a$ and $x$ is a real number.
HurwitzZeta.sinZetadefMathlib.NumberTheory.LSeries.HurwitzZetaOdd, function or constantWording
the sin Zeta of a and s (from the name)
English
Let $a$ be a unit circle. Let $s$ be a complex. Then the sin Zeta of $a$ and $s$ is a complex defined as the quotient of the completed sin Zeta of $a$ and $s$ and the Gamma of $s + 1$.
DirichletCharacter.zetaMuldefMathlib.NumberTheory.LSeries.Nonvanishing, function or constantWording
the Zeta product of x (from the name)
English
Let $x$ be a Dirichlet character of the set of complexes and $N$. Then the Zeta product of $x$ is an arithmetic function of the set of complexes defined as the product of $\operatorname{natToArithmeticFunction}$ applied to the Zeta and the arithmetic function of the function that maps $x_{1}$ to $x$ applied to $x_{1}$.
ArithmeticFunction.vonMangoldt.residueClassdefMathlib.NumberTheory.LSeries.PrimesInAP, function or constantWording
the residue class of a and x (from the name)
English
Let $a$ be an element of $\mathrm{ZMod}$ applied to $q$. Let $x$ be a natural number. Then the residue class of $a$ and $x$ is a real number defined as the indicator of the function that maps $x$ to $\operatorname{vonMangoldt}$ applied to $x$ and $x$.
RiemannHypothesisdefMathlib.NumberTheory.LSeries.RiemannZeta, predicateEnglish
$\mathrm{RiemannHypothesis}$, if for all complexes $s$, if the Riemann zeta function of $s$ is equal to $0$, then if it is not the case that there exists a natural number $n$, such that $\EqtMACRoH {s}{\operatorname{neg} (2)\times (n + 1)}$, then if $s \neq 1$, then the real part of $s$ is equal to $\frac{ 1}{2}$.
completedRiemannZetadefMathlib.NumberTheory.LSeries.RiemannZeta, function or constantWording
the completed Riemann Zeta of s (from the name)
English
Let $s$ be a complex. Then the completed Riemann Zeta of $s$ is a complex defined as $\operatorname{completedHurwitzZetaEven}$ applied to $0$ and $s$.
completedRiemannZeta₀defMathlib.NumberTheory.LSeries.RiemannZeta, function or constantWording
the completed Riemann Zeta of s (from the name)
English
Let $s$ be a complex. Then the completed Riemann Zeta of $s$ is a complex defined as $\mathrm{HurwitzZeta\_\_completedHurwitzZetaEven\_u2080\_}$ applied to $0$ and $s$.
riemannZetadefMathlib.NumberTheory.LSeries.RiemannZeta, function or constantWording
the Riemann zeta function of a (from the docstring)
English
Let $a$ be a complex. Then the Riemann zeta function of $a$ is a complex defined as $\operatorname{hurwitzZetaEven}$ applied to $0$ and $a$.
ZMod.LFunctiondefMathlib.NumberTheory.LSeries.ZMod, function or constantWording
the unique meromorphic function of x and s (from the docstring)
English
Let $x$ be a function from elements of $\mathrm{ZMod}$ applied to $N$ to complexes. Let $s$ be a complex. Then the unique meromorphic function of $x$ and $s$ is a complex defined as $N ^ {\operatorname{neg} (s)}\times \FinsetSum {\FinsetunivMACRoAC}{j}{(x (j)\times \operatorname{hurwitzZeta} (\operatorname{toAddCircle} (j), s))}$.
ZMod.completedLFunctiondefMathlib.NumberTheory.LSeries.ZMod, function or constantWording
the completed function of x and s (from the name)
English
Let $x$ be a function from elements of $\mathrm{ZMod}$ applied to $N$ to complexes. Let $s$ be a complex. Then the completed function of $x$ and $s$ is a complex defined as $N ^ {\operatorname{neg} (s)}\times \FinsetSum {\FinsetunivMACRoAC}{j}{(x (j)\times \operatorname{completedHurwitzZetaEven} (\operatorname{toAddCircle} (j), s))}+ N ^ {\operatorname{neg} (s)}\times \FinsetSum {\FinsetunivMACRoAC}{j_{1}}{(x (j_{1})\times \operatorname{completedHurwitzZetaOdd} (\operatorname{toAddCircle} (j_{1}), s))}$.
ZMod.completedLFunction₀defMathlib.NumberTheory.LSeries.ZMod, function or constantWording
the completed function of x and s (from the name)
English
Let $x$ be a function from elements of $\mathrm{ZMod}$ applied to $N$ to complexes. Let $s$ be a complex. Then the completed function of $x$ and $s$ is a complex defined as $N ^ {\operatorname{neg} (s)}\times \FinsetSum {\FinsetunivMACRoAC}{j}{(x (j)\times \mathrm{HurwitzZeta\_\_completedHurwitzZetaEven\_u2080\_} (\operatorname{toAddCircle} (j), s))}+ N ^ {\operatorname{neg} (s)}\times \FinsetSum {\FinsetunivMACRoAC}{j_{1}}{(x (j_{1})\times \operatorname{completedHurwitzZetaOdd} (\operatorname{toAddCircle} (j_{1}), s))}$.
riemannZetaZerosdefMathlib.NumberTheory.LSeries.ZetaZeros, function or constantWording
the Riemann Zeta zero (from the name)
English
The Riemann Zeta zero is an element of the power set of the set of complexes defined as the preimage of $\mathrm{riemannZeta}$ and $\operatorname{singleton}$ applied to $0$.
AddChar.FiniteField.primitiveChardefMathlib.NumberTheory.LegendreSymbol.AddCharacter, function or constantWording
the primitive characteristic of h1 and #3 (from the name)
English
Let $F$ and $\mathrm{F'}$ be sets such that the ring characteristic of $\mathrm{F'}$ is distinct from the ring characteristic of $F$. Then the primitive characteristic of $\mathrm{F'}$ and $h_{1}$ is a primitive additive characteristic of $F$ and $\mathrm{F'}$.
AddChar.IsPrimitivedefMathlib.NumberTheory.LegendreSymbol.AddCharacter, predicateWording
x2 is primitive (from the name)
English
Let $x_{2}$ be an additive characteristic of $R$ and $\mathrm{R'}$. Then $x_{2}$ is primitive, if for all elements $a$ of $R$, if $a \neq 0$, then the multiplicative shift of $x_{2}$ and $a$ is distinct from $1$.
AddChar.PrimitiveAddCharstructureMathlib.NumberTheory.LegendreSymbol.AddCharacter, typeWording
primitive additive characteristic of R and #2 (from the name)
English
Let $R$ and $\mathrm{R'}$ be sets. Then the primitive additive characteristics of $R$ and $\mathrm{R'}$ are a basic type.
AddChar.PrimitiveAddChar.chardefMathlib.NumberTheory.LegendreSymbol.AddCharacter, function or constantWording
the characteristic of self (from the name)
English
Let $\mathrm{self}$ be a primitive additive characteristic of $R$ and $\mathrm{R'}$. Then the characteristic of $\mathrm{self}$ is an additive characteristic of $R$ and the set of cyclotomic fields of the value of $\operatorname{n}$ applied to $\mathrm{self}$ and $\mathrm{R'}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
AddChar.PrimitiveAddChar.ndefMathlib.NumberTheory.LegendreSymbol.AddCharacter, function or constantEnglish
Let $\mathrm{self}$ be a primitive additive characteristic of $R$ and $\mathrm{R'}$. Then $\operatorname{n}$ applied to $\mathrm{self}$ is a positive natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AddChar.primitiveZModChardefMathlib.NumberTheory.LegendreSymbol.AddCharacter, function or constantEnglish
Let $n$ be a positive natural number. Let $\mathrm{F'}$ be a set. Assume that the value of $n$ is distinct from $0$. Then $\operatorname{primitiveZModChar}$ applied to $n$, $\mathrm{F'}$ and $h$ is a primitive additive characteristic of $\mathrm{ZMod}$ applied to the value of $n$ and $\mathrm{F'}$.
AddChar.zmodChardefMathlib.NumberTheory.LegendreSymbol.AddCharacter, function or constantWording
the integer modulo characteristic of n and h1 (from the name)
English
Let $n$ be a natural number such that $\EqtMACRoH {x_{1} ^ {n}}{1}$. Then the integer modulo characteristic of $n$ and $h_{1}$ is an additive characteristic of $\mathrm{ZMod}$ applied to $n$ and $C$.
legendreSymdefMathlib.NumberTheory.LegendreSymbol.Basic, function or constantWording
the Legendre symmetric power of p and a (from the name)
English
Let $p$ be a natural number. Let $a$ be an integer. Then the Legendre symmetric power of $p$ and $a$ is an integer defined as $\operatorname{quadraticChar}$ applied to $\mathrm{ZMod}$ applied to $p$ and $a$.
legendreSym.homdefMathlib.NumberTheory.LegendreSymbol.Basic, function or constantWording
the homomorphism of p (from the name)
English
Let $p$ be a natural number. Then the homomorphism of $p$ is a monoid with zero homomorphism of $\Integer$ and $\Integer$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{legendreSym}$ applied to $p$ and $\mathrm{legendreSym\_\_at\_zero}$ applied to $p$, $\mathrm{legendreSym\_\_at\_one}$ applied to $p$ and $\operatorname{mul}$ applied to $p$.
AddChar.FiniteField.primitiveChar_to_ComplexdefMathlib.NumberTheory.LegendreSymbol.Complex, function or constantWording
the primitive characteristic to complex of F (from the name)
English
Let $F$ be a set. Then the primitive characteristic to complex of $F$ is an additive characteristic of $F$ and the set of complexes.
jacobiSymdefMathlib.NumberTheory.LegendreSymbol.JacobiSymbol, function or constantWording
the Jacobi symbol of a and b (from the docstring)
English
Let $a$ be an integer. Let $b$ be a natural number. Then the Jacobi symbol of $a$ and $b$ is an integer defined as $\operatorname{prod}$ applied to $\operatorname{pmap}$ applied to the function that maps $p$ and $\mathrm{pp}$ to the Legendre symmetric power of $p$ and $a$, the prime factorization of $b$ and the function that maps $x$ and $\mathrm{pf}$ to $\mathrm{Nat\_\_prime\_of\_mem\_primeFactorsList}$ applied to $\mathrm{pf}$.
qrSigndefMathlib.NumberTheory.LegendreSymbol.JacobiSymbol, function or constantEnglish
Let $m$ and $n$ be natural numbers. Then $\mathrm{qrSign}$ applied to $m$ and $n$ is an integer defined as the Jacobi symbol of $\mathrm{ZMod\_\_\_u3c7\_\_u2084\_\_\_app}$ applied to $m$ and $n$.
quadraticChardefMathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic, function or constantWording
the quadratic character of F (from the docstring)
English
Let $F$ be a set. Then the quadratic character of $F$ is a multiplicative characteristic of $F$ and $\Integer$.
quadraticCharFundefMathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic, function or constantWording
the quadratic characteristic function of x and a (from the name)
English
Let $x$ be a set. Let $a$ be an element of $x$. Then the quadratic characteristic function of $x$ and $a$ is an element of $\Integer$ defined as $\iteMACRoG {(\EqtMACRoH {a}{0})}{0}{(\iteMACRoG {\mathrm{IsSquare} (a)}{1}{\operatorname{neg} (1)})}$.
ZMod.χ₄defMathlib.NumberTheory.LegendreSymbol.ZModChar, function or constantEnglish
$\mathrm{ZMod\_\_\_u3c7\_\_u2084\_}$ is a multiplicative characteristic of $\mathrm{ZMod}$ applied to $4$ and $\Integer$.
ZMod.χ₈defMathlib.NumberTheory.LegendreSymbol.ZModChar, function or constantEnglish
$\mathrm{ZMod\_\_\_u3c7\_\_u2088\_}$ is a multiplicative characteristic of $\mathrm{ZMod}$ applied to $8$ and $\Integer$.
ZMod.χ₈'defMathlib.NumberTheory.LegendreSymbol.ZModChar, function or constantEnglish
$\mathrm{ZMod\_\_\_u3c7\_\_u2088\_'}$ is a multiplicative characteristic of $\mathrm{ZMod}$ applied to $8$ and $\Integer$.
IsNonarchimedeanLocalFieldclassMathlib.NumberTheory.LocalField.Basic, predicateWording
K is a nonarchimedean local field (from the name)
English
Let $K$ be a set. Then we can say that $K$ is a nonarchimedean local field.
IsNonarchimedeanLocalField.valueGroupWithZeroIsoIntdefMathlib.NumberTheory.LocalField.Basic, function or constantWording
the value group of K (from the docstring)
English
Let $K$ be a set. Then the value group of $K$ is an order monoid isomorphism of the set of value groups with zero of $K$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$.
LucasLehmer.LucasLehmerTestdefMathlib.NumberTheory.LucasLehmer, predicateEnglish
Let $p$ be a natural number. Then $\operatorname{LucasLehmerTest}$ holds for $p$, if $\EqtMACRoH {\operatorname{lucasLehmerResidue} (p)}{0}$.
LucasLehmer.XdefMathlib.NumberTheory.LucasLehmer, typeEnglish
Let $q$ be a natural number. Then an element of $\operatorname{X}$ applied to $q$ is an element of the function that maps $q$ to $\mathrm{Prod}$ applied to $\mathrm{ZMod}$ applied to $q$ and $\mathrm{ZMod}$ applied to $q$.
LucasLehmer.X.αdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
$\mathrm{LucasLehmer\_\_X\_\_\_u3b1\_}$ is an element of $\operatorname{X}$ applied to $q$ defined as $\ProdmkMACRoU {0}{1}$.
LucasLehmer.X.ωdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
$\mathrm{LucasLehmer\_\_X\_\_\_u3c9\_}$ is an element of $\operatorname{X}$ applied to $q$ defined as $\ProdmkMACRoU {2}{1}$.
LucasLehmer.X.ωbdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
$\mathrm{LucasLehmer\_\_X\_\_\_u3c9\_b}$ is an element of $\operatorname{X}$ applied to $q$ defined as $\ProdmkMACRoU {2}{\operatorname{neg} (1)}$.
LucasLehmer.lucasLehmerResiduedefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $p$ be a natural number. Then $\operatorname{lucasLehmerResidue}$ applied to $p$ is an element of $\mathrm{ZMod}$ applied to $2 ^ {p}- 1$ defined as $\operatorname{sZMod}$ applied to $p$ and $p - 2$.
LucasLehmer.norm_num_ext.evalLucasLehmerTestdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
$\mathrm{LucasLehmer\_\_norm\_num\_ext\_\_evalLucasLehmerTest}$ is an element of $\operatorname{NormNumExt}$.
LucasLehmer.norm_num_ext.sModNatdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $q$ and $x$ be natural numbers. Then $\mathrm{LucasLehmer\_\_norm\_num\_ext\_\_sModNat}$ applied to $q$ and $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{LucasLehmer\_\_norm\_num\_ext\_\_sModNat\_\_\_f}$ applied to $q$.
LucasLehmer.norm_num_ext.sModNatTRdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $q$ and $k$ be natural numbers. Then $\mathrm{LucasLehmer\_\_norm\_num\_ext\_\_sModNatTR}$ applied to $q$ and $k$ is a natural number defined as $\mathrm{LucasLehmer\_\_norm\_num\_ext\_\_sModNatTR\_\_go}$ applied to $q$, $k$ and $\HModhModMACRoF {4}{q}$.
LucasLehmer.qdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $p$ be a natural number. Then $\operatorname{q}$ applied to $p$ is a positive natural number defined as the smallest prime factor of $\mathrm{mersenne}$ applied to $p$.
LucasLehmer.sdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $x$ be a natural number. Then $\operatorname{s}$ applied to $x$ is an integer defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{LucasLehmer\_\_s\_\_\_f}$.
LucasLehmer.sModdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $p$ and $x$ be natural numbers. Then $\operatorname{sMod}$ applied to $p$ and $x$ is an integer defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{LucasLehmer\_\_sMod\_\_\_f}$ applied to $p$.
LucasLehmer.sZModdefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $p$ and $x$ be natural numbers. Then $\operatorname{sZMod}$ applied to $p$ and $x$ is an element of $\mathrm{ZMod}$ applied to $2 ^ {p}- 1$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{LucasLehmer\_\_sZMod\_\_\_f}$ applied to $p$.
LucasLehmer.ωUnitdefMathlib.NumberTheory.LucasLehmer, function or constantWording
the unit of p (from the name)
English
Let $p$ be a natural number. Then the unit of $p$ is a unit of $\operatorname{X}$ applied to the value of $\operatorname{q}$ applied to $p$.
mersennedefMathlib.NumberTheory.LucasLehmer, function or constantEnglish
Let $p$ be a natural number. Then $\mathrm{mersenne}$ applied to $p$ is a natural number defined as $2 ^ {p}- 1$.
Polynomial.boxPolydefMathlib.NumberTheory.MahlerMeasure, function or constantEnglish
Let $n$ be a natural number. Let $x$ and $x_{1}$ be functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to real numbers. Then $\operatorname{boxPoly}$ applied to $n$, $x$ and $x_{1}$ is an element of the power set of the set of polynomials of $\Integer$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that the natural degree of $p$ is less than or equal to $n$ and for all elements $i$ of $\mathrm{Fin}$ applied to the sum of $n$ and $1$, $x (i)\leq \operatorname{coeff} (p , \operatorname{val} (i))$ and $\operatorname{coeff} (p , \operatorname{val} (i))\leq x_{1} (i)$.
Nat.GrahamConjecturedefMathlib.NumberTheory.MaricaSchoenheim, predicateEnglish
Let $n$ be a natural number. Let $f$ be a function from natural numbers to natural numbers. Then $\operatorname{GrahamConjecture}$ holds for $n$ and $f$, if if $n \neq 0$, then if $\mathrm{StrictMonoOn}$ holds for $f$ and $\operatorname{Iio}$ applied to $n$, then there exists a natural number $i$, such that $i < n$ and there exists a natural number $j$ such that $j < n$ and the product of the greatest common divisor of $f$ applied to $i$ and $f$ applied to $j$ and $n$ is less than or equal to $f$ applied to $i$.
ModularGroup.fddefMathlib.NumberTheory.Modular, function or constantEnglish
$\operatorname{fd}$ is an element of the power set of the set of upper half planes defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that $1$ is less than or equal to $\operatorname{normSq}$ applied to the coercion of $z$ and the absolute value of the real part of $z$ is less than or equal to $\frac{ 1}{2}$.
ModularGroup.fdodefMathlib.NumberTheory.Modular, function or constantEnglish
$\operatorname{fdo}$ is an element of the power set of the set of upper half planes defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that $1$ is less than $\operatorname{normSq}$ applied to the coercion of $z$ and the absolute value of the real part of $z$ is less than $\frac{ 1}{2}$.
ModularGroup.lcRow0defMathlib.NumberTheory.Modular, function or constantEnglish
Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to elements of $\Integer$. Then $\operatorname{lcRow0}$ applied to $p$ is a linear map of the set of matrixes of $\mathrm{Fin}$ applied to $2$ and $\Real$ and $\Real$ defined as the composition of $\HSMulhSMulMACRoAL {p (0)}{\operatorname{proj} (0)}+ \HSMulhSMulMACRoAL {p (1)}{\operatorname{proj} (1)}$ and the projection of $0$.
ModularGroup.lcRow0ExtenddefMathlib.NumberTheory.Modular, function or constantEnglish
Assume that $\mathrm{cd}$ applied to $0$ is coprime to $\mathrm{cd}$ applied to $1$. Then $\operatorname{lcRow0Extend}$ applied to $\mathrm{hcd}$ is a linear equivalence of the set of matrixes of $\mathrm{Fin}$ applied to $2$ and $\Real$ and the set of matrixes of $\mathrm{Fin}$ applied to $2$ and $\Real$.
ModularGroup.truncatedFundamentalDomaindefMathlib.NumberTheory.Modular, function or constantWording
the truncated fundamental domain of y (from the name)
English
Let $y$ be a real number. Then the truncated fundamental domain of $y$ is an element of the power set of the set of upper half planes defined as $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that $x$ is an element of $\operatorname{fd}$ and the imaginary part of $x$ is less than or equal to $y$.
Subgroup.HasDetOneclassMathlib.NumberTheory.ModularForms.ArithmeticSubgroups, predicateWording
x3 has determinant ones (from the name)
English
Let $x_{3}$ be a subgroup of the set of general linear groups of $n$ and $R$. Then we can say that $x_{3}$ has determinant ones.
Subgroup.HasDetPlusMinusOneclassMathlib.NumberTheory.ModularForms.ArithmeticSubgroups, predicateWording
x3 has determinant plus minus ones (from the name)
English
Let $x_{3}$ be a subgroup of the set of general linear groups of $n$ and $R$. Then we can say that $x_{3}$ has determinant plus minus ones.
Subgroup.IsArithmeticclassMathlib.NumberTheory.ModularForms.ArithmeticSubgroups, predicateWording
x is arithmetic (from the name)
English
Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then we can say that $x$ is arithmetic.
Subgroup.adjoinNegOnedefMathlib.NumberTheory.ModularForms.ArithmeticSubgroups, function or constantEnglish
Let $x_{2}$ be a subgroup of $G$. Then $\operatorname{adjoinNegOne}$ applied to $x_{2}$ is a subgroup of $G$.
Subgroup.detOnePartdefMathlib.NumberTheory.ModularForms.ArithmeticSubgroups, function or constantWording
the determinant one part of G (from the name)
English
Let $G$ be a subgroup of the set of general linear groups of $n$ and $R$. Then the determinant one part of $G$ is a subgroup of the set of general linear groups of $n$ and $R$ defined as the minimum of $G$ and the range of $\operatorname{toGL}$.
OnePoint.IsBoundedAtdefMathlib.NumberTheory.ModularForms.BoundedAtCusp, predicateEnglish
Let $c$ be an one point of $\Real$. Let $f$ be a function from upper half planes to complexes. Let $k$ be an element of $\Integer$. Then $\operatorname{IsBoundedAt}$ holds for $c$, $f$ and $k$, if for all general linear groups $g$ of $\mathrm{Fin}$ applied to $2$ and $\Real$, if $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{\operatorname{infty}}}{c}$, then the map of $g$ and $f$ is bounded at imaginary part infty.
OnePoint.IsZeroAtdefMathlib.NumberTheory.ModularForms.BoundedAtCusp, predicateEnglish
Let $c$ be an one point of $\Real$. Let $f$ be a function from upper half planes to complexes. Let $k$ be an element of $\Integer$. Then $\operatorname{IsZeroAt}$ holds for $c$, $f$ and $k$, if for all general linear groups $g$ of $\mathrm{Fin}$ applied to $2$ and $\Real$, if $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{\operatorname{infty}}}{c}$, then the map of $g$ and $f$ is a zero at imaginary part infty.
CongruenceSubgroup.GammadefMathlib.NumberTheory.ModularForms.CongruenceSubgroups, function or constantWording
the Gamma of N (from the name)
English
Let $N$ be a natural number. Then the Gamma of $N$ is a subgroup of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$ defined as the multiplicative kernel of the map of the cast ring homomorphism of $\mathrm{ZMod}$ applied to $N$.
CongruenceSubgroup.Gamma0defMathlib.NumberTheory.ModularForms.CongruenceSubgroups, function or constantWording
the Gamma of N (from the name)
English
Let $N$ be a natural number. Then the Gamma of $N$ is a subgroup of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$.
CongruenceSubgroup.Gamma0MapdefMathlib.NumberTheory.ModularForms.CongruenceSubgroups, function or constantWording
the Gamma map of N (from the name)
English
Let $N$ be an element of $\Natural$. Then the Gamma map of $N$ is a monoid homomorphism of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{Gamma0} (N)}{x})}$ and $\mathrm{ZMod}$ applied to $N$.
CongruenceSubgroup.Gamma1defMathlib.NumberTheory.ModularForms.CongruenceSubgroups, function or constantWording
the Gamma of N (from the name)
English
Let $N$ be a natural number. Then the Gamma of $N$ is a subgroup of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$ defined as the map of the composition of the subtype of the Gamma of $N$ and the subtype of the Gamma of $N$ and the top.
CongruenceSubgroup.Gamma1'defMathlib.NumberTheory.ModularForms.CongruenceSubgroups, function or constantWording
the Gamma of N (from the name)
English
Let $N$ be an element of $\Natural$. Then the Gamma of $N$ is a subgroup of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{Gamma0} (N)}{x})}$ defined as the multiplicative kernel of the Gamma map of $N$.
CongruenceSubgroup.IsCongruenceSubgroupdefMathlib.NumberTheory.ModularForms.CongruenceSubgroups, predicateWording
x is a congruence subgroup (from the name)
English
Let $x$ be a subgroup of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$. Then $x$ is a congruence subgroup, if there exists a natural number $N$, such that $N \neq 0$ and the Gamma of $N$ is less than or equal to $x$.
CongruenceSubgroup.conjGLdefMathlib.NumberTheory.ModularForms.CongruenceSubgroups, function or constantEnglish
Let $x$ be a subgroup of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$. Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then $\operatorname{conjGL}$ applied to $x$ and $g$ is a subgroup of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$ defined as the preimage of $\operatorname{mapGL}$ applied to $\Real$ and $\HSMulhSMulMACRoAL {\operatorname{toConjAct} (\operatorname{inv} (g))}{\operatorname{map} (\operatorname{mapGL} (\Real), x)}$.
CuspOrbitsdefMathlib.NumberTheory.ModularForms.Cusps, typeWording
cusp orbit of x (from the name)
English
Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then a cusp orbit of $x$ is an element of the function that maps $x$ to the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {x}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{cuspsSubMulAction} (x)}{x_{2}})}$.
IsCuspdefMathlib.NumberTheory.ModularForms.Cusps, predicateEnglish
Let $c$ be an one point of $\Real$. Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then $\mathrm{IsCusp}$ holds for $c$ and $x$, if there exists a general linear group $g$ of $\mathrm{Fin}$ applied to $2$ and $\Real$, such that $g$ is an element of $x$, $g$ is parabolic and $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{c}}{c}$.
Subgroup.IsRegularAtInftydefMathlib.NumberTheory.ModularForms.Cusps, predicateWording
x1 is a regular at infty (from the name)
English
Let $x_{1}$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $R$. Then $x_{1}$ is a regular at infty, if the strict period of $x_{1}$ is equal to the period of $x_{1}$.
Subgroup.periodsdefMathlib.NumberTheory.ModularForms.Cusps, function or constantWording
the period of x1 (from the name)
English
Let $x_{1}$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $R$. Then the period of $x_{1}$ is an additive subgroup of $R$ defined as the strict period of $\operatorname{adjoinNegOne}$ applied to $x_{1}$.
Subgroup.strictPeriodsdefMathlib.NumberTheory.ModularForms.Cusps, function or constantWording
the strict period of x1 (from the name)
English
Let $x_{1}$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $R$. Then the strict period of $x_{1}$ is an additive subgroup of $R$ defined as the preimage of the additive monoid homomorphism of the upper right homomorphism and $\operatorname{toAddSubgroup}$ applied to $x_{1}$.
Subgroup.strictWidthInftydefMathlib.NumberTheory.ModularForms.Cusps, function or constantWording
the strict width of the cusp of x (from the docstring)
English
Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then the strict width of the cusp of $x$ is a real number.
Subgroup.widthInftydefMathlib.NumberTheory.ModularForms.Cusps, function or constantWording
the width of the cusp of x (from the docstring)
English
Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then the width of the cusp of $x$ is a real number defined as the strict width of the cusp of $\operatorname{adjoinNegOne}$ applied to $x$.
cosetToCuspOrbitdefMathlib.NumberTheory.ModularForms.Cusps, function or constantWording
the coset to cusp orbit of x and x1 (from the name)
English
Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Let $x_{1}$ be a quotient of the set of special linear groups of $\mathrm{Fin}$ applied to $2$ and $\Integer$ and the preimage of $\operatorname{mapGL}$ applied to $\Real$ and $x$. Then the coset to cusp orbit of $x$ and $x_{1}$ is a cusp orbit of $x$.
cuspsSubMulActiondefMathlib.NumberTheory.ModularForms.Cusps, function or constantWording
the action of x (from the docstring)
English
Let $x$ be a subgroup of the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then the action of $x$ is a difference multiplicative action of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {x}{x_{1}})}$ and the set of one points of $\Real$.
Derivative.normalizedDerivOfComplexdefMathlib.NumberTheory.ModularForms.Derivative, function or constantWording
the normalized derivative of F and z (from the name)
English
Let $F$ be a function from upper half planes to complexes. Let $z$ be a upper half plane. Then the normalized derivative of $F$ and $z$ is a complex defined as the product of $\operatorname{inv}$ applied to the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product and $\operatorname{I}$ and the derivative of $\operatorname{comp}$ applied to $F$ and $\operatorname{toFun'}$ applied to the upper half plane and the coercion of $z$.
Derivative.serreDerivativedefMathlib.NumberTheory.ModularForms.Derivative, function or constantEnglish
Let $k$ be a complex. Let $F$ be a function from upper half planes to complexes. Let $z$ be a upper half plane. Then $\operatorname{serreDerivative}$ applied to $k$, $F$ and $z$ is a complex defined as the difference between the normalized derivative of $F$ and $z$ and $k \times \operatorname{inv} (12)\times \operatorname{E2} (z)\times F (z)$.
Derivative.serreDerivativeMFdefMathlib.NumberTheory.ModularForms.Derivative, function or constantEnglish
Let $k$ be an integer. Let $f$ be a modular form of $x$ and $k$. Assume that $\mathrm{autoParam}$ holds for the proposition that $x$ is less than or equal to the range of $\operatorname{mapGL}$ applied to $\Real$ and $\mathrm{Derivative\_\_serreDerivativeMF\_\_\_auto\_1}$. Then $\operatorname{serreDerivativeMF}$ applied to $k$, $f$ and $h$ is a modular form of $x$ and $k + 2$.
EisensteinSeries.divIntMapdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the quotient integer map of v and x (from the name)
English
Let $r$ be an integer. Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to integers. Let $x$ be an element of $\mathrm{Fin}$ applied to $m$. Then the quotient integer map of $v$ and $x$ is an integer defined as $\mathrm{div} (v , r , x)$.
EisensteinSeries.eisSummanddefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantEnglish
Let $k$ be an integer. Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to integers. Let $z$ be a upper half plane. Then $\operatorname{eisSummand}$ applied to $k$, $v$ and $z$ is a complex defined as the exponentiation of the sum of the product of $v$ applied to $0$ and the coercion of $z$ and $v$ applied to $1$ to $\operatorname{neg}$ applied to $k$.
EisensteinSeries.eisensteinSeriesSIFdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantEnglish
Let $a$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to elements of $\mathrm{ZMod}$ applied to $N$. Let $k$ be an integer. Then $\operatorname{eisensteinSeriesSIF}$ applied to $a$ and $k$ is an element of $\mathrm{SlashInvariantForm}$ applied to the map of $\operatorname{mapGL}$ applied to $\Real$ and the Gamma of $N$ and $k$.
EisensteinSeries.finGcdMapdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the finite greatest common divisor map of v (from the name)
English
Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to integers. Then the finite greatest common divisor map of $v$ is a natural number defined as $\operatorname{gcd}$ applied to $v$ applied to $0$ and $v$ applied to $1$.
EisensteinSeries.gammaSetdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the Gamma set of r and a (from the name)
English
Let $N$ and $r$ be natural numbers. Let $a$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to elements of $\mathrm{ZMod}$ applied to $N$. Then the Gamma set of $r$ and $a$ is an element of $\wp (\mathrm{Elem} (\mathrm{Fin} (2))\rightarrow \Integer)$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that $\EqtMACRoH {\operatorname{comp} (\operatorname{toIntCast} , v)}{a}$ and $\operatorname{gcd} (v (0), v (1))= r$.
EisensteinSeries.gammaSetDivGcdEquivdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the Gamma set quotient greatest common divisor equivalence of r (from the name)
English
Let $r$ be a natural number. Then the Gamma set quotient greatest common divisor equivalence of $r$ is an equivalence from the set of elements of the Gamma set of $r$ and $0$ to the set of elements of the Gamma set of $1$ and $0$ defined as the equivalence of $\operatorname{divIntMap}$ and $\mathrm{EisensteinSeries\_\_gammaSet\_div\_gcd\_to\_gammaSet10\_bijection}$ applied to $r$.
EisensteinSeries.gammaSetDivGcdSigmaEquivdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the Gamma set quotient greatest common divisor sigma equivalence (from the name)
English
The Gamma set quotient greatest common divisor sigma equivalence is an equivalence from the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to integers to $\Sigma$ applied to the function that maps $r$ to the set of elements of the Gamma set of $r$ and $0$.
EisensteinSeries.gammaSetEquivdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the Gamma set equivalence of a and x (from the name)
English
Let $a$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to elements of $\mathrm{ZMod}$ applied to $N$. Let $x$ be a special linear group of $\mathrm{Fin}$ applied to $2$ and $\Integer$. Then the Gamma set equivalence of $a$ and $x$ is an equivalence from the set of elements of the Gamma set of $r$ and $a$ to the set of elements of the Gamma set of $r$ and $\operatorname{vecMul}$ applied to $\operatorname{map}$ applied to the cast ring homomorphism of $\mathrm{ZMod}$ applied to $N$ and $x$.
EisensteinSeries.gammaSet_one_equivdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the Gamma set one equivalence of a and #3 (from the name)
English
Let $r$ be a natural number. Let $a$ and $\mathrm{a'}$ be functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $\mathrm{ZMod}$ applied to $1$. Then the Gamma set one equivalence of $a$ and $\mathrm{a'}$ is an equivalence from the set of elements of the Gamma set of $r$ and $a$ to the set of elements of the Gamma set of $r$ and $\mathrm{a'}$ defined as the equivalence of $\mathrm{EisensteinSeries\_\_gammaSet\_one\_const}$ applied to $r$, $a$ and $\mathrm{a'}$.
eisensteinSeriesdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Defs, function or constantWording
the Eisenstein series of k and z (from the name)
English
Let $a$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to elements of $\mathrm{ZMod}$ applied to $N$. Let $k$ be an integer. Let $z$ be a upper half plane. Then the Eisenstein series of $k$ and $z$ is a complex defined as the sum of the function that maps $x$ to $\operatorname{eisSummand}$ applied to $k$, $x$ and $z$ and $\operatorname{unconditional}$ applied to the set of elements of the Gamma set of $1$ and $a$.
EisensteinSeries.D2defMathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs, function or constantEnglish
Let $x$ be a special linear group of $\mathrm{Fin}$ applied to $2$ and $\Integer$. Let $x_{1}$ be a upper half plane. Then $\operatorname{D2}$ applied to $x$ and $x_{1}$ is a complex defined as the quotient of the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$ and $0$ and $\operatorname{denom}$ applied to $\operatorname{toGL}$ applied to $\operatorname{map}$ applied to the cast ring homomorphism of $\Real$ and $x$ and the coercion of $x_{1}$.
EisensteinSeries.E2defMathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs, function or constantEnglish
Let $x$ be a upper half plane. Then $\operatorname{E2}$ applied to $x$ is a complex defined as $\HSMulhSMulMACRoAL {(\frac{ 1}{2 \times \mathrm{riemannZeta} (2)})}{\operatorname{G2}}$.
EisensteinSeries.G2defMathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs, function or constantEnglish
Let $x$ be a upper half plane. Then $\operatorname{G2}$ applied to $x$ is a complex defined as the sum of the function that maps $m$ to the summand of $m$ and $x$ and the symmetric closed interval of $\Integer$.
EisensteinSeries.e2SummanddefMathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs, function or constantWording
the summand of m and z (from the name)
English
Let $m$ be an integer. Let $z$ be a upper half plane. Then the summand of $m$ and $z$ is a complex defined as the sum of the function that maps $n$ to $\operatorname{eisSummand}$ applied to $2$, $\operatorname{vecCons}$ applied to $m$ and $\operatorname{vecCons}$ applied to $n$ and $\operatorname{vecEmpty}$ and $z$ and $\operatorname{unconditional}$ applied to $\Integer$.
EisensteinSeries.rdefMathlib.NumberTheory.ModularForms.EisensteinSeries.Summable, function or constantEnglish
Let $z$ be a upper half plane. Then $\operatorname{r}$ applied to $z$ is a real number defined as the minimum of the imaginary part of $z$ and the square root of $\operatorname{r1}$ applied to $z$.
HurwitzKernelBounds.F_intdefMathlib.NumberTheory.ModularForms.JacobiTheta.Bounds, function or constantWording
the integer of a and t (from the name)
English
Let $k$ be a natural number. Let $a$ be a unit circle. Let $t$ be a real number. Then the integer of $a$ and $t$ is a real number.
HurwitzKernelBounds.F_natdefMathlib.NumberTheory.ModularForms.JacobiTheta.Bounds, function or constantWording
the natural number of a and t (from the name)
English
Let $k$ be a natural number. Let $a$ and $t$ be real numbers. Then the natural number of $a$ and $t$ is a real number defined as the sum of the function that maps $n$ to the natural number of $t$ and $n$ and $\operatorname{unconditional}$ applied to $\Natural$.
HurwitzKernelBounds.f_intdefMathlib.NumberTheory.ModularForms.JacobiTheta.Bounds, function or constantWording
the integer of t and n (from the name)
English
Let $k$ be a natural number. Let $a$ and $t$ be real numbers. Let $n$ be an integer. Then the integer of $t$ and $n$ is a real number defined as the product of the exponentiation of the absolute value of $n + a$ to $k$ and the exponential of the product of $\operatorname{neg}$ applied to the product, $(n + a)^ {2}$ and $t$.
HurwitzKernelBounds.f_natdefMathlib.NumberTheory.ModularForms.JacobiTheta.Bounds, function or constantWording
the natural number of t and n (from the name)
English
Let $k$ and $n$ be natural numbers. Let $a$ and $t$ be real numbers. Then the natural number of $t$ and $n$ is a real number defined as the product of $(n + a)^ {k}$ and the exponential of the product of $\operatorname{neg}$ applied to the product, $(n + a)^ {2}$ and $t$.
HurwitzKernelBounds.g_natdefMathlib.NumberTheory.ModularForms.JacobiTheta.Bounds, function or constantWording
the natural number of t and n (from the name)
English
Let $k$ and $n$ be natural numbers. Let $a$ and $t$ be real numbers. Then the natural number of $t$ and $n$ is a real number defined as the product of $(n + a)^ {k}$ and the exponential of the product of $\operatorname{neg}$ applied to the product, $n + a ^ {2}$ and $t$.
jacobiThetadefMathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable, function or constantWording
the Jacobi theta of x (from the name)
English
Let $x$ be a complex. Then the Jacobi theta of $x$ is a complex defined as the sum of the function that maps $n$ to the exponential of the product of the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$, $n ^ {2}$ and $x$ and $\operatorname{unconditional}$ applied to $\Integer$.
jacobiTheta₂defMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable, function or constantWording
the Jacobi theta of z and x (from the name)
English
Let $z$ and $x$ be complexes. Then the Jacobi theta of $z$ and $x$ is a complex defined as the sum of the function that maps $n$ to the Jacobi theta term of $z$ and $x$ and $\operatorname{unconditional}$ applied to $\Integer$.
jacobiTheta₂'defMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable, function or constantWording
the Jacobi theta of z and x (from the name)
English
Let $z$ and $x$ be complexes. Then the Jacobi theta of $z$ and $x$ is a complex defined as the sum of the function that maps $n$ to the Jacobi theta term of $z$ and $x$ and $\operatorname{unconditional}$ applied to $\Integer$.
jacobiTheta₂'_termdefMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable, function or constantWording
the Jacobi theta term of z and x (from the name)
English
Let $n$ be an integer. Let $z$ and $x$ be complexes. Then the Jacobi theta term of $z$ and $x$ is a complex defined as the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$, $n$ and the Jacobi theta term of $z$ and $x$.
jacobiTheta₂_fderivdefMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable, function or constantWording
the Jacobi theta derivative of z and x (from the name)
English
Let $z$ and $x$ be complexes. Then the Jacobi theta derivative of $z$ and $x$ is a continuous linear map of $\mathrm{Prod}$ applied to the set of complexes and the set of complexes and the set of complexes defined as the sum of the function that maps $n$ to the Jacobi theta term derivative of $z$ and $x$ and $\operatorname{unconditional}$ applied to $\Integer$.
jacobiTheta₂_termdefMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable, function or constantWording
the Jacobi theta term of z and x (from the name)
English
Let $n$ be an integer. Let $z$ and $x$ be complexes. Then the Jacobi theta term of $z$ and $x$ is a complex defined as the exponential of the sum of the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$, $n$ and $z$ and the product of the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$, $n ^ {2}$ and $x$.
jacobiTheta₂_term_fderivdefMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable, function or constantWording
the Jacobi theta term derivative of z and x (from the name)
English
Let $n$ be an element of $\Integer$. Let $z$ and $x$ be complexes. Then the Jacobi theta term derivative of $z$ and $x$ is a continuous linear map of $\mathrm{Prod}$ applied to the set of complexes and the set of complexes and the set of complexes defined as $\HSMulhSMulMACRoAL {\operatorname{exp} (2 \times \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I} \times n \times z + \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I} \times n ^ {2}\times x)}{(\HSMulhSMulMACRoAL {(2 \times \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I} \times n)}{\operatorname{fst} (\mathrm{Complex} , \mathrm{Complex})}+ \HSMulhSMulMACRoAL {(\operatorname{ofReal} (\operatorname{pi})\times \operatorname{I} \times n ^ {2})}{\operatorname{snd} (\mathrm{Complex} , \mathrm{Complex})})}$.
UpperHalfPlane.cuspFunctiondefMathlib.NumberTheory.ModularForms.QExpansion, function or constantWording
the cusp function of f and x (from the name)
English
Let $h$ be a real number. Let $f$ be a function from upper half planes to complexes. Let $x$ be a complex. Then the cusp function of $f$ and $x$ is a complex defined as the cusp function of $\operatorname{comp}$ applied to $f$ and $\operatorname{toFun'}$ applied to the upper half plane and $x$.
UpperHalfPlane.qExpansiondefMathlib.NumberTheory.ModularForms.QExpansion, function or constantWording
the expansion of h and f (from the name)
English
Let $h$ be a real number. Let $f$ be a function from upper half planes to complexes. Then the expansion of $h$ and $f$ is a power series of the set of complexes defined as $\operatorname{mk}$ applied to the function that maps $m$ to the product of $\operatorname{inv}$ applied to $m !$ and the iterated derivative of $\operatorname{cuspFunction}$ applied to $f$ and $0$.
UpperHalfPlane.valueAtInftydefMathlib.NumberTheory.ModularForms.QExpansion, function or constantWording
the value at infty of f (from the name)
English
Let $f$ be a function from upper half planes to complexes. Then the value at infty of $f$ is a complex defined as $\operatorname{limUnder}$ applied to $\operatorname{atImInfty}$ and $f$.
SlashActionclassMathlib.NumberTheory.ModularForms.SlashActions, predicateEnglish
Let $x$, $G$ and $x_{1}$ be sets. Then we can say that $\mathrm{SlashAction}$ holds for $x$, $G$ and $x_{1}$.
SlashAction.mapdefMathlib.NumberTheory.ModularForms.SlashActions, function or constantWording
the map of x5 and x6 (from the name)
English
Let $x_{4}$ be an element of $x$. Let $x_{5}$ be an element of $G$. Let $x_{6}$ be an element of $x_{1}$. Then the map of $x_{5}$ and $x_{6}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{4}$, $x_{5}$ and $x_{6}$.