solvableByRaddefMathlib.FieldTheory.AbelRuffini, function or constantEnglish
Let $F$ and $E$ be sets. Then $\mathrm{solvableByRad}$ applied to $F$ and $E$ is an intermediate field of $F$ and $E$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that for all elements $x_{3}$ of $E$, for all natural numbers $n$, if $n \neq 0$, then if $x_{3} ^ {n}$ is an element of $s$, then $x_{3}$ is an element of $s$.
Field.absoluteGaloisGroupdefMathlib.FieldTheory.AbsoluteGaloisGroup, typeWording
absolute Galois group of K (from the name)
English
Let $K$ be a set. Then an absolute Galois group of $K$ is an element of the function that maps $K$ to the set of algebra isomorphisms of the set of algebraic closures of $K$ and the set of algebraic closures of $K$.
Field.absoluteGaloisGroup.mapdefMathlib.FieldTheory.AbsoluteGaloisGroup, function or constantWording
the map of f (from the name)
English
Let $f$ be a ring homomorphism of $K$ and $L$. Then the map of $f$ is a continuous monoid homomorphism of the set of absolute Galois groups of $L$ and the set of absolute Galois groups of $K$ defined as the map of $K$ and $L$.
Field.absoluteGaloisGroup.mapOfAlgebradefMathlib.FieldTheory.AbsoluteGaloisGroup, function or constantWording
the map of K and L (from the name)
English
Let $K$ and $L$ be sets. Then the map of $K$ and $L$ is a continuous monoid homomorphism of the set of absolute Galois groups of $L$ and the set of absolute Galois groups of $K$.
Field.absoluteGaloisGroupAbelianizationdefMathlib.FieldTheory.AbsoluteGaloisGroup, typeWording
absolute Galois group abelianization of K (from the name)
English
Let $K$ be a set. Then an absolute Galois group abelianization of $K$ is an element of the function that maps $K$ to the set of topological abelianizations of the set of absolute Galois groups of $K$.
AlgEquiv.algebraicClosuredefMathlib.FieldTheory.AlgebraicClosure, function or constantWording
the algebraic closure of i (from the name)
English
Let $i$ be an algebra isomorphism of $E$ and $K$. Then the algebraic closure of $i$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{algebraicClosure} (F , E)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{algebraicClosure} (F , K)}{x_{6}})}$ defined as the algebra isomorphism of $i$.
algebraicClosuredefMathlib.FieldTheory.AlgebraicClosure, function or constantWording
the algebraic closure of F and E (from the name)
English
Let $F$ and $E$ be sets. Then the algebraic closure of $F$ and $E$ is an intermediate field of $F$ and $E$ defined as the intermediate field of the integral closure of $F$ and $E$.
algebraicClosure.algEquivOfAlgEquivdefMathlib.FieldTheory.AlgebraicClosure, function or constantWording
the algebra isomorphism of i (from the name)
English
Let $i$ be an algebra isomorphism of $E$ and $K$. Then the algebra isomorphism of $i$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{algebraicClosure} (F , E)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{algebraicClosure} (F , K)}{x_{6}})}$ defined as the composition of the intermediate field map of $i$ and the algebraic closure of $F$ and $E$ and the equivalence of $\mathrm{algebraicClosure\_\_map\_eq\_of\_algEquiv}$ applied to $i$.
FirstOrder.genericPolyMapSurjOnOfInjOndefMathlib.FieldTheory.AxGrothendieck, function or constantEnglish
Let $x_{2}$ be a formula of the ring and $\mathrm{Sum}$ applied to $x_{1}$ and $x$. Let $\mathrm{mons}$ be a function from elements of $x$ to finite sets of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{genericPolyMapSurjOnOfInjOn}$ applied to $x_{2}$ and $\mathrm{mons}$ is a sentence of the ring.
Field.Emb.Cardinal.embEquivPidefMathlib.FieldTheory.CardinalEmb, function or constantWording
the embedding equivalence product (from the name)
English
The embedding equivalence product is an equivalence from the set of embeddings of $F$ and $E$ to the set of functions from types $i$ of the order of the rank of $F$ and $E$ to factors of $\operatorname{some}$ applied to $i$.
Field.Emb.Cardinal.embFunctordefMathlib.FieldTheory.CardinalEmb, function or constantWording
the embedding functor of f (from the name)
English
Let $F$ and $E$ be sets. Assume that $i \leq j$. Let $f$ be an algebra homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{filtration} (j)}{x_{4}})}$ and the set of algebraic closures of $E$. Then the embedding functor of $f$ is an algebra homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{filtration} (i)}{x_{3}})}$ and the set of algebraic closures of $E$.
Field.Emb.Cardinal.equivLimdefMathlib.FieldTheory.CardinalEmb, function or constantWording
the equivalence limit of hi (from the name)
English
Assume that $\operatorname{IsSuccPrelimit}$ holds for $i$. Then the equivalence limit of $\mathrm{hi}$ is an equivalence from the set of algebra homomorphisms of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{filtration} (i)}{x_{3}})}$ and the set of algebraic closures of $E$ to the set of elements of the inverse limit of $\operatorname{embFunctor}$ and $i$.
Field.Emb.Cardinal.equivSuccdefMathlib.FieldTheory.CardinalEmb, function or constantWording
the equivalence successor of i (from the name)
English
Let $i$ be an element of $\mathrm{WithTop}$ applied to the set of types of the order of the rank of $F$ and $E$. Then the equivalence successor of $i$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{filtration} (\operatorname{succ} (i))}{x_{3}})}, \mathrm{AlgebraicClosure} (E))}{\mathrm{Prod} (\mathrm{AlgHom} (\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{filtration} (i)}{x_{4}})}, \mathrm{AlgebraicClosure} (E)), \operatorname{factor} (i))}$.
Field.Emb.Cardinal.factordefMathlib.FieldTheory.CardinalEmb, typeWording
factor of i (from the name)
English
Let $i$ be an element of $\mathrm{WithTop}$ applied to the set of types of the order of the rank of $F$ and $E$. Then a factor of $i$ is an element of the function that maps $i$ to $\operatorname{recTopCoe}$ applied to $\mathrm{PUnit}$, the function that maps $x_{3}$ to the set of embeddings of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (x_{3})))}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (x_{3})))}{x_{6}})}, \operatorname{singleton} (\operatorname{wellOrderedBasis} (F , E , \operatorname{leastExt} (x_{3}))))}{x_{5}})}$ and $i$.
Field.Emb.Cardinal.filtrationdefMathlib.FieldTheory.CardinalEmb, function or constantWording
the filtration (from the name)
English
The filtration is an order embedding of $\mathrm{WithTop}$ applied to the set of types of the order of the rank of $F$ and $E$ and the set of intermediate fields of $F$ and $E$.
Field.Emb.Cardinal.leastExtdefMathlib.FieldTheory.CardinalEmb, function or constantWording
the least extension of x3 (from the name)
English
Let $F$ and $E$ be sets. Let $x_{3}$ be a type of the order of the rank of $F$ and $E$. Then the least extension of $x_{3}$ is a type of the order of the rank of $F$ and $E$.
Field.Emb.Cardinal.succEquivdefMathlib.FieldTheory.CardinalEmb, function or constantWording
the successor equivalence of i (from the name)
English
Let $i$ be a type of the order of the rank of $F$ and $E$. Then the successor equivalence of $i$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (\operatorname{succ} (i))))}{x_{3}})}, \mathrm{AlgebraicClosure} (E))}{\mathrm{Prod} (\mathrm{AlgHom} (\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (i)))}{x_{4}})}, \mathrm{AlgebraicClosure} (E)), \operatorname{Emb} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (i)))}{x_{5}})}, \SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (i)))}{x_{7}})}, \operatorname{singleton} (\operatorname{wellOrderedBasis} (F , E , \operatorname{leastExt} (i))))}{x_{6}})}))}$ defined as the composition of the arrow congruence of the equivalence of $\mathrm{Field\_\_Emb\_\_Cardinal\_\_filtration\_succ}$ applied to $i$ and the identity and the composition of the algebra homomorphism equivalence sigma and the sigma equivalence product of the function that maps $x_{3}$ to the inverse of the embedding equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{image} (\operatorname{comp} (\operatorname{coe} (\operatorname{wellOrderedBasis} (F , E)), \operatorname{leastExt}), \operatorname{Iio} (i)))}{x_{6}})}, \operatorname{singleton} (\operatorname{wellOrderedBasis} (F , E , \operatorname{leastExt} (i))))}{x_{5}})}$ and the set of algebraic closures of $E$.
Field.Emb.Cardinal.wellOrderedBasisdefMathlib.FieldTheory.CardinalEmb, function or constantEnglish
Let $F$ and $E$ be sets. Then $\operatorname{wellOrderedBasis}$ applied to $F$ and $E$ is a basis of $F$ and $E$.
Differential.logDerivdefMathlib.FieldTheory.Differential.Basic, function or constantWording
the logarithmic derivative of a (from the docstring)
English
Let $a$ be an element of $R$. Then the logarithmic derivative of $a$ is an element of $R$ defined as $\frac{ \operatorname{deriv} (a)}{a}$.
IsLiouvilleclassMathlib.FieldTheory.Differential.Liouville, predicateEnglish
Let $F$ and $K$ be sets. Then we can say that $\mathrm{IsLiouville}$ holds for $F$ and $K$.
FinTrdegclassMathlib.FieldTheory.FinTrdeg, predicateEnglish
Let $K$ and $L$ be sets. Then we can say that $\mathrm{FinTrdeg}$ holds for $K$ and $L$.
FiniteField.frobeniusAlgEquivdefMathlib.FieldTheory.Finite.Basic, function or constantWording
the Frobenius algebra isomorphism of p (from the name)
English
Let $K$ and $R$ be sets. Let $p$ be a natural number. Then the Frobenius algebra isomorphism of $p$ is an algebra isomorphism of $R$ and $R$.
FiniteField.frobeniusAlgEquivOfAlgebraicdefMathlib.FieldTheory.Finite.Basic, function or constantWording
the Frobenius algebra isomorphism of K and L (from the name)
English
Let $K$ and $L$ be sets. Then the Frobenius algebra isomorphism of $K$ and $L$ is an algebra isomorphism of $L$ and $L$ defined as $\operatorname{symm}$ applied to the algebra isomorphism equivalence algebra homomorphism of $K$ and $L$ and the Frobenius algebra homomorphism of $K$ and $L$.
FiniteField.frobeniusAlgHomdefMathlib.FieldTheory.Finite.Basic, function or constantWording
the Frobenius algebra homomorphism of K and R (from the name)
English
Let $K$ and $R$ be sets. Then the Frobenius algebra homomorphism of $K$ and $R$ is an algebra homomorphism of $R$ and $R$.
FiniteField.ExtensiondefMathlib.FieldTheory.Finite.Extension, typeWording
extension of p and n (from the name)
English
Let $k$ be a set. Let $p$ and $n$ be natural numbers. Then an extension of $p$ and $n$ is an element of the function that maps $k$, $p$ and $n$ to the set of Galois fields of $p$ and the product of the rank of $\mathrm{ZMod}$ applied to $p$ and $k$ and $n$.
FiniteField.Extension.frobdefMathlib.FieldTheory.Finite.Extension, function or constantEnglish
Let $k$ be a set. Let $p$ and $n$ be natural numbers. Then $\operatorname{frob}$ applied to $k$, $p$ and $n$ is an algebra isomorphism of the set of extensions of $p$ and $n$ and the set of extensions of $p$ and $n$ defined as the Frobenius algebra isomorphism of $k$ and the set of extensions of $p$ and $n$.
FiniteField.algEquivExtensiondefMathlib.FieldTheory.Finite.Extension, function or constantWording
the algebra isomorphism extension of p and n (from the name)
English
Let $k$ and $l$ be sets. Let $p$ and $n$ be natural numbers such that the rank of $k$ and $l$ is equal to $n$. Then the algebra isomorphism extension of $p$ and $n$ is an algebra isomorphism of $l$ and the set of extensions of $p$ and $n$.
FiniteField.algEquivOfCardEqdefMathlib.FieldTheory.Finite.GaloisField, function or constantWording
the algebra isomorphism of p and #2 (from the name)
English
Let $p$ be a natural number. Assume that the cardinality of $K$ is equal to the cardinality of $\mathrm{K'}$. Then the algebra isomorphism of $p$ and $\mathrm{hKK'}$ is an algebra isomorphism of $K$ and $\mathrm{K'}$.
FiniteField.ringEquivOfCardEqdefMathlib.FieldTheory.Finite.GaloisField, function or constantWording
the ring isomorphism of #1 (from the name)
English
Assume that the cardinality of $K$ is equal to the cardinality of $\mathrm{K'}$. Then the ring isomorphism of $\mathrm{hKK'}$ is a ring isomorphism of $K$ and $\mathrm{K'}$.
GaloisFielddefMathlib.FieldTheory.Finite.GaloisField, typeWording
Galois field of p and n (from the name)
English
Let $p$ and $n$ be natural numbers. Then a Galois field of $p$ and $n$ is an element of the function that maps $p$ and $n$ to the set of splitting fields of $\operatorname{X} ^ {p ^ {n}}- \operatorname{X}$.
GaloisField.algEquivGaloisFielddefMathlib.FieldTheory.Finite.GaloisField, function or constantWording
the algebra isomorphism Galois field of p and n (from the name)
English
Let $p$ and $n$ be natural numbers such that the cardinality of $K$ is equal to $p ^ {n}$. Then the algebra isomorphism Galois field of $p$ and $n$ is an algebra isomorphism of $K$ and the set of Galois fields of $p$ and $n$ defined as the algebra isomorphism of $K$ and $\operatorname{X} ^ {p ^ {n}}- \operatorname{X}$.
GaloisField.algEquivGaloisFieldOfFintypedefMathlib.FieldTheory.Finite.GaloisField, function or constantWording
the algebra isomorphism Galois field of p and n (from the name)
English
Let $p$ and $n$ be natural numbers such that the cardinality of $K$ is equal to $p ^ {n}$. Then the algebra isomorphism Galois field of $p$ and $n$ is an algebra isomorphism of $K$ and the set of Galois fields of $p$ and $n$ defined as the algebra isomorphism of $K$ and $\operatorname{X} ^ {p ^ {n}}- \operatorname{X}$.
GaloisField.equivZmodPdefMathlib.FieldTheory.Finite.GaloisField, function or constantWording
the equivalence integer modulo of p (from the name)
English
Let $p$ be a natural number. Then the equivalence integer modulo of $p$ is an algebra isomorphism of the set of Galois fields of $p$ and $1$ and $\mathrm{ZMod}$ applied to $p$ defined as the inverse of the algebra isomorphism of $\mathrm{ZMod}$ applied to $p$ and $\operatorname{X} ^ {p ^ {1}}- \operatorname{X}$.
MvPolynomial.RdefMathlib.FieldTheory.Finite.Polynomial, typeEnglish
Let $x$ and $K$ be sets. Then an element of $\operatorname{R}$ applied to $x$ and $K$ is an element of the function that maps $x$ and $K$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{restrictDegree} (x , K , \operatorname{card} (K)- 1)}{x_{3}})}$.
MvPolynomial.evalᵢdefMathlib.FieldTheory.Finite.Polynomial, function or constantWording
the evaluation of x and K (from the name)
English
Let $x$ and $K$ be sets. Then the evaluation of $x$ and $K$ is a linear map of $\operatorname{R}$ applied to $x$ and $K$ and the set of functions from functions from elements of $x$ to elements of $K$ to elements of $K$ defined as the composition of the evaluation of $K$ and $x$ and the subtype of $\operatorname{restrictDegree}$ applied to $x$, $K$ and the difference between the cardinality of $K$ and $1$.
MvPolynomial.evalₗdefMathlib.FieldTheory.Finite.Polynomial, function or constantWording
the evaluation of K and x (from the name)
English
Let $K$ and $x$ be sets. Then the evaluation of $K$ and $x$ is a linear map of the set of multivariate polynomials of $x$ and $K$ and the set of functions from functions from elements of $x$ to elements of $K$ to elements of $K$.
MvPolynomial.indicatordefMathlib.FieldTheory.Finite.Polynomial, function or constantWording
the indicator of a (from the name)
English
Let $a$ be a function from elements of $x$ to elements of $K$. Then the indicator of $a$ is a multivariate polynomial of $x$ and $K$ defined as $\FinsetProd {\FinsetunivMACRoAC}{n}{(1 - (\operatorname{X} (n)- \operatorname{C} (a (n)))^ {(\operatorname{card} (K)- 1)})}$.
IsNoetherian.finsetBasisdefMathlib.FieldTheory.Finiteness, function or constantWording
the finite set basis of K and V (from the name)
English
Let $K$ and $V$ be sets. Then the finite set basis of $K$ and $V$ is a basis of $K$ and $V$.
IsNoetherian.finsetBasisIndexdefMathlib.FieldTheory.Finiteness, function or constantWording
the finite set basis index of K and V (from the name)
English
Let $K$ and $V$ be sets. Then the finite set basis index of $K$ and $V$ is a finite set of $V$.
FixedBy.subfielddefMathlib.FieldTheory.Fixed, function or constantWording
the subfield of F and m (from the name)
English
Let $F$ be a set. Let $m$ be an element of $M$. Then the subfield of $F$ and $m$ is a subfield of $F$.
FixedPoints.minpolydefMathlib.FieldTheory.Fixed, function or constantWording
the minimal polynomial of G (from the docstring)
English
Let $G$ and $F$ be sets. Let $x_{4}$ be an element of $F$. Then the minimal polynomial of $G$ is a polynomial of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{subfield} (G , F)}{x_{5}})}$.
FixedPoints.subfielddefMathlib.FieldTheory.Fixed, function or constantWording
the subfield of M and F (from the name)
English
Let $M$ and $F$ be sets. Then the subfield of $M$ and $F$ is a subfield of $F$.
FixedPoints.toAlgAutMulEquivdefMathlib.FieldTheory.Fixed, function or constantWording
the algebra automorphism multiplicative equivalence of G and F (from the name)
English
Let $G$ and $F$ be sets. Then the algebra automorphism multiplicative equivalence of $G$ and $F$ is a multiplicative equivalence of $G$ and the set of algebra isomorphisms of $F$ and $F$ defined as the multiplicative equivalence of the algebra automorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{subfield} (G , F)}{x_{3}})}$ and $F$ and $\mathrm{FixedPoints\_\_toAlgAut\_bijective}$ applied to $G$ and $F$.
FixedPoints.toAlgHomEquivdefMathlib.FieldTheory.Fixed, function or constantWording
the algebra homomorphism equivalence of G and F (from the name)
English
Let $G$ and $F$ be sets. Then the algebra homomorphism equivalence of $G$ and $F$ is an equivalence from $G$ to the set of algebra homomorphisms of $F$ and $F$ defined as the equivalence of $\operatorname{toAlgHom}$ and $\mathrm{FixedPoints\_\_toAlgHom\_bijective}$ applied to $G$ and $F$.
IsInvariantSubfieldclassMathlib.FieldTheory.Fixed, predicateWording
S is a invariant subfield (from the name)
English
Let $M$ be a set. Let $S$ be a subfield of $F$. Then we can say that $S$ is an invariant subfield.
IsAbelianGaloisclassMathlib.FieldTheory.Galois.Abelian, predicateEnglish
Let $K$ and $L$ be sets. Then we can say that $\mathrm{IsAbelianGalois}$ holds for $K$ and $L$.
IsGaloisclassMathlib.FieldTheory.Galois.Basic, predicateEnglish
Let $F$ and $E$ be sets. Then we can say that $\mathrm{IsGalois}$ holds for $F$ and $E$.
IsGalois.normalAutEquivQuotientdefMathlib.FieldTheory.Galois.Basic, function or constantWording
the normal automorphism equivalence quotient of H (from the name)
English
Let $H$ be a subgroup of the set of algebra isomorphisms of $L$ and $L$. Then the normal automorphism equivalence quotient of $H$ is a multiplicative equivalence of the set of quotients of the set of algebra isomorphisms of $L$ and $L$ and $H$ and the set of algebra isomorphisms of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{fixedField} (H)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{fixedField} (H)}{x_{4}})}$.
InfiniteGalois.normalAutEquivQuotientdefMathlib.FieldTheory.Galois.Infinite, function or constantWording
the normal automorphism equivalence quotient of H (from the name)
English
Let $H$ be a closed subgroup of the set of algebra isomorphisms of $K$ and $K$. Then the normal automorphism equivalence quotient of $H$ is a multiplicative equivalence of the set of quotients of the set of algebra isomorphisms of $K$ and $K$ and $\operatorname{toSubgroup}$ applied to $H$ and the set of algebra isomorphisms of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{fixedField} (\operatorname{toSubgroup} (H))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{fixedField} (\operatorname{toSubgroup} (H))}{x_{4}})}$.
IsGaloisGroup.mulEquivCongrdefMathlib.FieldTheory.Galois.IsGaloisGroup, function or constantWording
the multiplicative equivalence congruence of B and #4 (from the name)
English
Let $G$, $\mathrm{G'}$, $A$ and $B$ be sets. Then the multiplicative equivalence congruence of $A$ and $B$ is a multiplicative equivalence of $G$ and $\mathrm{G'}$ defined as the composition of the multiplicative equivalence algebra isomorphism of $A$ and $B$ and the inverse of the multiplicative equivalence algebra isomorphism of $A$ and $B$.
IsGaloisGroup.quotientMulEquivdefMathlib.FieldTheory.Galois.IsGaloisGroup, function or constantWording
the quotient multiplicative equivalence of #6 (from the name)
English
Let $G$, $\mathrm{G'}$, $A$, $B$ and $C$ be sets. Let $N$ be a subgroup of $G$. Then the quotient multiplicative equivalence of $N$ is a multiplicative equivalence of the set of quotients of $G$ and $N$ and $\mathrm{G'}$ defined as the multiplicative equivalence congruence of $A$ and $B$.
IsGaloisGroup.restrictHomdefMathlib.FieldTheory.Galois.IsGaloisGroup, function or constantWording
the restriction homomorphism from the Galois group of G (from the docstring)
English
Let $G$, $\mathrm{G'}$, $A$, $B$ and $C$ be sets. Then the restriction homomorphism from the Galois group of $G$ is a monoid homomorphism of $G$ and $\mathrm{G'}$ defined as the composition of the monoid homomorphism of the quotient multiplicative equivalence of $\mathrm{fixingSubgroup}$ applied to $G$ and the range of $\operatorname{coe}$ applied to the algebra map of the set of fraction rings of $B$ and the set of fraction rings of $C$ and $\operatorname{mk'}$ applied to $\mathrm{fixingSubgroup}$ applied to $G$ and the range of $\operatorname{coe}$ applied to the algebra map of the set of fraction rings of $B$ and the set of fraction rings of $C$.
IsGalois.normalBasisdefMathlib.FieldTheory.Galois.NormalBasis, function or constantWording
the normal basis of K and L (from the name)
English
Let $K$ and $L$ be sets. Then the normal basis of $K$ and $L$ is a basis of $K$ and $L$.
InfiniteGalois.algEquivToLimitdefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the algebra isomorphism to limit of k and K (from the name)
English
Let $k$ and $K$ be sets. Then the algebra isomorphism to limit of $k$ and $K$ is a monoid homomorphism of the set of algebra isomorphisms of $K$ and $K$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$.
InfiniteGalois.asProfiniteGaloisGroupFunctordefMathlib.FieldTheory.Galois.Profinite, function or constantEnglish
Let $k$ and $K$ be sets. Then $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$ is a functor of the set of opposites of the set of finite Galois intermediate fields of $k$ and $K$ and the set of profinite groups defined as the composition of the finite Galois group functor of $k$ and $K$ and the forgetful functor of the set of finite groups and the set of profinite groups.
InfiniteGalois.continuousMulEquivToLimitdefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the continuous multiplicative equivalence to limit of k and K (from the name)
English
Let $k$ and $K$ be sets. Then the continuous multiplicative equivalence to limit of $k$ and $K$ is a continuous multiplicative equivalence of the set of algebra isomorphisms of $K$ and $K$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$ defined as $\operatorname{mk}$ applied to the multiplicative equivalence to limit of $k$ and $K$, $\mathrm{InfiniteGalois\_\_algEquivToLimit\_continuous}$ and $\mathrm{InfiniteGalois\_\_mulEquivToLimit\_symm\_continuous}$.
InfiniteGalois.limitToAlgEquivdefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the limit to algebra isomorphism of g (from the name)
English
Let $g$ be a carrier of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$. Then the limit to algebra isomorphism of $g$ is an algebra isomorphism of $K$ and $K$.
InfiniteGalois.mulEquivToLimitdefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the multiplicative equivalence to limit of k and K (from the name)
English
Let $k$ and $K$ be sets. Then the multiplicative equivalence to limit of $k$ and $K$ is a multiplicative equivalence of the set of algebra isomorphisms of $K$ and $K$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$.
InfiniteGalois.profiniteGalGrpdefMathlib.FieldTheory.Galois.Profinite, function or constantEnglish
Let $k$ and $K$ be sets. Then $\operatorname{profiniteGalGrp}$ applied to $k$ and $K$ is a profinite group defined as $\operatorname{of}$ applied to the set of algebra isomorphisms of $K$ and $K$.
InfiniteGalois.profiniteGalGrpIsoLimitdefMathlib.FieldTheory.Galois.Profinite, function or constantEnglish
Let $k$ and $K$ be sets. Then $\operatorname{profiniteGalGrpIsoLimit}$ applied to $k$ and $K$ is an isomorphism of $\operatorname{profiniteGalGrp}$ applied to $k$ and $K$ and the abbreviation for the limit of $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$ defined as the profinite group isomorphism of the continuous multiplicative equivalence to limit of $k$ and $K$.
InfiniteGalois.projdefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the projection of L (from the name)
English
Let $L$ be a finite Galois intermediate field of $k$ and $K$. Then the projection of $L$ is a monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of $\operatorname{asProfiniteGaloisGroupFunctor}$ applied to $k$ and $K$ and the set of algebra isomorphisms of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toIntermediateField} (L)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{toIntermediateField} (L)}{x_{4}})}$.
finGaloisGroupFunctordefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the finite Galois group functor of k and K (from the name)
English
Let $k$ and $K$ be sets. Then the finite Galois group functor of $k$ and $K$ is a functor of the set of opposites of the set of finite Galois intermediate fields of $k$ and $K$ and the set of finite groups defined as $\operatorname{mk}$ applied to the function that maps $L$ to the finite Galois group of the opposite of $L$, the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{finGaloisGroupMap}$, $\mathrm{finGaloisGroupMap\_\_map\_id}$ and the function that maps $x_{5}$, $x_{6}$ and $x_{7}$ to $\mathrm{finGaloisGroupMap\_\_map\_comp}$.
finGaloisGroupMapdefMathlib.FieldTheory.Galois.Profinite, function or constantWording
the finite Galois group map of le (from the name)
English
Let $\mathrm{le}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the finite Galois group map of $\mathrm{le}$ is a homomorphism of the finite Galois group of the opposite of $x_{3}$ and the finite Galois group of the opposite of $x_{4}$ defined as the finite group of $\operatorname{restrictNormalHom}$ applied to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{toIntermediateField} (\operatorname{unop} (x_{4}))}{x_{5}})}$.
PowerBasis.equivAdjoinSimpledefMathlib.FieldTheory.IntermediateField.Adjoin.Basic, function or constantEnglish
Let $\mathrm{pb}$ be a power basis of $K$ and $L$. Then $\operatorname{equivAdjoinSimple}$ applied to $\mathrm{pb}$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{adjoin} (K , \operatorname{singleton} (\operatorname{gen} (\mathrm{pb})))}{x_{3}})}$ and $L$.
PowerBasis.ofAdjoinSimpleEqTopdefMathlib.FieldTheory.IntermediateField.Adjoin.Basic, function or constantWording
the power basis of h and hgen (from the name)
English
Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $K$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then the power basis of $h$ and $\mathrm{hgen}$ is a power basis of $K$ and $L$ defined as the map of the power basis of $h$ and the composition of the equivalence of $\mathrm{hgen}$ and the top.
minpoly.algEquivdefMathlib.FieldTheory.IntermediateField.Adjoin.Basic, function or constantWording
the algebra isomorphism of hx and h_mp (from the name)
English
Assume that $x_{3}$ is algebraic. Assume that the minimal polynomial of $K$ and $x_{3}$ is equal to the minimal polynomial of $K$ and $y$. Then the algebra isomorphism of $\mathrm{hx}$ and $\mathrm{h\_mp}$ is an algebra isomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (K , \operatorname{singleton} (x_{3}))}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (K , \operatorname{singleton} (y))}{x_{5}})}$.
AlgHom.equivFieldRangedefMathlib.FieldTheory.IntermediateField.Basic, function or constantWording
the equivalence field range of f (from the name)
English
Let $f$ be an algebra homomorphism of $L$ and $\mathrm{L'}$. Then the equivalence field range of $f$ is an algebra isomorphism of $L$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{fieldRange} (f)}{x_{5}})}$.
AlgHom.fieldRangedefMathlib.FieldTheory.IntermediateField.Basic, function or constantWording
the range of f (from the docstring)
English
Let $f$ be an algebra homomorphism of $L$ and $\mathrm{L'}$. Then the range of $f$ is an intermediate field of $K$ and $\mathrm{L'}$.
Subfield.extendScalarsdefMathlib.FieldTheory.IntermediateField.Basic, function or constantEnglish
Assume that $F \leq E$. Then $\operatorname{extendScalars}$ applied to $h$ is an intermediate field of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {F}{x_{1}})}$ and $L$.
Subfield.extendScalars.orderIsodefMathlib.FieldTheory.IntermediateField.Basic, function or constantWording
the order isomorphism of F (from the name)
English
Let $F$ be a subfield of $L$. Then the order isomorphism of $F$ is an order isomorphism of $\SubtypeSet {E}{\mathrm{Leq} (F , E)}$ and the set of intermediate fields of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {F}{x_{1}})}$ and $L$.
AlgebraicClosuredefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, typeWording
algebraic closure of k (from the name)
English
Let $k$ be a set. Then an algebraic closure of $k$ is an element of the function that maps $k$ to the set of quotients of the set of multivariate polynomials of $\operatorname{Vars}$ applied to $k$ and $k$ and the maximum ideal of $k$.
AlgebraicClosure.MonicsdefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, typeEnglish
Let $k$ be a set. Then an element of $\operatorname{Monics}$ applied to $k$ is an element of the function that maps $k$ to $\SubtypeSet {f}{\operatorname{Monic} (f)}$.
AlgebraicClosure.VarsdefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, typeEnglish
Let $k$ be a set. Then an element of $\operatorname{Vars}$ applied to $k$ is an element of the function that maps $k$ to $\Sigma$ applied to the function that maps $f$ to $\mathrm{Fin}$ applied to the natural degree of $f$.
AlgebraicClosure.finEquivRootsdefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, function or constantWording
the finite equivalence root of hf (from the name)
English
Assume that $\operatorname{Splits}$ holds for the map of $i$ and $f$. Then the finite equivalence root of $\mathrm{hf}$ is an element of $\EquivMACRoAE {\mathrm{Fin} (\operatorname{natDegree} (f))}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toEnumFinset} (\operatorname{roots} (\operatorname{map} (i , f)))}{x_{3}})})}$.
AlgebraicClosure.maxIdealdefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, function or constantWording
the maximum ideal of k (from the name)
English
Let $k$ be a set. Then the maximum ideal of $k$ is an ideal of the set of multivariate polynomials of $\operatorname{Vars}$ applied to $k$ and $k$.
AlgebraicClosure.spanCoeffsdefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, function or constantWording
the span of all coefficients of k (from the docstring)
English
Let $k$ be a set. Then the span of all coefficients of $k$ is an ideal of the set of multivariate polynomials of $\operatorname{Vars}$ applied to $k$ and $k$ defined as the span of the range of the function that maps $\mathrm{fn}$ to $\operatorname{coeff}$ applied to the difference product difference of $\ProdfstMACRoZ {\mathrm{fn}}$ and $\ProdsndMACRoAA {\mathrm{fn}}$.
AlgebraicClosure.subProdXSubCdefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, function or constantWording
the difference product difference of f (from the name)
English
Let $f$ be an element of $\operatorname{Monics}$ applied to $k$. Then the difference product difference of $f$ is a polynomial of the set of multivariate polynomials of $\operatorname{Vars}$ applied to $k$ and $k$ defined as the difference between the map of the algebra map of $k$ and the set of multivariate polynomials of $\operatorname{Vars}$ applied to $k$ and $k$ and $f$ and $\FinsetProd {\FinsetunivMACRoAC}{i}{(\operatorname{X} - \operatorname{C} (\operatorname{X} (\operatorname{mk} (f , i))))}$.
AlgebraicClosure.toSplittingFielddefMathlib.FieldTheory.IsAlgClosed.AlgebraicClosure, function or constantWording
the splitting field of s (from the name)
English
Let $s$ be a finite set of $\operatorname{Monics}$ applied to $k$. Then the splitting field of $s$ is an algebra homomorphism of the set of multivariate polynomials of $\operatorname{Vars}$ applied to $k$ and $k$ and the set of splitting fields of $\FinsetProd {s}{f}{f}$.
Algebra.IsAlgebraic.algHomEquivAlgHomOfSplitsdefMathlib.FieldTheory.IsAlgClosed.Basic, function or constantWording
the algebra homomorphism equivalence algebra homomorphism of L and hL (from the name)
English
Let $A$ and $L$ be sets such that for all elements $x_{8}$ of $K$, $\operatorname{Splits}$ holds for the map of the algebra map of $F$ and $L$ and the minimal polynomial of $F$ and $x_{8}$. Then the algebra homomorphism equivalence algebra homomorphism of $L$ and $\mathrm{hL}$ is an equivalence from the set of algebra homomorphisms of $K$ and $L$ to the set of algebra homomorphisms of $K$ and $A$.
IsAlgClosedclassMathlib.FieldTheory.IsAlgClosed.Basic, predicateEnglish
Let $k$ be a set. Then we can say that $\mathrm{IsAlgClosed}$ holds for $k$.
IsAlgClosed.liftdefMathlib.FieldTheory.IsAlgClosed.Basic, function or constantWording
the lift (from the name)
English
The lift is an algebra homomorphism of $S$ and $M$.
IsAlgClosureclassMathlib.FieldTheory.IsAlgClosed.Basic, predicateEnglish
Let $R$ and $K$ be sets. Then we can say that $\mathrm{IsAlgClosure}$ holds for $R$ and $K$.
IsAlgClosure.equivdefMathlib.FieldTheory.IsAlgClosed.Basic, function or constantWording
the equivalence of L and M (from the name)
English
Let $R$, $L$ and $M$ be sets. Then the equivalence of $L$ and $M$ is an algebra isomorphism of $L$ and $M$.
IsAlgClosure.equivOfAlgebraicdefMathlib.FieldTheory.IsAlgClosed.Basic, function or constantWording
the equivalence of L and M (from the name)
English
Let $K$, $J$, $L$ and $M$ be sets. Then the equivalence of $L$ and $M$ is an algebra isomorphism of $L$ and $M$ defined as the equivalence of $L$ and $M$.
IsAlgClosure.equivOfAlgebraic'defMathlib.FieldTheory.IsAlgClosed.Basic, function or constantWording
the equivalence of L and M (from the name)
English
Let $R$, $S$, $L$ and $M$ be sets. Then the equivalence of $L$ and $M$ is an algebra isomorphism of $L$ and $M$ defined as the equivalence of $L$ and $M$.
IsAlgClosure.equivOfEquivdefMathlib.FieldTheory.IsAlgClosed.Basic, function or constantWording
the equivalence of hSR (from the name)
English
Let $L$ and $M$ be sets. Let $\mathrm{hSR}$ be a ring isomorphism of $S$ and $R$. Then the equivalence of $\mathrm{hSR}$ is a ring isomorphism of $L$ and $M$ defined as $\operatorname{equivOfEquivAux}$ applied to $L$, $M$ and $\mathrm{hSR}$.
IsAlgClosed.equivOfTranscendenceBasisdefMathlib.FieldTheory.IsAlgClosed.Classification, function or constantWording
the equivalence of w and e (from the name)
English
Let $v$ be a function from elements of $x_{5}$ to elements of $K$. Let $w$ be a function from elements of $x_{6}$ to elements of $L$. Let $e$ be an equivalence from $x_{5}$ to $x_{6}$. Assume that $R$ is a transcendence basis. Assume that $R$ is a transcendence basis. Then the equivalence of $w$ and $e$ is a ring isomorphism of $K$ and $L$.
IsPRadicalclassMathlib.FieldTheory.IsPerfectClosure, predicateEnglish
Let $i$ be a ring homomorphism of $K$ and $L$. Let $p$ be a natural number. Then we can say that $\mathrm{IsPRadical}$ holds for $i$ and $p$.
IsPerfectClosuredefMathlib.FieldTheory.IsPerfectClosure, predicateEnglish
Let $i$ be a ring homomorphism of $K$ and $L$. Let $p$ be a natural number. Then $\mathrm{IsPerfectClosure}$ holds for $i$ and $p$, if $\mathrm{IsPRadical}$ holds for $i$ and $p$.
IsPerfectClosure.equivdefMathlib.FieldTheory.IsPerfectClosure, function or constantWording
the equivalence of j and p (from the name)
English
Let $i$ be a ring homomorphism of $K$ and $L$. Let $j$ be a ring homomorphism of $K$ and $M$. Let $p$ be a natural number. Then the equivalence of $j$ and $p$ is a ring isomorphism of $L$ and $M$.
PerfectRing.liftdefMathlib.FieldTheory.IsPerfectClosure, function or constantWording
the lift of j and p (from the name)
English
Let $i$ be a ring homomorphism of $K$ and $L$. Let $j$ be a ring homomorphism of $K$ and $M$. Let $p$ be a natural number. Then the lift of $j$ and $p$ is a ring homomorphism of $L$ and $M$.
PerfectRing.liftEquivdefMathlib.FieldTheory.IsPerfectClosure, function or constantWording
the lift equivalence of i and p (from the name)
English
Let $M$ be a set. Let $i$ be a ring homomorphism of $K$ and $L$. Let $p$ be a natural number. Then the lift equivalence of $i$ and $p$ is an equivalence from the set of ring homomorphisms of $K$ and $M$ to the set of ring homomorphisms of $L$ and $M$ defined as $\operatorname{mk}$ applied to the function that maps $j$ to the lift of $j$ and $p$, the function that maps $f$ to the composition of $f$ and $i$, the function that maps $f_{1}$ to $\mathrm{PerfectRing\_\_lift\_comp}$ applied to $i$, $f_{1}$ and $p$ and the function that maps $f_{2}$ to $\mathrm{PerfectRing\_\_comp\_lift}$ applied to $i$, $f_{2}$ and $p$.
pNilradicaldefMathlib.FieldTheory.IsPerfectClosure, function or constantWording
the nilradical of R and p (from the name)
English
Let $R$ be a set. Let $p$ be an element of $\Natural$. Then the nilradical of $R$ and $p$ is an ideal of $R$ defined as $\iteMACRoG {\mathrm{Lt} (1 , p)}{\mathrm{nilradical} (R)}{\operatorname{bot}}$.
IsRealClosedclassMathlib.FieldTheory.IsRealClosed.Basic, predicateEnglish
Let $R$ be a set. Then we can say that $\mathrm{IsRealClosed}$ holds for $R$.
IsSepClosedclassMathlib.FieldTheory.IsSepClosed, predicateEnglish
Let $k$ be a set. Then we can say that $\mathrm{IsSepClosed}$ holds for $k$.
IsSepClosed.liftdefMathlib.FieldTheory.IsSepClosed, function or constantWording
the lift (from the name)
English
The lift is an algebra homomorphism of $L$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{IsSepClosed\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_IsSepClosed\_\_1301403324\_\_\_hygCtx\_\_\_hyg\_\_2}$.
IsSepClosureclassMathlib.FieldTheory.IsSepClosed, predicateEnglish
Let $k$ and $K$ be sets. Then we can say that $\mathrm{IsSepClosure}$ holds for $k$ and $K$.
IsSepClosure.equivdefMathlib.FieldTheory.IsSepClosed, function or constantWording
the equivalence of L and M (from the name)
English
Let $K$, $L$ and $M$ be sets. Then the equivalence of $L$ and $M$ is an algebra isomorphism of $L$ and $M$.
SeparableClosuredefMathlib.FieldTheory.IsSepClosed, typeWording
separable closure of F (from the name)
English
Let $F$ be a set. Then a separable closure of $F$ is an element of the function that maps $F$ to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , \mathrm{AlgebraicClosure} (F))}{x_{1}})}$.
finiteExtsdefMathlib.FieldTheory.KrullTopology, function or constantEnglish
Let $K$ and $L$ be sets. Then $\mathrm{finiteExts}$ applied to $K$ and $L$ is an element of the power set of the set of intermediate fields of $K$ and $L$ defined as $\operatorname{ofPred}$ applied to the function that maps $E$ to $\mathrm{FiniteDimensional}$ applied to $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {E}{x_{3}})}$.
fixedByFinitedefMathlib.FieldTheory.KrullTopology, function or constantEnglish
Let $K$ and $L$ be sets. Then $\mathrm{fixedByFinite}$ applied to $K$ and $L$ is an element of the power set of the set of subgroups of the set of algebra isomorphisms of $L$ and $L$ defined as the image of $\operatorname{fixingSubgroup}$ and $\mathrm{finiteExts}$ applied to $K$ and $L$.
galBasisdefMathlib.FieldTheory.KrullTopology, function or constantEnglish
Let $K$ and $L$ be sets. Then $\mathrm{galBasis}$ applied to $K$ and $L$ is a filter basis of the set of algebra isomorphisms of $L$ and $L$.
AdjoinRootXPowSubCEquivToRootsOfUnitydefMathlib.FieldTheory.KummerExtension, function or constantEnglish
Assume that the primitive root of $n$ and $K$ is nonempty. Assume that $\operatorname{X} ^ {n}- \operatorname{C} (a)$ is irreducible. Let $x_{1}$ be an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ and $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$. Then $\mathrm{AdjoinRootXPowSubCEquivToRootsOfUnity}$ applied to $h$, $H$ and $x_{1}$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , K)}{x_{2}})}$.
adjoinRootXPowSubCEquivdefMathlib.FieldTheory.KummerExtension, function or constantEnglish
Assume that the primitive root of $n$ and $K$ is nonempty. Assume that $\operatorname{X} ^ {n}- \operatorname{C} (a)$ is irreducible. Assume that $\EqtMACRoH {x_{3} ^ {n}}{\operatorname{algebraMap} (K , L , a)}$. Then $\mathrm{adjoinRootXPowSubCEquiv}$ applied to $h_{1}$, $H$ and $h_{2}$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ and $L$.
autAdjoinRootXPowSubCdefMathlib.FieldTheory.KummerExtension, function or constantEnglish
Let $n$ be an element of $\Natural$. Let $a$ be an element of $K$. Then $\mathrm{autAdjoinRootXPowSubC}$ applied to $n$ and $a$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , K)}{x_{1}})}$ and the set of algebra isomorphisms of $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ and $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ defined as the composition of the monoid homomorphism of the algebra homomorphism unit equivalence of $K$ and $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ and the homomorphism unit of $\mathrm{autAdjoinRootXPowSubCHom}$ applied to $n$ and $a$.
autAdjoinRootXPowSubCEquivdefMathlib.FieldTheory.KummerExtension, function or constantEnglish
Assume that the primitive root of $n$ and $K$ is nonempty. Assume that $\operatorname{X} ^ {n}- \operatorname{C} (a)$ is irreducible. Then $\mathrm{autAdjoinRootXPowSubCEquiv}$ applied to $h$ and $H$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , K)}{x_{1}})}$ and the set of algebra isomorphisms of $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ and $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$.
autAdjoinRootXPowSubCHomdefMathlib.FieldTheory.KummerExtension, function or constantEnglish
Let $n$ be an element of $\Natural$. Let $a$ be an element of $K$. Then $\mathrm{autAdjoinRootXPowSubCHom}$ applied to $n$ and $a$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , K)}{x_{1}})}$ and the set of algebra homomorphisms of $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$ and $\mathrm{AdjoinRoot}$ applied to $\operatorname{X} ^ {n}- \operatorname{C} (a)$.
autEquivRootsOfUnitydefMathlib.FieldTheory.KummerExtension, function or constantWording
the automorphism equivalence root of H and L (from the name)
English
Assume that the primitive root of $n$ and $K$ is nonempty. Assume that $\operatorname{X} ^ {n}- \operatorname{C} (a)$ is irreducible. Let $L$ be a set. Then the automorphism equivalence root of $H$ and $L$ is a multiplicative equivalence of the set of algebra isomorphisms of $L$ and $L$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , K)}{x_{3}})}$ defined as the composition of the automorphism congruence of the inverse of $\mathrm{adjoinRootXPowSubCEquiv}$ applied to $h$, $H$ and $\mathrm{rootOfSplitsXPowSubC\_pow}$ applied to $a$ and $L$ and the inverse of $\mathrm{autAdjoinRootXPowSubCEquiv}$ applied to $h$ and $H$.
autEquivZmoddefMathlib.FieldTheory.KummerExtension, function or constantWording
the automorphism equivalence integer modulo of L and h2 (from the name)
English
Assume that $\operatorname{X} ^ {n}- \operatorname{C} (a)$ is irreducible. Let $L$ be a set. Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{3}$ and $n$. Then the automorphism equivalence integer modulo of $L$ and $h_{2}$ is a multiplicative equivalence of the set of algebra isomorphisms of $L$ and $L$ and the set of multiplicatives of $\mathrm{ZMod}$ applied to $n$.
rootOfSplitsXPowSubCdefMathlib.FieldTheory.KummerExtension, function or constantWording
the root of a (from the name)
English
Assume that $0 < n$. Let $a$ be an element of $K$. Let $L$ be a set. Then the root of $a$ is an element of $L$.
RatFunc.laurentdefMathlib.FieldTheory.Laurent, function or constantEnglish
Let $r$ be an element of $R$. Then $\operatorname{laurent}$ applied to $r$ is an algebra homomorphism of the set of rational number functions of $R$ and the set of rational number functions of $R$.
minpolydefMathlib.FieldTheory.Minpoly.Basic, function or constantWording
the minimal polynomial of A and x3 (from the name)
English
Let $A$ be a set. Let $x_{3}$ be an element of $B$. Then the minimal polynomial of $A$ and $x_{3}$ is a polynomial of $A$.
ConjRootClassdefMathlib.FieldTheory.Minpoly.ConjRootClass, typeWording
conjugate root class of K and L (from the name)
English
Let $K$ and $L$ be sets. Then a conjugate root class of $K$ and $L$ is an element of the function that maps $K$ and $L$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $K$ and $L$.
ConjRootClass.carrierdefMathlib.FieldTheory.Minpoly.ConjRootClass, function or constantWording
the carrier of c (from the name)
English
Let $c$ be a conjugate root class of $K$ and $L$. Then the carrier of $c$ is an element of $\wp L$ defined as the preimage of $\operatorname{mk}$ applied to $K$ and $\operatorname{singleton}$ applied to $c$.
ConjRootClass.minpolydefMathlib.FieldTheory.Minpoly.ConjRootClass, function or constantWording
the minimal polynomial of the conjugates of x3 (from the docstring)
English
Let $x_{3}$ be a conjugate root class of $K$ and $L$. Then the minimal polynomial of the conjugates of $x_{3}$ is a polynomial of $K$.
ConjRootClass.mkdefMathlib.FieldTheory.Minpoly.ConjRootClass, function or constantEnglish
Let $K$ be a set. Let $x_{3}$ be an element of $L$. Then $\operatorname{mk}$ applied to $K$ and $x_{3}$ is a conjugate root class of $K$ and $L$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $K$ and $L$ and $x_{3}$.
minpoly.rootsOfMinPolyPiTypedefMathlib.FieldTheory.Minpoly.Field, function or constantWording
the root of x5 and x6 (from the name)
English
Let $F$, $E$ and $K$ be sets. Let $x_{5}$ be an algebra homomorphism of $E$ and $K$. Let $x_{6}$ be an element of the range of $\operatorname{coe}$ applied to the finite basis of $F$ and $E$. Then the root of $x_{5}$ and $x_{6}$ is an element of $\SubtypeSet {l}{(\MembershipmemMACRoT {\operatorname{aroots} (\mathrm{minpoly} (F , x_{6}), K)}{l})}$ defined as $x_{5}$ applied to $x_{6}$.
IsConjRootdefMathlib.FieldTheory.Minpoly.IsConjRoot, predicateEnglish
Let $R$ be a set. Let $x_{3}$ and $y$ be elements of $A$. Then $\mathrm{IsConjRoot}$ holds for $R$, $x_{3}$ and $y$, if the minimal polynomial of $R$ and $x_{3}$ is equal to the minimal polynomial of $R$ and $y$.
Algebra.adjoin.powerBasis'defMathlib.FieldTheory.Minpoly.IsIntegrallyClosed, function or constantWording
the power basis of hx (from the name)
English
Assume that $x_{3}$ is integral. Then the power basis of $\mathrm{hx}$ is a power basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$.
PowerBasis.ofAdjoinEqTop'defMathlib.FieldTheory.Minpoly.IsIntegrallyClosed, function or constantWording
the power basis of hx and #2 (from the name)
English
Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then the power basis of $\mathrm{hx}$ and $\mathrm{hx'}$ is a power basis of $R$ and $S$ defined as the map of the power basis of $\mathrm{hx}$ and the composition of the equivalence of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{3}$ and the top and the top subalgebra.
minpoly.equivAdjoindefMathlib.FieldTheory.Minpoly.IsIntegrallyClosed, function or constantEnglish
Assume that $x_{3}$ is integral. Then $\operatorname{equivAdjoin}$ applied to $\mathrm{hx}$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to the minimal polynomial of $R$ and $x_{3}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$.
minpolyDivdefMathlib.FieldTheory.Minpoly.MinpolyDiv, function or constantWording
the minimal polynomial quotient of R and x3 (from the name)
English
Let $R$ be a set. Let $x_{3}$ be an element of $S$. Then the minimal polynomial quotient of $R$ and $x_{3}$ is a polynomial of $S$ defined as $\operatorname{divByMonic}$ applied to the map of the algebra map of $R$ and $S$ and the minimal polynomial of $R$ and $x_{3}$ and $\operatorname{X} - \operatorname{C} (x_{3})$.
AlgEquiv.liftNormaldefMathlib.FieldTheory.Normal.Basic, function or constantWording
the lift normal of x7 and E (from the name)
English
Let $x_{7}$ be an algebra isomorphism of $x_{1}$ and $x_{2}$. Let $E$ be a set. Then the lift normal of $x_{7}$ and $E$ is an algebra isomorphism of $E$ and $E$.
AlgHom.liftNormaldefMathlib.FieldTheory.Normal.Basic, function or constantWording
the lift normal of x7 and E (from the name)
English
Let $x_{7}$ be an algebra homomorphism of $x_{1}$ and $x_{2}$. Let $E$ be a set. Then the lift normal of $x_{7}$ and $E$ is an algebra homomorphism of $E$ and $E$.
Algebra.IsAlgebraic.algHomEmbeddingOfSplitsdefMathlib.FieldTheory.Normal.Closure, function or constantWording
the algebra homomorphism embedding of h1 and #2 (from the name)
English
Assume that for all elements $x_{7}$ of $K$, $\operatorname{Splits}$ holds for the map of the algebra map of $F$ and $L$ and the minimal polynomial of $F$ and $x_{7}$. Let $\mathrm{L'}$ be a set. Then the algebra homomorphism embedding of $h_{1}$ and $\mathrm{L'}$ is an embedding of the set of algebra homomorphisms of $K$ and $\mathrm{L'}$ and the set of algebra homomorphisms of $K$ and $L$.
IsNormalClosureclassMathlib.FieldTheory.Normal.Closure, predicateWording
K is a normal closure with respect to L (from the name)
English
Let $F$, $K$ and $L$ be sets. Then we can say that $K$ is a normal closure with respect to $L$.
IsNormalClosure.equivdefMathlib.FieldTheory.Normal.Closure, function or constantWording
the equivalence (from the name)
English
The equivalence is an algebra isomorphism of $L$ and $\mathrm{L'}$.
IsNormalClosure.liftdefMathlib.FieldTheory.Normal.Closure, function or constantWording
the lift of splits (from the name)
English
Assume that for all elements $x_{7}$ of $K$, $\operatorname{Splits}$ holds for the map of the algebra map of $F$ and $\mathrm{L'}$ and the minimal polynomial of $F$ and $x_{7}$. Then the lift of $\mathrm{splits}$ is an algebra homomorphism of $L$ and $\mathrm{L'}$.
normalClosure.algHomEquivdefMathlib.FieldTheory.Normal.Closure, function or constantWording
the algebra homomorphism equivalence of K and L (from the name)
English
Let $F$, $K$ and $L$ be sets. Then the algebra homomorphism equivalence of $K$ and $L$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (K , \SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{normalClosure} (F)}{x_{5}})})}{\mathrm{AlgHom} (K , L)}$.
AlgEquiv.restrictNormaldefMathlib.FieldTheory.Normal.Defs, function or constantEnglish
Let $x_{7}$ be an algebra isomorphism of $x_{1}$ and $x_{2}$. Let $E$ be a set. Then $\operatorname{restrictNormal}$ applied to $x_{7}$ and $E$ is an algebra isomorphism of $E$ and $E$ defined as $\operatorname{restrictNormal'}$ applied to the algebra homomorphism of $x_{7}$ and $E$.
AlgEquiv.restrictNormalHomdefMathlib.FieldTheory.Normal.Defs, function or constantEnglish
Let $E$ be a set. Then $\operatorname{restrictNormalHom}$ applied to $E$ is a monoid homomorphism of the set of algebra isomorphisms of $x_{1}$ and $x_{1}$ and the set of algebra isomorphisms of $E$ and $E$ defined as $\operatorname{mk'}$ applied to the function that maps $x_{7}$ to $\operatorname{restrictNormal}$ applied to $x_{7}$ and $E$ and the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{AlgEquiv\_\_restrictNormal\_trans}$ applied to $x_{9}$, $x_{8}$ and $E$.
AlgHom.restrictNormaldefMathlib.FieldTheory.Normal.Defs, function or constantEnglish
Let $x_{7}$ be an algebra homomorphism of $x_{1}$ and $x_{2}$. Let $E$ be a set. Then $\operatorname{restrictNormal}$ applied to $x_{7}$ and $E$ is an algebra homomorphism of $E$ and $E$ defined as the composition of the composition of the algebra homomorphism of the inverse of the algebra isomorphism of the algebra homomorphism of $E$ and $x_{2}$ and $\operatorname{restrictNormalAux}$ applied to $x_{7}$ and $E$ and the algebra homomorphism of the algebra isomorphism of the algebra homomorphism of $E$ and $x_{1}$.
AlgHom.restrictNormal'defMathlib.FieldTheory.Normal.Defs, function or constantEnglish
Let $x_{7}$ be an algebra homomorphism of $x_{1}$ and $x_{2}$. Let $E$ be a set. Then $\operatorname{restrictNormal'}$ applied to $x_{7}$ and $E$ is an algebra isomorphism of $E$ and $E$.
NormalclassMathlib.FieldTheory.Normal.Defs, predicateEnglish
Let $F$ and $K$ be sets. Then we can say that $\mathrm{Normal}$ holds for $F$ and $K$.
Normal.algHomEquivAutdefMathlib.FieldTheory.Normal.Defs, function or constantWording
the algebra homomorphism equivalence automorphism of x1 and E (from the name)
English
Let $F$, $x_{1}$ and $E$ be sets. Then the algebra homomorphism equivalence automorphism of $x_{1}$ and $E$ is an equivalence from the set of algebra homomorphisms of $E$ and $x_{1}$ to the set of algebra isomorphisms of $E$ and $E$.
Algebra.normalizedTracedefMathlib.FieldTheory.NormalizedTrace, function or constantWording
the normalized trace of F and K (from the name)
English
Let $F$ and $K$ be sets. Then the normalized trace of $F$ and $K$ is a linear map of $K$ and $F$.
PerfectFieldclassMathlib.FieldTheory.Perfect, predicateWording
K is a perfect field (from the name)
English
Let $K$ be a set. Then we can say that $K$ is a perfect field.
PerfectRingclassMathlib.FieldTheory.Perfect, predicateWording
p is a perfect ring (from the name)
English
Let $R$ be a set. Let $p$ be a natural number. Then we can say that $p$ is a perfect ring.
Polynomial.rootsExpandEquivRootsdefMathlib.FieldTheory.Perfect, function or constantWording
the root expand equivalence root of p and f (from the name)
English
Let $p$ be an element of $\Natural$. Let $f$ be a polynomial of $R$. Then the root expand equivalence root of $p$ and $f$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (\operatorname{expand} (R , p , f)))}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (f))}{x_{3}})})}$.
Polynomial.rootsExpandPowEquivRootsdefMathlib.FieldTheory.Perfect, function or constantWording
the root expand power equivalence root of f and n (from the name)
English
Let $p$ and $n$ be elements of $\Natural$. Let $f$ be a polynomial of $R$. Then the root expand power equivalence root of $f$ and $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (\operatorname{expand} (R , p ^ {n}, f)))}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (f))}{x_{3}})})}$.
Polynomial.rootsExpandPowToRootsdefMathlib.FieldTheory.Perfect, function or constantWording
the root expand power to root of n and f (from the name)
English
Let $p$ and $n$ be elements of $\Natural$. Let $f$ be a polynomial of $R$. Then the root expand power to root of $n$ and $f$ is an embedding of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (\operatorname{expand} (R , p ^ {n}, f)))}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (f))}{x_{3}})}$.
Polynomial.rootsExpandToRootsdefMathlib.FieldTheory.Perfect, function or constantWording
the root expand to root of p and f (from the name)
English
Let $p$ be an element of $\Natural$. Let $f$ be a polynomial of $R$. Then the root expand to root of $p$ and $f$ is an embedding of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (\operatorname{expand} (R , p , f)))}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{roots} (f))}{x_{3}})}$.
frobeniusEquivdefMathlib.FieldTheory.Perfect, function or constantWording
the Frobenius automorphism of R and p (from the docstring)
English
Let $R$ be a set. Let $p$ be a natural number. Then the Frobenius automorphism of $R$ and $p$ is a ring isomorphism of $R$ and $R$.
iterateFrobeniusEquivdefMathlib.FieldTheory.Perfect, function or constantEnglish
Let $R$ be a set. Let $p$ and $n$ be natural numbers. Then $\mathrm{iterateFrobeniusEquiv}$ applied to $R$, $p$ and $n$ is a ring isomorphism of $R$ and $R$ defined as the ring isomorphism of $\mathrm{iterateFrobenius}$ applied to $R$, $p$ and $n$ and $\mathrm{bijective\_iterateFrobenius}$ applied to $R$, $p$ and $n$.
powMulEquivdefMathlib.FieldTheory.Perfect, function or constantWording
the power multiplicative equivalence of M and p (from the name)
English
Let $M$ be a set. Let $p$ be a natural number. Then the power multiplicative equivalence of $M$ and $p$ is a multiplicative equivalence of $M$ and $M$.
PerfectClosuredefMathlib.FieldTheory.PerfectClosure, typeWording
perfect closure of K and p (from the name)
English
Let $K$ be a set. Let $p$ be a natural number. Then a perfect closure of $K$ and $p$ is an element of the function that maps $K$ and $p$ to $\mathrm{Quot}$ applied to $\operatorname{R}$ applied to $K$ and $p$.
PerfectClosure.RinductiveMathlib.FieldTheory.PerfectClosure, predicateEnglish
Let $K$ be a set. Let $p$ be a natural number. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Prod}$ applied to $\Natural$ and $K$. Then we can say that $\operatorname{R}$ holds for $K$, $p$, $x_{1}$ and $x_{2}$.
PerfectClosure.liftdefMathlib.FieldTheory.PerfectClosure, function or constantWording
the lift of p (from the name)
English
Let $K$ and $L$ be sets. Let $p$ be a natural number. Then the lift of $p$ is an equivalence from the set of ring homomorphisms of $K$ and $L$ to the set of ring homomorphisms of the set of perfect closures of $K$ and $p$ and $L$.
PerfectClosure.liftOndefMathlib.FieldTheory.PerfectClosure, function or constantEnglish
Let $x_{1}$ be a perfect closure of $K$ and $p$. Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $\Natural$ and $K$ to elements of $L$ such that for all elements $x_{2}$ and $y$ of $\mathrm{Prod}$ applied to $\Natural$ and $K$, if $\operatorname{R}$ holds for $K$, $p$, $x_{2}$ and $y$, then $\EqtMACRoH {f (x_{2})}{f (y)}$. Then $\operatorname{liftOn}$ applied to $x_{1}$, $f$ and $\mathrm{hf}$ is an element of $L$ defined as $\operatorname{liftOn}$ applied to $x_{1}$, $f$ and $\mathrm{hf}$.
PerfectClosure.mkdefMathlib.FieldTheory.PerfectClosure, function or constantEnglish
Let $K$ be a set. Let $p$ be a natural number. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $\Natural$ and $K$. Then $\operatorname{mk}$ applied to $K$, $p$ and $x_{1}$ is a perfect closure of $K$ and $p$ defined as $\operatorname{mk}$ applied to $\operatorname{R}$ applied to $K$ and $p$ and $x_{1}$.
PerfectClosure.ofdefMathlib.FieldTheory.PerfectClosure, function or constantEnglish
Let $K$ be a set. Let $p$ be a natural number. Then $\operatorname{of}$ applied to $K$ and $p$ is a ring homomorphism of $K$ and the set of perfect closures of $K$ and $p$.
Polynomial.GaldefMathlib.FieldTheory.PolynomialGaloisGroup, typeEnglish
Let $p$ be a polynomial of $F$. Then an element of $\operatorname{Gal}$ applied to $p$ is an element of the function that maps $p$ to the set of algebra isomorphisms of the set of splitting fields of $p$ and the set of splitting fields of $p$.
Polynomial.Gal.galActionHomdefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantEnglish
Let $p$ be a polynomial of $F$. Let $E$ be a set. Then $\operatorname{galActionHom}$ applied to $p$ and $E$ is a monoid homomorphism of $\operatorname{Gal}$ applied to $p$ and the set of permutations of the set of elements of the root set of $p$ and $E$ defined as the permutation homomorphism of $\operatorname{Gal}$ applied to $p$ and the set of elements of the root set of $p$ and $E$.
Polynomial.Gal.mapRootsdefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantWording
the map root of p and x3 (from the name)
English
Let $p$ be a polynomial of $F$. Let $E$ be a set. Let $x_{3}$ be an element of the root set of $p$ and the set of splitting fields of $p$. Then the map root of $p$ and $x_{3}$ is an element of the root set of $p$ and $E$.
Polynomial.Gal.restrictdefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantEnglish
Let $p$ be a polynomial of $F$. Let $E$ be a set. Then $\operatorname{restrict}$ applied to $p$ and $E$ is a monoid homomorphism of the set of algebra isomorphisms of $E$ and $E$ and $\operatorname{Gal}$ applied to $p$ defined as $\operatorname{restrictNormalHom}$ applied to the set of splitting fields of $p$.
Polynomial.Gal.restrictCompdefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantEnglish
Let $p$ and $q$ be polynomials of $F$ such that the natural degree of $q$ is distinct from $0$. Then $\operatorname{restrictComp}$ applied to $p$, $q$ and $\mathrm{hq}$ is a monoid homomorphism of $\operatorname{Gal}$ applied to the composition of $p$ and $q$ and $\operatorname{Gal}$ applied to $p$ defined as $\operatorname{restrict}$ applied to $p$ and the set of splitting fields of the composition of $p$ and $q$.
Polynomial.Gal.restrictDvddefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantEnglish
Assume that $p$ divides $q$. Then $\operatorname{restrictDvd}$ applied to $\mathrm{hpq}$ is a monoid homomorphism of $\operatorname{Gal}$ applied to $q$ and $\operatorname{Gal}$ applied to $p$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {q}{0}$, the function that maps $\mathrm{hq}$ to $1$ and the function that maps $\mathrm{hq1}$ to $\operatorname{restrict}$ applied to $p$ and the set of splitting fields of $q$.
Polynomial.Gal.restrictProddefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantEnglish
Let $p$ and $q$ be polynomials of $F$. Then $\operatorname{restrictProd}$ applied to $p$ and $q$ is a monoid homomorphism of $\operatorname{Gal}$ applied to $p \times q$ and $\mathrm{Prod}$ applied to $\operatorname{Gal}$ applied to $p$ and $\operatorname{Gal}$ applied to $q$.
Polynomial.Gal.rootsEquivRootsdefMathlib.FieldTheory.PolynomialGaloisGroup, function or constantWording
the root equivalence root of p (from the name)
English
Let $p$ be a polynomial of $F$. Let $E$ and $\mathrm{E'}$ be sets. Then the root equivalence root of $p$ is an equivalence from the set of elements of the root set of $p$ and $E$ to the set of elements of the root set of $p$ and $\mathrm{E'}$ defined as the composition of the inverse of $\operatorname{rootsEquivRootsAux}$ applied to $p$ and $E$ and $\operatorname{rootsEquivRootsAux}$ applied to $p$ and $\mathrm{E'}$.
Subfield.botEquivRatdefMathlib.FieldTheory.PrimeField, function or constantWording
the bottom equivalence rational number of K (from the name)
English
Let $K$ be a set. Then the bottom equivalence rational number of $K$ is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{1}})}$ and $\Rational$ defined as the composition of the subfield congruence of $\mathrm{Subfield\_\_bot\_eq\_of\_charZero}$ and the inverse of $\operatorname{rangeRestrictFieldEquiv}$ applied to the algebra map of $\Rational$ and $K$.
Subfield.botEquivZModdefMathlib.FieldTheory.PrimeField, function or constantEnglish
Let $K$ be a set. Let $p$ be an element of $\Natural$. Then $\operatorname{botEquivZMod}$ applied to $K$ and $p$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{2}})}$ and $\mathrm{ZMod}$ applied to $p$ defined as the composition of the subfield congruence of $\mathrm{Subfield\_\_bot\_eq\_of\_zmod\_algebra}$ applied to $p$ and the inverse of $\operatorname{rangeRestrictFieldEquiv}$ applied to the algebra map of $\mathrm{ZMod}$ applied to $p$ and $K$.
Field.powerBasisOfFiniteOfSeparabledefMathlib.FieldTheory.PrimitiveElement, function or constantWording
the power basis of F and E (from the name)
English
Let $F$ and $E$ be sets. Then the power basis of $F$ and $E$ is a power basis of $F$ and $E$.
AdjoinPthRootsdefMathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots, typeEnglish
Let $k$ be a set. Then an element of $\mathrm{AdjoinPthRoots}$ applied to $k$ is an element of the function that maps $k$ to $k$.
AdjoinPthRoots.rootdefMathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots, function or constantWording
the root of k (from the name)
English
Let $k$ be a set. Then the root of $k$ is a ring isomorphism of $k$ and $\mathrm{AdjoinPthRoots}$ applied to $k$ defined as the identity map of $k$.
IsPurelyInseparableclassMathlib.FieldTheory.PurelyInseparable.Basic, predicateEnglish
Let $F$ and $E$ be sets. Then we can say that $\mathrm{IsPurelyInseparable}$ holds for $F$ and $E$.
Subalgebra.perfectClosuredefMathlib.FieldTheory.PurelyInseparable.Basic, function or constantWording
the perfect closure of R in A (from the docstring)
English
Let $R$ and $A$ be sets. Let $p$ be a natural number. Then the perfect closure of $R$ in $A$ is a subalgebra of $R$ and $A$.
IsPurelyInseparable.HasExponentclassMathlib.FieldTheory.PurelyInseparable.Exponent, predicateEnglish
Let $K$ and $L$ be sets. Then we can say that $\operatorname{HasExponent}$ holds for $K$ and $L$.
IsPurelyInseparable.elemExponentdefMathlib.FieldTheory.PurelyInseparable.Exponent, function or constantWording
the exponent of K and a (from the docstring)
English
Let $K$ be a set. Let $a$ be an element of $L$. Then the exponent of $K$ and $a$ is a natural number.
IsPurelyInseparable.elemReductdefMathlib.FieldTheory.PurelyInseparable.Exponent, function or constantWording
the element of K and a (from the docstring)
English
Let $K$ be a set. Let $a$ be an element of $L$. Then the element of $K$ and $a$ is an element of $K$.
IsPurelyInseparable.exponentdefMathlib.FieldTheory.PurelyInseparable.Exponent, function or constantWording
the exponent of K and L (from the name)
English
Let $K$ and $L$ be sets. Then the exponent of $K$ and $L$ is a natural number defined as $\operatorname{find}$ applied to $\mathrm{IsPurelyInseparable\_\_HasExponent\_\_has\_exponent}$.
IsPurelyInseparable.iterateFrobeniusdefMathlib.FieldTheory.PurelyInseparable.Exponent, function or constantEnglish
Let $K$ and $L$ be sets. Let $p$ be a natural number. Assume that the exponent of $K$ and $L$ is less than or equal to $n$. Then $\operatorname{iterateFrobenius}$ applied to $K$, $L$, $p$ and $\mathrm{hn}$ is a ring homomorphism of $L$ and $K$.
IsPurelyInseparable.iterateFrobeniusₛₗdefMathlib.FieldTheory.PurelyInseparable.Exponent, function or constantEnglish
Let $F$, $K$ and $L$ be sets. Let $p$ be a natural number. Assume that the exponent of $K$ and $L$ is less than or equal to $n$. Then $\mathrm{IsPurelyInseparable\_\_iterateFrobenius\_u209b\_\_u2097\_}$ applied to $F$, $K$, $L$, $p$ and $\mathrm{hn}$ is a linear map of $L$ and $K$.
AlgEquiv.perfectClosuredefMathlib.FieldTheory.PurelyInseparable.PerfectClosure, function or constantWording
the perfect closure of i (from the name)
English
Let $i$ be an algebra isomorphism of $E$ and $K$. Then the perfect closure of $i$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{perfectClosure} (F , E)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{perfectClosure} (F , K)}{x_{6}})}$ defined as the algebra isomorphism of $i$.
Module.Basis.mapPowExpCharPowOfIsSeparabledefMathlib.FieldTheory.PurelyInseparable.PerfectClosure, function or constantWording
the map power exponential characteristic power of n and b (from the name)
English
Let $q$ and $n$ be natural numbers. Let $b$ be a basis of $F$ and $E$. Then the map power exponential characteristic power of $n$ and $b$ is a basis of $F$ and $E$.
perfectClosuredefMathlib.FieldTheory.PurelyInseparable.PerfectClosure, function or constantWording
the perfect closure of F and E (from the name)
English
Let $F$ and $E$ be sets. Then the perfect closure of $F$ and $E$ is an intermediate field of $F$ and $E$.
perfectClosure.algEquivOfAlgEquivdefMathlib.FieldTheory.PurelyInseparable.PerfectClosure, function or constantWording
the algebra isomorphism of i (from the name)
English
Let $i$ be an algebra isomorphism of $E$ and $K$. Then the algebra isomorphism of $i$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{perfectClosure} (F , E)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{perfectClosure} (F , K)}{x_{6}})}$ defined as the composition of the intermediate field map of $i$ and the perfect closure of $F$ and $E$ and the equivalence of $\mathrm{perfectClosure\_\_map\_eq\_of\_algEquiv}$ applied to $i$.
Polynomial.idealXdefMathlib.FieldTheory.RatFunc.AsPolynomial, function or constantWording
the ideal of K (from the name)
English
Let $K$ be a set. Then the ideal of $K$ is a height one spectrum of the set of polynomials of $K$.
RatFunc.CdefMathlib.FieldTheory.RatFunc.AsPolynomial, function or constantEnglish
$\operatorname{C}$ is a ring homomorphism of $K$ and the set of rational number functions of $K$ defined as the algebra map of $K$ and the set of rational number functions of $K$.
RatFunc.XdefMathlib.FieldTheory.RatFunc.AsPolynomial, function or constantEnglish
$\operatorname{X}$ is a rational number function of $K$ defined as $\operatorname{algebraMap}$ applied to the set of polynomials of $K$, the set of rational number functions of $K$ and $\operatorname{X}$.
RatFunc.algEquivOfTranscendentaldefMathlib.FieldTheory.RatFunc.AsPolynomial, function or constantWording
the algebra isomorphism of f and h (from the name)
English
Let $f$ be a transcendental element of $L$. Then the algebra isomorphism of $f$ and $h$ is an algebra isomorphism of the set of rational number functions of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{adjoin} (K , \operatorname{singleton} (f))}{x_{3}})}$ defined as the algebra isomorphism of the algebra isomorphism of $f$.
RatFunc.evaldefMathlib.FieldTheory.RatFunc.AsPolynomial, function or constantWording
the evaluation of a and p (from the name)
English
Let $f$ be a ring homomorphism of $K$ and $L$. Let $a$ be an element of $L$. Let $p$ be a rational number function of $K$. Then the evaluation of $a$ and $p$ is an element of $L$ defined as the quotient of the evaluation of $a$ and the numerator of $p$ and the evaluation of $a$ and the denominator of $p$.
RatFunc.adddefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the sum of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be rational number functions of $K$. Then the sum of $x_{1}$ and $x_{2}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_28348954\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$ and $x_{2}$.
RatFunc.coePolynomialdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the coercion polynomial of P (from the name)
English
Let $P$ be a polynomial of $K$. Then the coercion polynomial of $P$ is a rational number function of $K$ defined as $\operatorname{algebraMap}$ applied to the set of polynomials of $K$, the set of rational number functions of $K$ and $P$.
RatFunc.denomdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the denominator of x1 (from the docstring)
English
Let $x_{1}$ be a rational number function of $K$. Then the denominator of $x_{1}$ is a polynomial of $K$ defined as $\ProdsndMACRoAA {\operatorname{numDenom} (x_{1})}$.
RatFunc.divdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the quotient of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be rational number functions of $K$. Then the quotient of $x_{1}$ and $x_{2}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_3298078443\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$ and $x_{2}$.
RatFunc.invdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the inverse of x1 (from the name)
English
Let $x_{1}$ be a rational number function of $K$. Then the inverse of $x_{1}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_3307059979\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{1}$.
RatFunc.liftAlgHomdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the lift algebra homomorphism of x5 and h1 (from the name)
English
Let $x_{5}$ be an algebra homomorphism of the set of polynomials of $K$ and $L$ such that the non zero divisor of the set of polynomials of $K$ is less than or equal to the preimage of $x_{5}$ and the non zero divisor of $L$. Then the lift algebra homomorphism of $x_{5}$ and $h_{1}$ is an algebra homomorphism of the set of rational number functions of $K$ and $L$.
RatFunc.liftMonoidWithZeroHomdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the lift monoid with zero homomorphism of x3 and h (from the name)
English
Let $x_{3}$ be a monoid with zero homomorphism of the set of polynomials of $R$ and $x$ such that the non zero divisor of the set of polynomials of $R$ is less than or equal to the preimage of $x_{3}$ and the non zero divisor of $x$. Then the lift monoid with zero homomorphism of $x_{3}$ and $h$ is a monoid with zero homomorphism of the set of rational number functions of $R$ and $x$.
RatFunc.liftRingHomdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the lift ring homomorphism of x2 and h (from the name)
English
Let $x_{2}$ be a ring homomorphism of the set of polynomials of $R$ and $L$ such that the non zero divisor of the set of polynomials of $R$ is less than or equal to the preimage of $x_{2}$ and the non zero divisor of $L$. Then the lift ring homomorphism of $x_{2}$ and $h$ is a ring homomorphism of the set of rational number functions of $R$ and $L$.
RatFunc.mapdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the map of x3 and h1 (from the name)
English
Let $x_{3}$ be an element of $F$ such that the non zero divisor of the set of polynomials of $R$ is less than or equal to the preimage of $x_{3}$ and the non zero divisor of the set of polynomials of $S$. Then the map of $x_{3}$ and $h_{1}$ is a monoid homomorphism of the set of rational number functions of $R$ and the set of rational number functions of $S$.
RatFunc.mapAlgHomdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the map algebra homomorphism of x5 and h2 (from the name)
English
Let $x_{5}$ be an algebra homomorphism of the set of polynomials of $K$ and the set of polynomials of $R$ such that the non zero divisor of the set of polynomials of $K$ is less than or equal to the preimage of $x_{5}$ and the non zero divisor of the set of polynomials of $R$. Then the map algebra homomorphism of $x_{5}$ and $h_{2}$ is an algebra homomorphism of the set of rational number functions of $K$ and the set of rational number functions of $R$.
RatFunc.mapRingHomdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the map ring homomorphism of x3 and h1 (from the name)
English
Let $x_{3}$ be an element of $F$ such that the non zero divisor of the set of polynomials of $R$ is less than or equal to the preimage of $x_{3}$ and the non zero divisor of the set of polynomials of $S$. Then the map ring homomorphism of $x_{3}$ and $h_{1}$ is a ring homomorphism of the set of rational number functions of $R$ and the set of rational number functions of $S$.
RatFunc.muldefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the product of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be rational number functions of $K$. Then the product of $x_{1}$ and $x_{2}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_2535021678\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$ and $x_{2}$.
RatFunc.negdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the negation of x1 (from the name)
English
Let $x_{1}$ be a rational number function of $K$. Then the negation of $x_{1}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_870781102\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{1}$.
RatFunc.numdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the numerator of x1 (from the docstring)
English
Let $x_{1}$ be a rational number function of $K$. Then the numerator of $x_{1}$ is a polynomial of $K$ defined as $\ProdfstMACRoZ {\operatorname{numDenom} (x_{1})}$.
RatFunc.numDenomdefMathlib.FieldTheory.RatFunc.Basic, function or constantEnglish
Let $x_{1}$ be a rational number function of $K$. Then $\operatorname{numDenom}$ applied to $x_{1}$ is an element of $\mathrm{Prod}$ applied to the set of polynomials of $K$ and the set of polynomials of $K$.
RatFunc.onedefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the one (from the name)
English
The one is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_2569038123\_\_\_hygCtx\_\_\_hyg\_\_2}$.
RatFunc.smuldefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the scalar multiple of x2 and x3 (from the name)
English
Let $x_{2}$ be an element of $R$. Let $x_{3}$ be a rational number function of $K$. Then the scalar multiple of $x_{2}$ and $x_{3}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_2982343433\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{2}$ and $x_{3}$.
RatFunc.subdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the difference of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be rational number functions of $K$. Then the difference of $x_{1}$ and $x_{2}$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_1611123591\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$ and $x_{2}$.
RatFunc.toFractionRingAlgEquivdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the fraction ring algebra isomorphism of K and R (from the name)
English
Let $K$ and $R$ be sets. Then the fraction ring algebra isomorphism of $K$ and $R$ is an algebra isomorphism of the set of rational number functions of $K$ and the set of fraction rings of the set of polynomials of $K$.
RatFunc.toFractionRingRingEquivdefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the fraction ring ring isomorphism of K (from the name)
English
Let $K$ be a set. Then the fraction ring ring isomorphism of $K$ is a ring isomorphism of the set of rational number functions of $K$ and the set of fraction rings of the set of polynomials of $K$.
RatFunc.zerodefMathlib.FieldTheory.RatFunc.Basic, function or constantWording
the zero rational function (from the docstring)
English
The zero rational function is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Basic\_\_1687740377\_\_\_hygCtx\_\_\_hyg\_\_2}$.
RatFuncstructureMathlib.FieldTheory.RatFunc.Defs, typeWording
rational number function of K (from the name)
English
Let $K$ be a set. Then the rational number functions of $K$ are a basic type.
RatFunc.liftOndefMathlib.FieldTheory.RatFunc.Defs, function or constantEnglish
Let $x_{1}$ be a rational number function of $K$. Let $f$ be a function from polynomials of $K$ and polynomials of $K$ to elements of $P$ such that for all polynomials $p$, $q$, $\mathrm{p'}$ and $\mathrm{q'}$ of $K$, if $q$ is an element of the non zero divisor of the set of polynomials of $K$, then if $\mathrm{q'}$ is an element of the non zero divisor of the set of polynomials of $K$, then if $\EqtMACRoH {\mathrm{q'} \times p}{q \times \mathrm{p'}}$, then $\EqtMACRoH {f (p , q)}{f (\mathrm{p'} , \mathrm{q'})}$. Then $\operatorname{liftOn}$ applied to $x_{1}$, $f$ and $H$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Defs\_\_3348800825\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$, $f$ and $H$.
RatFunc.liftOn'defMathlib.FieldTheory.RatFunc.Defs, function or constantEnglish
Let $x_{1}$ be a rational number function of $K$. Let $f$ be a function from polynomials of $K$ and polynomials of $K$ to elements of $P$ such that for all polynomials $p$, $q$ and $a$ of $K$, if $q \neq 0$, then if $a \neq 0$, then $\EqtMACRoH {f (a \times p , a \times q)}{f (p , q)}$. Then $\operatorname{liftOn'}$ applied to $x_{1}$, $f$ and $H$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Defs\_\_574961263\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$, $f$ and $H$.
RatFunc.mkdefMathlib.FieldTheory.RatFunc.Defs, function or constantEnglish
Let $p$ and $q$ be polynomials of $K$. Then $\operatorname{mk}$ applied to $p$ and $q$ is a rational number function of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{RatFunc\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_FieldTheory\_\_RatFunc\_\_Defs\_\_953219046\_\_\_hygCtx\_\_\_hyg\_\_2}$, $p$ and $q$.
RatFunc.toFractionRingdefMathlib.FieldTheory.RatFunc.Defs, function or constantWording
the coercion to the fraction ring of the polynomial ring of self (from the docstring)
English
Let $\mathrm{self}$ be a rational number function of $K$. Then the coercion to the fraction ring of the polynomial ring of $\mathrm{self}$ is a fraction ring of the set of polynomials of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
RatFunc.intDegreedefMathlib.FieldTheory.RatFunc.Degree, function or constantWording
the integer degree of x1 (from the name)
English
Let $x_{1}$ be a rational number function of $K$. Then the integer degree of $x_{1}$ is an integer defined as the difference between the natural degree of the numerator of $x_{1}$ and the natural degree of the denominator of $x_{1}$.
RatFunc.minpolyXdefMathlib.FieldTheory.RatFunc.IntermediateField, function or constantWording
the minimal polynomial of f and A (from the name)
English
Let $f$ be a rational number function of $K$. Let $A$ be a set. Then the minimal polynomial of $f$ and $A$ is a polynomial of $A$ defined as the difference between the map of the algebra map of $K$ and $A$ and the numerator of $f$ and the product of $\operatorname{C}$ applied to $\operatorname{algebraMap}$ applied to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (K , \operatorname{singleton} (f))}{x_{5}})}$, $A$ and $f$ and the map of the algebra map of $K$ and $A$ and the denominator of $f$.
RatFunc.Luroth.algEquivdefMathlib.FieldTheory.RatFunc.Luroth, function or constantWording
the algebra isomorphism of h (from the name)
English
Assume that $E$ is distinct from the bottom. Then the algebra isomorphism of $h$ is an algebra isomorphism of the set of rational number functions of $K$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {E}{x_{1}})}$.
RatFunc.Luroth.generatordefMathlib.FieldTheory.RatFunc.Luroth, function or constantWording
the generator of E (from the name)
English
Let $E$ be an intermediate field of $K$ and the set of rational number functions of $K$. Then the generator of $E$ is a rational number function of $K$.
RatFunc.CompletionAtInftydefMathlib.FieldTheory.RatFunc.Valuation, typeWording
completion at infty of F (from the name)
English
Let $F$ be a set. Then a completion at infty of $F$ is an element of the function that maps $F$ to the set of completions of the set of rational number functions of $F$.
RatFunc.inftyValuationdefMathlib.FieldTheory.RatFunc.Valuation, function or constantWording
the infty valuation of F (from the name)
English
Let $F$ be a set. Then the infty valuation of $F$ is a valuation of the set of rational number functions of $F$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inftyValuationDef}$ applied to $F$ and $\mathrm{RatFunc\_\_InftyValuation\_\_map\_zero'}$ applied to $F$, $\mathrm{RatFunc\_\_InftyValuation\_\_map\_one'}$ applied to $F$ and $\mathrm{RatFunc\_\_InftyValuation\_\_map\_mul'}$ applied to $F$ and $\mathrm{RatFunc\_\_InftyValuation\_\_map\_add\_le\_max'}$ applied to $F$.
RatFunc.inftyValuationDefdefMathlib.FieldTheory.RatFunc.Valuation, function or constantWording
the valuation at infinity of F and r (from the docstring)
English
Let $F$ be a set. Let $r$ be a rational number function of $F$. Then the valuation at infinity of $F$ and $r$ is an element of $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as $\iteMACRoG {(\EqtMACRoH {r}{0})}{0}{\operatorname{exp} (\operatorname{intDegree} (r))}$.
Subfield.relfinrankdefMathlib.FieldTheory.Relrank, function or constantEnglish
Let $A$ and $B$ be subfields of $E$. Then $\operatorname{relfinrank}$ applied to $A$ and $B$ is a natural number.
Subfield.relrankdefMathlib.FieldTheory.Relrank, function or constantEnglish
Let $A$ and $B$ be subfields of $E$. Then $\operatorname{relrank}$ applied to $A$ and $B$ is a cardinal.
Algebra.IsSeparableclassMathlib.FieldTheory.Separable, predicateEnglish
Let $F$ and $K$ be sets. Then we can say that $\operatorname{IsSeparable}$ holds for $F$ and $K$.
IsSeparabledefMathlib.FieldTheory.Separable, predicateWording
x3 is separable (from the name)
English
Let $F$ be a set. Let $x_{3}$ be an element of $K$. Then $x_{3}$ is separable, if the minimal polynomial of $F$ and $x_{3}$ is separable.
Polynomial.SeparabledefMathlib.FieldTheory.Separable, predicateWording
f is separable (from the name)
English
Let $f$ be a polynomial of $R$. Then $f$ is separable, if $f$ is coprime to $\operatorname{derivative}$ applied to $f$.
AlgEquiv.separableClosuredefMathlib.FieldTheory.SeparableClosure, function or constantWording
the separable closure of i (from the name)
English
Let $i$ be an algebra isomorphism of $E$ and $K$. Then the separable closure of $i$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , E)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , K)}{x_{6}})}$ defined as the algebra isomorphism of $i$.
Field.finInsepDegreedefMathlib.FieldTheory.SeparableClosure, function or constantWording
the finite inseparable degree of F and E (from the docstring)
English
Let $F$ and $E$ be sets. Then the finite inseparable degree of $F$ and $E$ is an element of $\Natural$ defined as the rank of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , E)}{x_{3}})}$ and $E$.
Field.insepDegreedefMathlib.FieldTheory.SeparableClosure, function or constantEnglish
Let $F$ and $E$ be sets. Then $\operatorname{insepDegree}$ applied to $F$ and $E$ is a cardinal defined as the rank of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , E)}{x_{3}})}$ and $E$.
Field.sepDegreedefMathlib.FieldTheory.SeparableClosure, function or constantEnglish
Let $F$ and $E$ be sets. Then $\operatorname{sepDegree}$ applied to $F$ and $E$ is a cardinal defined as the rank of $F$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , E)}{x_{3}})}$.
separableClosuredefMathlib.FieldTheory.SeparableClosure, function or constantWording
the separable closure of F and E (from the name)
English
Let $F$ and $E$ be sets. Then the separable closure of $F$ and $E$ is an intermediate field of $F$ and $E$.
separableClosure.algEquivOfAlgEquivdefMathlib.FieldTheory.SeparableClosure, function or constantWording
the algebra isomorphism of i (from the name)
English
Let $i$ be an algebra isomorphism of $E$ and $K$. Then the algebra isomorphism of $i$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , E)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{separableClosure} (F , K)}{x_{6}})}$ defined as the composition of the intermediate field map of $i$ and the separable closure of $F$ and $E$ and the equivalence of $\mathrm{separableClosure\_\_map\_eq\_of\_algEquiv}$ applied to $i$.
separableClosureOperatordefMathlib.FieldTheory.SeparableClosure, function or constantWording
the separable closure operator of F and E (from the name)
English
Let $F$ and $E$ be sets. Then the separable closure operator of $F$ and $E$ is a closure operator of the set of intermediate fields of $F$ and $E$.
Field.EmbdefMathlib.FieldTheory.SeparableDegree, typeWording
embedding of F and E (from the name)
English
Let $F$ and $E$ be sets. Then an embedding of $F$ and $E$ is an element of the function that maps $F$ and $E$ to the set of algebra homomorphisms of $E$ and the set of algebraic closures of $E$.
Field.embEquivOfAdjoinSplitsdefMathlib.FieldTheory.SeparableDegree, function or constantWording
the embedding equivalence of hS and hK (from the name)
English
Let $F$, $E$ and $K$ be sets such that $\operatorname{adjoin}$ applied to $F$ and $S$ is equal to the top and for all elements $s$ of $E$, if $s$ is an element of $S$, then $s$ is integral and $\operatorname{Splits}$ holds for the map of the algebra map of $F$ and $K$ and the minimal polynomial of $F$ and $s$. Then the embedding equivalence of $\mathrm{hS}$ and $\mathrm{hK}$ is an equivalence from the set of embeddings of $F$ and $E$ to the set of algebra homomorphisms of $E$ and $K$.
Field.embEquivOfEquivdefMathlib.FieldTheory.SeparableDegree, function or constantWording
the embedding equivalence of i (from the name)
English
Let $F$, $E$ and $K$ be sets. Let $i$ be an algebra isomorphism of $E$ and $K$. Then the embedding equivalence of $i$ is an equivalence from the set of embeddings of $F$ and $E$ to the set of embeddings of $F$ and $K$ defined as the arrow congruence of $i$ and the inverse of $\operatorname{restrictScalars}$ applied to $F$ and the equivalence of the set of algebraic closures of $K$ and the set of algebraic closures of $E$.
Field.embEquivOfIsAlgCloseddefMathlib.FieldTheory.SeparableDegree, function or constantWording
the embedding equivalence of E and K (from the name)
English
Let $F$, $E$ and $K$ be sets. Then the embedding equivalence of $E$ and $K$ is an equivalence from the set of embeddings of $F$ and $E$ to the set of algebra homomorphisms of $E$ and $K$.
Field.embProdEmbOfIsAlgebraicdefMathlib.FieldTheory.SeparableDegree, function or constantWording
the embedding product embedding of E and K (from the name)
English
Let $F$, $E$ and $K$ be sets. Then the embedding product embedding of $E$ and $K$ is an equivalence from $\mathrm{Prod}$ applied to the set of embeddings of $F$ and $E$ and the set of embeddings of $E$ and $K$ to the set of embeddings of $F$ and $K$ defined as the inverse of the composition of the composition of the algebra homomorphism equivalence sigma and the sigma equivalence product of the function that maps $f$ to the inverse of the embedding equivalence of $K$ and the set of algebraic closures of $K$ and the left product congruence of the function that maps $x_{6}$ to the arrow congruence of the identity and $\operatorname{restrictScalars}$ applied to $F$ and the equivalence of the set of algebraic closures of $K$ and the set of algebraic closures of $E$.
Field.finSepDegreedefMathlib.FieldTheory.SeparableDegree, function or constantEnglish
Let $F$ and $E$ be sets. Then $\operatorname{finSepDegree}$ applied to $F$ and $E$ is a natural number defined as the cardinality of the set of embeddings of $F$ and $E$.
Polynomial.natSepDegreedefMathlib.FieldTheory.SeparableDegree, function or constantWording
the separable degree of f (from the docstring)
English
Let $f$ be a polynomial of $F$. Then the separable degree of $f$ is a natural number defined as the cardinality of the finite set of $\operatorname{aroots}$ applied to $f$ and the set of splitting fields of $f$.
MvPolynomial.toPolynomialAdjoinImageCompldefMathlib.FieldTheory.SeparablyGenerated, function or constantEnglish
Let $F$ be a multivariate polynomial of $x$ and $k$. Let $a$ be a function from elements of $x$ to elements of $K$. Let $i$ be an element of $x$. Then $\operatorname{toPolynomialAdjoinImageCompl}$ applied to $F$, $a$ and $i$ is a polynomial of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (k , \operatorname{image} (a , \operatorname{compl} (\operatorname{singleton} (i))))}{x_{4}})}$ defined as $\operatorname{mapAlgHom}$ applied to the algebra evaluation of the function that maps $j_{1}$ to $a$ applied to $j_{1}$ and $\operatorname{optionEquivLeft}$ applied to $k$, $\SubtypeSet {b_{3}}{\mathrm{Neq} (b_{3} , i)}$ and $\operatorname{renameEquiv}$ applied to $k$, the inverse of $\operatorname{optionSubtypeNe}$ applied to $i$ and $F$.
Polynomial.IsSplittingField.algEquivdefMathlib.FieldTheory.SplittingField.Construction, function or constantWording
the algebra isomorphism of L and f (from the name)
English
Let $L$ be a set. Let $f$ be a polynomial of $K$. Then the algebra isomorphism of $L$ and $f$ is an algebra isomorphism of $L$ and the set of splitting fields of $f$.
Polynomial.SplittingFielddefMathlib.FieldTheory.SplittingField.Construction, typeWording
splitting field of f (from the name)
English
Let $f$ be a polynomial of $K$. Then a splitting field of $f$ is an element of the function that maps $f$ to the set of quotients of the set of multivariate polynomials of $\operatorname{SplittingFieldAux}$ applied to the natural degree of $f$ and $f$ and $K$ and the kernel of $\operatorname{toRingHom}$ applied to the algebra evaluation of $\mathrm{id}$.
Polynomial.SplittingField.liftdefMathlib.FieldTheory.SplittingField.Construction, function or constantWording
the lift of f and hb (from the name)
English
Let $f$ be a polynomial of $K$ such that $\operatorname{Splits}$ holds for the map of the algebra map of $K$ and $L$ and $f$. Then the lift of $f$ and $\mathrm{hb}$ is an algebra homomorphism of the set of splitting fields of $f$ and $L$ defined as the lift of $f$.
Polynomial.factordefMathlib.FieldTheory.SplittingField.Construction, function or constantWording
the factor of f (from the name)
English
Let $f$ be a polynomial of $K$. Then the factor of $f$ is a polynomial of $K$ defined as $\mathrm{dite}$ applied to the proposition that there exists a polynomial $g$ of $K$, such that $g$ is irreducible and $g$ divides $f$, the function that maps $H$ to $\operatorname{choose}$ applied to $H$ and the function that maps $H_{1}$ to $\operatorname{X}$.
Polynomial.removeFactordefMathlib.FieldTheory.SplittingField.Construction, function or constantEnglish
Let $f$ be a polynomial of $K$. Then $\operatorname{removeFactor}$ applied to $f$ is a polynomial of $\mathrm{AdjoinRoot}$ applied to the factor of $f$ defined as $\operatorname{divByMonic}$ applied to the map of $\operatorname{of}$ applied to the factor of $f$ and $f$ and the difference between $\operatorname{X}$ and $\operatorname{C}$ applied to the adjoined root of the factor of $f$.
Polynomial.IsSplittingFieldclassMathlib.FieldTheory.SplittingField.IsSplittingField, predicateWording
f is a splitting field (from the name)
English
Let $K$ and $L$ be sets. Let $f$ be a polynomial of $K$. Then we can say that $f$ is a splitting field.
Polynomial.IsSplittingField.liftdefMathlib.FieldTheory.SplittingField.IsSplittingField, function or constantWording
the lift of f (from the name)
English
Let $L$ be a set. Let $f$ be a polynomial of $K$ such that $\operatorname{Splits}$ holds for the map of the algebra map of $K$ and $F$ and $f$. Then the lift of $f$ is an algebra homomorphism of $L$ and $F$.
Algebra.IsSeparablyGeneratedclassMathlib.FieldTheory.TranscendentalSeparable, predicateEnglish
Let $k$ and $K$ be sets. Then we can say that $\operatorname{IsSeparablyGenerated}$ holds for $k$ and $K$.
Algebra.IsTranscendentalSeparableclassMathlib.FieldTheory.TranscendentalSeparable, predicateEnglish
Let $k$ and $K$ be sets. Then we can say that $\operatorname{IsTranscendentalSeparable}$ holds for $k$ and $K$.