Definitions: Mathlib.RingTheory, part 2 of 6

399 definitions of 53 modules, Mathlib.RingTheory.Discriminant to Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring. ‹ previous next ›

Mathlib.RingTheory.Discriminant

Algebra.discrdefMathlib.RingTheory.Discriminant, function or constant
Wording
no wording
English
Let $A$ be a set. Let $b$ be a function from elements of $x$ to elements of $B$. Then $\operatorname{discr}$ applied to $A$ and $b$ is an element of $A$ defined as the determinant of the trace matrix of $A$ and $b$.

Mathlib.RingTheory.DividedPowerAlgebra.Init

DividedPowerAlgebradefMathlib.RingTheory.DividedPowerAlgebra.Init, type
Wording
divided power algebra of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a divided power algebra of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of quotients of the ring congruence relation of $R$ and $M$.
DividedPowerAlgebra.RelinductiveMathlib.RingTheory.DividedPowerAlgebra.Init, predicate
Wording
no wording
English
Let $R$ and $M$ be sets. Let $x_{3}$ and $x_{4}$ be multivariate polynomials of $\mathrm{Prod}$ applied to $\Natural$ and $M$ and $R$. Then we can say that $\operatorname{Rel}$ holds for $R$, $M$, $x_{3}$ and $x_{4}$.
DividedPowerAlgebra.RelIdefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
no wording
English
Let $R$ and $M$ be sets. Then $\operatorname{RelI}$ applied to $R$ and $M$ is an ideal of the set of multivariate polynomials of $\mathrm{Prod}$ applied to $\Natural$ and $M$ and $R$ defined as the ideal generated by an arbitrary binary relation of $\operatorname{Rel}$ applied to $R$ and $M$.
DividedPowerAlgebra.dpdefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
no wording
English
Let $R$ be a set. Let $n$ be a natural number. Let $m$ be an element of $M$. Then $\operatorname{dp}$ applied to $R$, $n$ and $m$ is a divided power algebra of $R$ and $M$ defined as the morphism into the quotient by a congruence relation of $\operatorname{X}$ applied to $\ProdmkMACRoU {n}{m}$.
DividedPowerAlgebra.embeddefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
the embed of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the embed of $R$ and $M$ is a linear map of $M$ and the set of divided power algebras of $R$ and $M$.
DividedPowerAlgebra.liftdefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
the lift of hI and g (from the name)
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $g$ be a linear map of $M$ and $A$ such that for all elements $m$ of $M$, $\MembershipmemMACRoT {I}{g (m)}$. Then the lift of $\mathrm{hI}$ and $g$ is an algebra homomorphism of the set of divided power algebras of $R$ and $M$ and $A$.
DividedPowerAlgebra.lift'defMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
the lift of hf_mul and hf_add (from the name)
English
Assume that for all elements $m_{2}$ of $M$, $\EqtMACRoH {f (\ProdmkMACRoU {0}{m_{2}})}{1}$. Assume that for all natural numbers $n_{2}$, for all elements $r$ of $R$, for all elements $m_{1}$ of $M$, $\EqtMACRoH {f (\ProdmkMACRoU {n_{2}}{(\HSMulhSMulMACRoAL {r}{m_{1}})})}{\HSMulhSMulMACRoAL {(r ^ {n_{2}})}{f (\ProdmkMACRoU {n_{2}}{m_{1}})}}$. Assume that for all natural numbers $n_{1}$ and $p$, for all elements $m$ of $M$, $f (\ProdmkMACRoU {n_{1}}{m})\times f (\ProdmkMACRoU {p}{m})$ is equal to $\HSMulhSMulMACRoAL {\operatorname{choose} (n_{1} + p , n_{1})}{f (\ProdmkMACRoU {(n_{1} + p)}{m})}$. Assume that for all natural numbers $n$, for all elements $u$ and $v$ of $M$, $\EqtMACRoH {f (\ProdmkMACRoU {n}{(u + v)})}{\FinsetSum {\operatorname{antidiagonal} (n)}{x_{5}}{\mathrm{DividedPowerAlgebra\_\_lift'\_\_match\_1} (\lambda x_{6} . A , x_{5} , \lambda k . \lambda l . f (\ProdmkMACRoU {k}{u})\times f (\ProdmkMACRoU {l}{v}))}}$. Then the lift of $\mathrm{hf\_mul}$ and $\mathrm{hf\_add}$ is an algebra homomorphism of the set of divided power algebras of $R$ and $M$ and $A$.
DividedPowerAlgebra.mapdefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
the map of S and f (from the name)
English
Let $S$ be a set. Let $f$ be a linear map of $M$ and $N$. Then the map of $S$ and $f$ is an algebra homomorphism of the set of divided power algebras of $R$ and $M$ and the set of divided power algebras of $S$ and $N$.
DividedPowerAlgebra.mapEquivdefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
the map equivalence of g (from the name)
English
Let $g$ be a linear equivalence of $M$ and $N$. Then the map equivalence of $g$ is an algebra isomorphism of the set of divided power algebras of $R$ and $M$ and the set of divided power algebras of $R$ and $N$.
DividedPowerAlgebra.ringCondefMathlib.RingTheory.DividedPowerAlgebra.Init, function or constant
Wording
the ring congruence relation of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the ring congruence relation of $R$ and $M$ is a ring congruence relation of the set of multivariate polynomials of $\mathrm{Prod}$ applied to $\Natural$ and $M$ and $R$ defined as the ring congruence relation generator of $\operatorname{Rel}$ applied to $R$ and $M$.

Mathlib.RingTheory.DividedPowers.Basic

DividedPowersstructureMathlib.RingTheory.DividedPowers.Basic, type
Wording
divided power of I (from the name)
English
Let $I$ be an ideal of $A$. Then the divided powers of $I$ are a basic type.
DividedPowers.dpowdefMathlib.RingTheory.DividedPowers.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a divided power of $I$. Let $x_{1}$ be a natural number. Let $x_{2}$ be an element of $A$. Then $\operatorname{dpow}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
DividedPowers.equivdefMathlib.RingTheory.DividedPowers.Basic, function or constant
Wording
the equivalence of h (from the name)
English
Assume that the map of $e$ and $I$ is equal to $J$. Then the equivalence of $h$ is an equivalence from the set of divided powers of $I$ to the set of divided powers of $J$.
DividedPowers.expdefMathlib.RingTheory.DividedPowers.Basic, function or constant
Wording
the exponential series of hI and a (from the docstring)
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $a$ be an element of $A$. Then the exponential series of $\mathrm{hI}$ and $a$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{dpow}$ applied to $\mathrm{hI}$, $n$ and $a$.
DividedPowers.ofRingEquivdefMathlib.RingTheory.DividedPowers.Basic, function or constant
Wording
the divided power of h and hI (from the name)
English
Assume that the map of $e$ and $I$ is equal to $J$. Let $\mathrm{hI}$ be a divided power of $I$. Then the divided power of $h$ and $\mathrm{hI}$ is a divided power of $J$.
dividedPowersBotdefMathlib.RingTheory.DividedPowers.Basic, function or constant
Wording
the divided power bottom of A (from the name)
English
Let $A$ be a set. Then the divided power bottom of $A$ is a divided power of the bottom.

Mathlib.RingTheory.DividedPowers.DPMorphism

DividedPowers.DPMorphismstructureMathlib.RingTheory.DividedPowers.DPMorphism, type
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $\mathrm{hJ}$ be a divided power of $J$. Then the elements of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hJ}$ are a basic type.
DividedPowers.DPMorphism.compdefMathlib.RingTheory.DividedPowers.DPMorphism, function or constant
Wording
the composition of g and f (from the name)
English
Let $g$ be an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hJ}$ and $\mathrm{hK}$. Let $f$ be an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hJ}$. Then the composition of $g$ and $f$ is an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hK}$.
DividedPowers.DPMorphism.fromGensdefMathlib.RingTheory.DividedPowers.DPMorphism, function or constant
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $\mathrm{hJ}$ be a divided power of $J$. Assume that $I$ is equal to the span of $S$. Assume that the map of $f$ and $I$ is less than or equal to $J$. Assume that for all natural numbers $n$, for all elements $x_{2}$ of $A$, if $x_{2}$ is an element of $S$, then $\EqtMACRoH {f (\operatorname{dpow} (\mathrm{hI} , n , x_{2}))}{\operatorname{dpow} (\mathrm{hJ} , n , f (x_{2}))}$. Then $\operatorname{fromGens}$ applied to $\mathrm{hI}$, $\mathrm{hJ}$, $\mathrm{hS}$, $\mathrm{hf}$ and $h$ is an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hJ}$.
DividedPowers.DPMorphism.iddefMathlib.RingTheory.DividedPowers.DPMorphism, function or constant
Wording
the identity map of hI (from the docstring)
English
Let $\mathrm{hI}$ be a divided power of $I$. Then the identity map of $\mathrm{hI}$ is an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hI}$.
DividedPowers.DPMorphism.mk'defMathlib.RingTheory.DividedPowers.DPMorphism, function or constant
Wording
no wording
English
Assume that $\operatorname{IsDPMorphism}$ holds for $\mathrm{hI}$, $\mathrm{hJ}$ and $f$. Then $\operatorname{mk'}$ applied to $\mathrm{hf}$ is an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hJ}$ defined as $\operatorname{mk}$ applied to $f$, $\mathrm{DividedPowers\_\_IsDPMorphism\_\_ideal\_comp}$ applied to $\mathrm{hf}$ and the function that maps $x_{2}$ to $\mathrm{DividedPowers\_\_IsDPMorphism\_\_dpow\_comp}$ applied to $\mathrm{hf}$.
DividedPowers.IsDPMorphismstructureMathlib.RingTheory.DividedPowers.DPMorphism, predicate
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $\mathrm{hJ}$ be a divided power of $J$. Let $f$ be a ring homomorphism of $A$ and $B$. Then we can say that $\operatorname{IsDPMorphism}$ holds for $\mathrm{hI}$, $\mathrm{hJ}$ and $f$.
DividedPowers.ideal_from_ringHomdefMathlib.RingTheory.DividedPowers.DPMorphism, function or constant
Wording
the ideal from ring homomorphism of hI and hJ (from the name)
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $\mathrm{hJ}$ be a divided power of $J$. Assume that the map of $f$ and $I$ is less than or equal to $J$. Then the ideal from ring homomorphism of $\mathrm{hI}$ and $\mathrm{hJ}$ is an ideal of $A$.

Mathlib.RingTheory.DividedPowers.Padic

DividedPowers.ofInjectivedefMathlib.RingTheory.DividedPowers.Padic, function or constant
Wording
the divided power of f and hJ (from the name)
English
Let $I$ be an ideal of $A$. Let $J$ be an ideal of $B$. Let $f$ be a ring homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is injective. Let $\mathrm{hJ}$ be a divided power of $J$. Assume that the map of $f$ and $I$ is equal to $J$. Assume that for all natural numbers $n$, for all elements $x_{2}$ of $A$, if $x_{2}$ is an element of $I$, then there exists an element $y$ of $A$, such that there exists an element $h_{1}$ of $\mathrm{if}$ applied to $\mathrm{Neq} (n , 0)$ and $\MembershipmemMACRoT {I}{y}$, such that $\EqtMACRoH {f (y)}{\operatorname{dpow} (\mathrm{hJ} , n , f (x_{2}))}$. Then the divided power of $f$ and $\mathrm{hJ}$ is a divided power of $I$.
PadicInt.dividedPowersdefMathlib.RingTheory.DividedPowers.Padic, function or constant
Wording
the divided power of p (from the name)
English
Let $p$ be a natural number. Then the divided power of $p$ is a divided power of the span of $\operatorname{singleton}$ applied to $p$.

Mathlib.RingTheory.DividedPowers.RatAlgebra

DividedPowers.CharP.dividedPowersdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
the divided power of p (from the name)
English
Let $A$ be a set. Let $p$ be a natural number such that $\EqtMACRoH {I ^ {p}}{0}$. Then the divided power of $p$ is a divided power of $I$.
DividedPowers.IsNilpotent.dividedPowersdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
the divided power of hp and hIp (from the name)
English
Assume that $p$ is nilpotent. Assume that $\EqtMACRoH {I ^ {p}}{0}$. Then the divided power of $\mathrm{hp}$ and $\mathrm{hIp}$ is a divided power of $I$.
DividedPowers.OfInvertibleFactorial.dividedPowersdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
the divided power of hn_fac and hnI (from the name)
English
Assume that $(n - 1)!$ is a unit. Assume that $\EqtMACRoH {I ^ {n}}{0}$. Then the divided power of $\mathrm{hn\_fac}$ and $\mathrm{hnI}$ is a divided power of $I$ defined as $\operatorname{mk}$ applied to $\operatorname{dpow}$ applied to $I$, the function that maps $x_{2}$, $x_{3}$ and $\mathrm{hx}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_null}$ applied to $\mathrm{hx}$, the function that maps $x_{4}$ and $\mathrm{hx1}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_zero}$ applied to $\mathrm{hx1}$, the function that maps $x_{5}$ and $\mathrm{hx2}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_one}$ applied to $\mathrm{hx2}$, the function that maps $x_{6}$, $x_{7}$, $\mathrm{hn}$ and $\mathrm{hx3}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_mem}$ applied to $\mathrm{hn}$ and $\mathrm{hx3}$, the function that maps $x_{8}$, $x_{9}$, $x_{10}$, $\mathrm{hx4}$ and $\mathrm{hy}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_add}$ applied to $\mathrm{hn\_fac}$, $\mathrm{hnI}$, $\mathrm{hx4}$ and $\mathrm{hy}$, the function that maps $x_{11}$, $x_{12}$ and $x_{13}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_mul}$, the function that maps $x_{14}$, $x_{15}$, $x_{16}$ and $\mathrm{hx5}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_mul\_dpow}$ applied to $\mathrm{hn\_fac}$, $\mathrm{hnI}$ and $\mathrm{hx5}$ and the function that maps $x_{17}$, $x_{18}$, $x_{19}$, $\mathrm{hk}$ and $\mathrm{hx6}$ to $\mathrm{DividedPowers\_\_OfInvertibleFactorial\_\_dpow\_comp}$ applied to $\mathrm{hn\_fac}$, $\mathrm{hnI}$, $\mathrm{hk}$ and $\mathrm{hx6}$.
DividedPowers.OfInvertibleFactorial.dpowdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
no wording
English
Let $I$ be an ideal of $A$. Let $x_{2}$ be an element of $\Natural$. Let $x_{3}$ be an element of $A$. Then $\operatorname{dpow}$ applied to $I$, $x_{2}$ and $x_{3}$ is an element of $A$ defined as $\iteMACRoG {(\MembershipmemMACRoT {I}{x_{3}})}{(\operatorname{inverse} (x_{2} !)\times x_{3} ^ {x_{2}})}{0}$.
DividedPowers.OfSquareZero.dividedPowersdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
the divided power of hI2 (from the name)
English
Assume that $\EqtMACRoH {I ^ {2}}{0}$. Then the divided power of $\mathrm{hI2}$ is a divided power of $I$.
DividedPowers.RatAlgebra.dividedPowersdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
the divided power of I (from the name)
English
Let $I$ be an ideal of $R$. Then the divided power of $I$ is a divided power of $I$.
DividedPowers.RatAlgebra.dpowdefMathlib.RingTheory.DividedPowers.RatAlgebra, function or constant
Wording
no wording
English
Let $I$ be an ideal of $R$. Let $x_{2}$ be a natural number. Let $x_{3}$ be an element of $R$. Then $\operatorname{dpow}$ applied to $I$, $x_{2}$ and $x_{3}$ is an element of $R$ defined as $\operatorname{dpow}$ applied to $I$, $x_{2}$ and $x_{3}$.

Mathlib.RingTheory.DividedPowers.SubDPIdeal

DividedPowers.DPMorphism.kerdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the kernel of hJ and f (from the name)
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $\mathrm{hJ}$ be a divided power of $J$. Let $f$ be an element of $\operatorname{DPMorphism}$ applied to $\mathrm{hI}$ and $\mathrm{hJ}$. Then the kernel of $\mathrm{hJ}$ and $f$ is an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$.
DividedPowers.IsSubDPIdealstructureMathlib.RingTheory.DividedPowers.SubDPIdeal, predicate
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $J$ be an ideal of $A$. Then we can say that $\operatorname{IsSubDPIdeal}$ holds for $\mathrm{hI}$ and $J$.
DividedPowers.IsSubDPIdeal.dividedPowersdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the divided power structure of hI and hJ (from the docstring)
English
Let $\mathrm{hI}$ be a divided power of $I$ such that $\operatorname{IsSubDPIdeal}$ holds for $\mathrm{hI}$ and $J$. Then the divided power structure of $\mathrm{hI}$ and $\mathrm{hJ}$ is a divided power of $J$.
DividedPowers.Quotient.OfSurjective.dividedPowersdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the divided power of hI (from the name)
English
Let $\mathrm{hI}$ be a divided power of $I$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Assume that $J$ is equal to the map of $f$ and $I$. Assume that $\operatorname{IsSubDPIdeal}$ holds for $\mathrm{hI}$ and the minimum of the kernel of $f$ and $I$. Then the divided power of $\mathrm{hI}$ is a divided power of $J$.
DividedPowers.Quotient.OfSurjective.dpowdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $f$ be a ring homomorphism of $A$ and $B$. Let $x_{2}$ be a natural number. Let $x_{3}$ be an element of $B$. Then $\operatorname{dpow}$ applied to $\mathrm{hI}$, $f$, $x_{2}$ and $x_{3}$ is an element of $B$ defined as $\operatorname{extend}$ applied to the function that maps $a$ to $f$ applied to $a$, the function that maps $a_{1}$ to $f$ applied to $\operatorname{dpow}$ applied to $\mathrm{hI}$, $x_{2}$ and $a_{1}$, $0$ and $x_{3}$.
DividedPowers.Quotient.dividedPowersdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the divided power of hI and hIJ (from the name)
English
Let $\mathrm{hI}$ be a divided power of $I$ such that $\operatorname{IsSubDPIdeal}$ holds for $\mathrm{hI}$ and $\MinminMACRoAG {J}{I}$. Then the divided power of $\mathrm{hI}$ and $\mathrm{hIJ}$ is a divided power of the map of $\operatorname{mk}$ applied to $J$ and $I$.
DividedPowers.Quotient.dpowdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $J$ be an ideal of $A$. Let $x_{1}$ be a natural number. Let $x_{2}$ be a quotient of $A$ and $J$. Then $\operatorname{dpow}$ applied to $\mathrm{hI}$, $J$, $x_{1}$ and $x_{2}$ is a quotient of $A$ and $J$ defined as $\operatorname{dpow}$ applied to $\mathrm{hI}$, $\operatorname{mk}$ applied to $J$, $x_{1}$ and $x_{2}$.
DividedPowers.SubDPIdealstructureMathlib.RingTheory.DividedPowers.SubDPIdeal, type
Wording
no wording
English
Let $\mathrm{hI}$ be a divided power of $I$. Then the elements of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$ are a basic type.
DividedPowers.SubDPIdeal.carrierdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$. Then the carrier of $\mathrm{self}$ is an ideal of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
DividedPowers.SubDPIdeal.mk'defMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
no wording
English
Assume that $\operatorname{IsSubDPIdeal}$ holds for $\mathrm{hI}$ and $J$. Then $\operatorname{mk'}$ applied to $\mathrm{hJ}$ is an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$ defined as $\operatorname{mk}$ applied to $J$, $\operatorname{isSubideal}$ applied to $\mathrm{hJ}$ and $\mathrm{DividedPowers\_\_IsSubDPIdeal\_\_dpow\_mem}$ applied to $\mathrm{hJ}$.
DividedPowers.SubDPIdeal.proddefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the product of J (from the name)
English
Let $J$ be an ideal of $A$. Then the product of $J$ is an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$.
DividedPowers.SubDPIdeal.spandefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the span of hI and S (from the name)
English
Let $\mathrm{hI}$ be a divided power of $I$. Let $S$ be an element of $\wp A$. Then the span of $\mathrm{hI}$ and $S$ is an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $J$ to the proposition that $S$ is less than or equal to the carrier of $J$.
DividedPowers.SubDPIdeal.toIdealdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
the ideal of J (from the name)
English
Let $J$ be an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$. Then the ideal of $J$ is an ideal of $A$ defined as the carrier of $J$.
DividedPowers.dpEqualizerdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
no wording
English
Let $\mathrm{hI}$ and $\mathrm{hI'}$ be divided powers of $I$. Then $\operatorname{dpEqualizer}$ applied to $\mathrm{hI}$ and $\mathrm{hI'}$ is an ideal of $A$.
DividedPowers.subDPIdeal_inf_of_quotdefMathlib.RingTheory.DividedPowers.SubDPIdeal, function or constant
Wording
no wording
English
Assume that $\EqtMACRoH {\operatorname{toRingHom} (x_{1})}{\operatorname{mk} (J)}$. Then $\mathrm{DividedPowers\_\_subDPIdeal\_inf\_of\_quot}$ applied to $h$ is an element of $\operatorname{SubDPIdeal}$ applied to $\mathrm{hI}$.

Mathlib.RingTheory.EssentialFiniteness

Algebra.EssFiniteTypeclassMathlib.RingTheory.EssentialFiniteness, predicate
Wording
no wording
English
Let $R$ and $S$ be sets. Then we can say that $\operatorname{EssFiniteType}$ holds for $R$ and $S$.
Algebra.EssFiniteType.finsetdefMathlib.RingTheory.EssentialFiniteness, function or constant
Wording
the finite set of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the finite set of $R$ and $S$ is a finite set of $S$ defined as $\operatorname{choose}$ applied to $\operatorname{cond}$.
Algebra.EssFiniteType.subalgebradefMathlib.RingTheory.EssentialFiniteness, function or constant
Wording
the subalgebra of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the subalgebra of $R$ and $S$ is a subalgebra of $R$ and $S$ defined as $\operatorname{adjoin}$ applied to $R$ and the finite set of $R$ and $S$.
Algebra.EssFiniteType.submonoiddefMathlib.RingTheory.EssentialFiniteness, function or constant
Wording
the submonoid of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the submonoid of $R$ and $S$ is a submonoid of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{subalgebra} (R , S)}{x_{3}})}$ defined as the preimage of the algebra map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{subalgebra} (R , S)}{x_{3}})}$ and $S$ and the submonoid consisting of the units of $S$.
RingHom.EssFiniteTypedefMathlib.RingTheory.EssentialFiniteness, predicate
Wording
f is a essential finite type (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $f$ is an essential finite type, if $\operatorname{EssFiniteType}$ holds for $R$ and $S$.
RingHom.EssFiniteType.finsetdefMathlib.RingTheory.EssentialFiniteness, function or constant
Wording
the finite set of hf (from the name)
English
Assume that $f$ is an essential finite type. Then the finite set of $\mathrm{hf}$ is a finite set of $S$ defined as the finite set of $R$ and $S$.

Mathlib.RingTheory.Etale.Basic

Algebra.EtaleclassMathlib.RingTheory.Etale.Basic, predicate
Wording
no wording
English
Let $R$ and $A$ be sets. Then we can say that $\operatorname{Etale}$ holds for $R$ and $A$.
Algebra.FormallyEtaleclassMathlib.RingTheory.Etale.Basic, predicate
Wording
no wording
English
Let $R$ and $A$ be sets. Then we can say that $\operatorname{FormallyEtale}$ holds for $R$ and $A$.
RingHom.FormallyEtaledefMathlib.RingTheory.Etale.Basic, predicate
Wording
no wording
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{FormallyEtale}$ holds for $f$, if $\operatorname{FormallyEtale}$ holds for $R$ and $S$.

Mathlib.RingTheory.Etale.Field

Algebra.FormallyEtale.equivPiOfIsSepCloseddefMathlib.RingTheory.Etale.Field, function or constant
Wording
the equivalence product of K and A (from the name)
English
Let $K$ and $A$ be sets. Then the equivalence product of $K$ and $A$ is an algebra isomorphism of $A$ and the set of functions from prime spectra of $A$ to elements of $K$.

Mathlib.RingTheory.Etale.Finite

CommAlgCat.FiniteEtaledefMathlib.RingTheory.Etale.Finite, type
Wording
finite etale of R (from the name)
English
Let $R$ be a set. Then a finite etale of $R$ is an element of the function that maps $R$ to the set of full subcategories of the finite etale of $R$.
CommAlgCat.FiniteEtale.baseChangedefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the base change of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the base change of $R$ and $S$ is a functor of the set of finite etales of $R$ and the set of finite etales of $S$.
CommAlgCat.FiniteEtale.baseChangeSelfIsodefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the base change self isomorphism of R (from the name)
English
Let $R$ be a set. Then the base change self isomorphism of $R$ is an isomorphism of the base change of $R$ and $R$ and the identity of the set of finite etales of $R$.
CommAlgCat.FiniteEtale.equivOfIsSepCloseddefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the equivalence of x (from the name)
English
Let $x$ be a set. Then the equivalence of $x$ is an equivalence of the set of opposites of the set of finite etales of $x$ and the set of finite type categories.
CommAlgCat.FiniteEtale.fiberdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the fiber of R and x1 (from the name)
English
Let $R$ and $x_{1}$ be sets. Then the fiber of $R$ and $x_{1}$ is a functor of the set of opposites of the set of finite etales of $R$ and the set of finite type categories.
CommAlgCat.FiniteEtale.fiberIsoBaseChangeFiberdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the fiber isomorphism base change fiber of x1 and S (from the name)
English
Let $R$, $x_{1}$ and $S$ be sets. Then the fiber isomorphism base change fiber of $x_{1}$ and $S$ is an isomorphism of the fiber of $R$ and $x_{1}$ and the composition of the opposite of the base change of $R$ and $S$ and the fiber of $S$ and $x_{1}$.
CommAlgCat.FiniteEtale.fiberIsoCompdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the fiber isomorphism composition of R and x1 (from the name)
English
Let $R$ and $x_{1}$ be sets. Then the fiber isomorphism composition of $R$ and $x_{1}$ is an isomorphism of the fiber of $R$ and $x_{1}$ and the composition of the opposite of the base change of $R$ and $x_{1}$ and the finite spectrum of $x_{1}$ defined as the composition of the fiber isomorphism base change fiber of $x_{1}$ and $x_{1}$ and the left isomorphism whisker of the opposite of the base change of $R$ and $x_{1}$ and the fiber isomorphism finite spectrum of $x_{1}$.
CommAlgCat.FiniteEtale.fiberIsoFiniteSpecdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the fiber isomorphism finite spectrum of x (from the name)
English
Let $x$ be a set. Then the fiber isomorphism finite spectrum of $x$ is an isomorphism of the fiber of $x$ and $x$ and the finite spectrum of $x$.
CommAlgCat.FiniteEtale.finiteSpecdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the finite spectrum of k (from the name)
English
Let $k$ be a set. Then the finite spectrum of $k$ is a functor of the set of opposites of the set of finite etales of $k$ and the set of finite type categories.
CommAlgCat.FiniteEtale.isoMkdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the isomorphism of e (from the name)
English
Let $e$ be an algebra isomorphism of the set of carriers of the object of $S$ and the set of carriers of the object of $T$. Then the isomorphism of $e$ is an isomorphism of $S$ and $T$ defined as the isomorphism of the finite etale of $R$ and the isomorphism of $e$.
CommAlgCat.FiniteEtale.ofdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
no wording
English
Let $R$ and $S$ be sets. Then $\operatorname{of}$ applied to $R$ and $S$ is a finite etale of $R$.
CommAlgCat.FiniteEtale.ofHomdefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the finite etale of f (from the name)
English
Let $f$ be an algebra homomorphism of $S$ and $T$. Then the finite etale of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $S$ and $\operatorname{of}$ applied to $R$ and $T$ defined as $\operatorname{mk}$ applied to the commutative algebra category of $f$.
CommAlgCat.etaledefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the etale of R (from the name)
English
Let $R$ be a set. Then the etale of $R$ is an object property of the set of commutative algebra categories of $R$ defined as the function that maps $S$ to $\operatorname{Etale}$ applied to $R$ and the set of carriers of $S$.
CommAlgCat.finitedefMathlib.RingTheory.Etale.Finite, function or constant
Wording
no wording
English
Let $R$ be a set. Then there is an object property of the set of commutative algebra categories of $R$. Proof. Let $R$ be arbitrary. Let $S$ be arbitrary. By R. By S. By CommAlgCat__carrier. By Module__Finite.
CommAlgCat.finiteEtaledefMathlib.RingTheory.Etale.Finite, function or constant
Wording
the finite etale of R (from the name)
English
Let $R$ be a set. Then the finite etale of $R$ is an object property of the set of commutative algebra categories of $R$ defined as the minimum of $\operatorname{finite}$ applied to $R$ and the etale of $R$.

Mathlib.RingTheory.Etale.Kaehler

Algebra.Extension.tensorCotangentdefMathlib.RingTheory.Etale.Kaehler, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $Q$ such that the algebra map of the set of rings of $P$ and the set of rings of $Q$ is equal to the underlying ring homomorphism of $f$ and $\operatorname{coe}$ applied to the lift base change of the set of rings of $Q$ and the map kernel of $f$ and $\mathrm{halg}$ is bijective. Then $\operatorname{tensorCotangent}$ applied to $f$, $\mathrm{halg}$ and $H$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{Cotangent}$ applied to $P$ and $\operatorname{Cotangent}$ applied to $Q$.
Algebra.Extension.tensorCotangentInvFundefMathlib.RingTheory.Etale.Kaehler, function or constant
Wording
the tensor cotangent inverse function of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$ such that the algebra map of the set of rings of $P$ and the set of rings of $Q$ is equal to the underlying ring homomorphism of $f$ and $\operatorname{coe}$ applied to the lift base change of the set of rings of $Q$ and the map kernel of $f$ and $\mathrm{halg}$ is bijective. Then the tensor cotangent inverse function of $f$ is an additive monoid homomorphism of $\operatorname{Cotangent}$ applied to $Q$ and the set of tensor products of $T$ and $\operatorname{Cotangent}$ applied to $P$.
Algebra.Extension.tensorCotangentSpaceOfFormallyEtaledefMathlib.RingTheory.Etale.Kaehler, function or constant
Wording
the tensor cotangent space of f and H (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$ such that $\operatorname{FormallyEtale}$ holds for the underlying ring homomorphism of $f$. Then the tensor cotangent space of $f$ and $H$ is a linear equivalence of the set of tensor products of $T$ and the set of cotangent spaces of $P$ and the set of cotangent spaces of $Q$.
Algebra.Extension.tensorH1CotangentOfFormallyEtaledefMathlib.RingTheory.Etale.Kaehler, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $Q$ such that the algebra map of the set of rings of $P$ and the set of rings of $Q$ is equal to the underlying ring homomorphism of $f$, $\operatorname{FormallyEtale}$ holds for the underlying ring homomorphism of $f$ and $\operatorname{coe}$ applied to the lift base change of the set of rings of $Q$ and the map kernel of $f$ and $\mathrm{halg}$ is bijective. Then $\operatorname{tensorH1CotangentOfFormallyEtale}$ applied to $f$, $\mathrm{halg}$, $h_{2}$ and $h_{3}$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{H1Cotangent}$ applied to $Q$.
Algebra.tensorH1CotangentOfIsLocalizationdefMathlib.RingTheory.Etale.Kaehler, function or constant
Wording
no wording
English
Let $R$ and $T$ be sets. Let $M$ be a submonoid of $S$. Then $\operatorname{tensorH1CotangentOfIsLocalization}$ applied to $R$, $T$ and $M$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{H1Cotangent}$ applied to $R$ and $S$ and $\operatorname{H1Cotangent}$ applied to $R$ and $T$.
KaehlerDifferential.tensorKaehlerEquivOfFormallyEtaledefMathlib.RingTheory.Etale.Kaehler, function or constant
Wording
no wording
English
Let $R$, $S$ and $T$ be sets. Then $\operatorname{tensorKaehlerEquivOfFormallyEtale}$ applied to $R$, $S$ and $T$ is a linear equivalence of the set of tensor products of $T$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $T$.

Mathlib.RingTheory.Etale.Locus

Algebra.IsEtaleAtdefMathlib.RingTheory.Etale.Locus, predicate
Wording
no wording
English
Let $R$ be a set. Let $q$ be an ideal of $A$. Then $\operatorname{IsEtaleAt}$ holds for $R$ and $q$, if $\operatorname{FormallyEtale}$ holds for $R$ and $\operatorname{AtPrime}$ applied to $q$.
Algebra.etaleLocusdefMathlib.RingTheory.Etale.Locus, function or constant
Wording
the etale locus of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the etale locus of $R$ and $A$ is an element of the power set of the set of prime spectra of $A$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\operatorname{IsEtaleAt}$ applied to $R$ and $\operatorname{asIdeal}$ applied to $p$.

Mathlib.RingTheory.Etale.QuasiFinite

Ideal.fiberIsoOfBijectiveResidueFielddefMathlib.RingTheory.Etale.QuasiFinite, function or constant
Wording
the fiber isomorphism of H (from the name)
English
Assume that $\operatorname{coe}$ applied to the map of $q$ and the algebra of $R$ and $\mathrm{R'}$ is bijective. Then the fiber isomorphism of $H$ is an order isomorphism of the set of elements of $\operatorname{primesOver}$ applied to $q$ and the set of tensor products of $\mathrm{R'}$ and $S$ and the set of elements of $\operatorname{primesOver}$ applied to $p$ and $S$ defined as the composition of the prime over order isomorphism fiber of $q$ and the composition of the preimage equivalence of the ring isomorphism of the composition of $\operatorname{restrictScalars}$ applied to the set of residue fields of $p$ and $\operatorname{cancelBaseChange}$ applied to $R$, $\mathrm{R'}$, the set of residue fields of $q$, the set of residue fields of $q$ and $S$ and the congruence of the inverse of the algebra isomorphism of the algebra of the set of residue fields of $p$ and the set of residue fields of $q$ and $H$ and the identity and the inverse of the prime over order isomorphism fiber of $p$.

Mathlib.RingTheory.Etale.StandardEtale

Algebra.IsStandardEtaleclassMathlib.RingTheory.Etale.StandardEtale, predicate
Wording
no wording
English
Let $R$ and $S$ be sets. Then we can say that $\operatorname{IsStandardEtale}$ holds for $R$ and $S$.
StandardEtalePairstructureMathlib.RingTheory.Etale.StandardEtale, type
Wording
standard etale pair of R (from the name)
English
Let $R$ be a set. Then the standard etale pairs of $R$ are a basic type.
StandardEtalePair.HasMapdefMathlib.RingTheory.Etale.StandardEtale, predicate
Wording
no wording
English
Let $P$ be a standard etale pair of $R$. Let $x_{3}$ be an element of $S$. Then $\operatorname{HasMap}$ holds for $P$ and $x_{3}$, if $\EqtMACRoH {\operatorname{aeval} (x_{3} , \operatorname{f} (P))}{0}$ and $\operatorname{aeval}$ applied to $x_{3}$ and $\operatorname{g}$ applied to $P$ is a unit.
StandardEtalePair.RingdefMathlib.RingTheory.Etale.StandardEtale, type
Wording
ring of P (from the name)
English
Let $P$ be a standard etale pair of $R$. Then a ring of $P$ is an element of the function that maps $P$ to the set of quotients of the set of polynomials of the set of polynomials of $R$ and the span of $\operatorname{insert}$ applied to $\operatorname{C}$ applied to $\operatorname{f}$ applied to $P$ and $\operatorname{singleton}$ applied to $\operatorname{X} \times \operatorname{C} (\operatorname{g} (P))- 1$.
StandardEtalePair.XdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
no wording
English
Let $P$ be a standard etale pair of $R$. Then $\operatorname{X}$ applied to $P$ is a ring of $P$ defined as $\operatorname{mk}$ applied to the span of $\operatorname{insert}$ applied to $\operatorname{C}$ applied to $\operatorname{f}$ applied to $P$ and $\operatorname{singleton}$ applied to $\operatorname{X} \times \operatorname{C} (\operatorname{g} (P))- 1$ and $\operatorname{C}$ applied to $\operatorname{X}$.
StandardEtalePair.equivAwayAdjoinRootdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
no wording
English
Let $P$ be a standard etale pair of $R$. Then $\operatorname{equivAwayAdjoinRoot}$ applied to $P$ is an algebra isomorphism of the set of rings of $P$ and $\operatorname{Away}$ applied to $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $P$ and $\operatorname{g}$ applied to $P$.
StandardEtalePair.equivAwayQuotientdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
no wording
English
Let $P$ be a standard etale pair of $R$. Then $\operatorname{equivAwayQuotient}$ applied to $P$ is an algebra isomorphism of the set of rings of $P$ and the set of quotients of $\operatorname{Away}$ applied to $\operatorname{g}$ applied to $P$ and the span of $\operatorname{singleton}$ applied to $\operatorname{algebraMap}$ applied to the set of polynomials of $R$, $\operatorname{Away}$ applied to $\operatorname{g}$ applied to $P$ and $\operatorname{f}$ applied to $P$.
StandardEtalePair.equivMvPolynomialQuotientdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the equivalence multivariate polynomial quotient of P (from the name)
English
Let $P$ be a standard etale pair of $R$. Then the equivalence multivariate polynomial quotient of $P$ is an algebra isomorphism of the set of rings of $P$ and the set of quotients of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $2$ and $R$ and the span of $\operatorname{insert}$ applied to $\operatorname{equivMvPolynomial}$ applied to $R$ and $\operatorname{C}$ applied to $\operatorname{f}$ applied to $P$ and $\operatorname{singleton}$ applied to $\operatorname{equivMvPolynomial}$ applied to $R$ and $\operatorname{X} \times \operatorname{C} (\operatorname{g} (P))- 1$.
StandardEtalePair.equivPolynomialQuotientdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the equivalence polynomial quotient of P (from the name)
English
Let $P$ be a standard etale pair of $R$. Then the equivalence polynomial quotient of $P$ is an algebra isomorphism of the set of rings of $P$ and the set of quotients of the set of polynomials of the set of polynomials of $R$ and the span of $\operatorname{insert}$ applied to $\operatorname{C}$ applied to $\operatorname{f}$ applied to $P$ and $\operatorname{singleton}$ applied to $\operatorname{X} \times \operatorname{C} (\operatorname{g} (P))- 1$ defined as the identity.
StandardEtalePair.fdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a standard etale pair of $R$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a polynomial of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
StandardEtalePair.gdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a standard etale pair of $R$. Then $\operatorname{g}$ applied to $\mathrm{self}$ is a polynomial of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
StandardEtalePair.homEquivdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the homomorphism equivalence of P (from the name)
English
Let $P$ be a standard etale pair of $R$. Then the homomorphism equivalence of $P$ is an equivalence from the set of algebra homomorphisms of the set of rings of $P$ and $S$ to $\SubtypeSet {x_{3}}{\operatorname{HasMap} (P , x_{3})}$.
StandardEtalePair.liftdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the lift of P and x3 (from the name)
English
Let $P$ be a standard etale pair of $R$. Let $x_{3}$ be an element of $S$ such that $\operatorname{HasMap}$ holds for $P$ and $x_{3}$. Then the lift of $P$ and $x_{3}$ is an algebra homomorphism of the set of rings of $P$ and $S$.
StandardEtalePair.mapdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the map of P and f (from the name)
English
Let $P$ be a standard etale pair of $R$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $P$ and $f$ is a standard etale pair of $S$.
StandardEtalePresentationstructureMathlib.RingTheory.Etale.StandardEtale, type
Wording
standard etale presentation of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the standard etale presentations of $R$ and $S$ are a basic type.
StandardEtalePresentation.baseChangedefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the base change of P (from the docstring)
English
Let $P$ be a standard etale presentation of $R$ and $S$. Then the base change of $P$ is a standard etale presentation of $T$ and the set of tensor products of $T$ and $S$.
StandardEtalePresentation.equivRingdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the equivalence ring of P (from the name)
English
Let $P$ be a standard etale presentation of $R$ and $S$. Then the equivalence ring of $P$ is an algebra isomorphism of $S$ and the set of rings of $\operatorname{P}$ applied to $P$ defined as the inverse of the algebra isomorphism of the lift of $\operatorname{P}$ applied to $P$ and $\operatorname{x}$ applied to $P$ and $\mathrm{StandardEtalePresentation\_\_lift\_bijective}$ applied to $P$.
StandardEtalePresentation.mapEquivdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the map equivalence of P and e (from the name)
English
Let $P$ be a standard etale presentation of $R$ and $S$. Let $e$ be an algebra isomorphism of $S$ and $T$. Then the map equivalence of $P$ and $e$ is a standard etale presentation of $R$ and $T$.
StandardEtalePresentation.toPresentationdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the presentation of P (from the name)
English
Let $P$ be a standard etale presentation of $R$ and $S$. Then the presentation of $P$ is a presentation of $\mathrm{Fin}$ applied to $2$ and $\mathrm{Fin}$ applied to $2$.
StandardEtalePresentation.toSubmersivePresentationdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
the submersive presentation of P (from the name)
English
Let $P$ be a standard etale presentation of $R$ and $S$. Then the submersive presentation of $P$ is a submersive presentation of $\mathrm{Fin}$ applied to $2$ and $\mathrm{Fin}$ applied to $2$.
StandardEtalePresentation.xdefMathlib.RingTheory.Etale.StandardEtale, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a standard etale presentation of $R$ and $S$. Then $\operatorname{x}$ applied to $\mathrm{self}$ is an element of $S$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.RingTheory.Etale.Weakly

Algebra.WeaklyEtaleclassMathlib.RingTheory.Etale.Weakly, predicate
Wording
no wording
English
Let $R$ and $S$ be sets. Then we can say that $\operatorname{WeaklyEtale}$ holds for $R$ and $S$.

Mathlib.RingTheory.Extension.Basic

Algebra.ExtensionstructureMathlib.RingTheory.Extension.Basic, type
Wording
extension of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the extensions of $R$ and $S$ are a basic type.
Algebra.Extension.CotangentdefMathlib.RingTheory.Extension.Basic, type
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then an element of $\operatorname{Cotangent}$ applied to $P$ is an element of the function that maps $P$ to $\operatorname{Cotangent}$ applied to the kernel of $P$.
Algebra.Extension.Cotangent.mapdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the map of $f$ is a linear map of $\operatorname{Cotangent}$ applied to $P$ and $\operatorname{Cotangent}$ applied to $\mathrm{P'}$.
Algebra.Extension.Cotangent.mkdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
no wording
English
$\operatorname{mk}$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (P)}{x_{3}})}$ and $\operatorname{Cotangent}$ applied to $P$.
Algebra.Extension.Cotangent.ofdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
no wording
English
Let $x_{3}$ be an element of $\operatorname{Cotangent}$ applied to the kernel of $P$. Then $\operatorname{of}$ applied to $x_{3}$ is an element of $\operatorname{Cotangent}$ applied to $P$ defined as $x_{3}$.
Algebra.Extension.Cotangent.valdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the value of x3 (from the name)
English
Let $x_{3}$ be an element of $\operatorname{Cotangent}$ applied to $P$. Then the value of $x_{3}$ is an element of $\operatorname{Cotangent}$ applied to the kernel of $P$ defined as $x_{3}$.
Algebra.Extension.HomstructureMathlib.RingTheory.Extension.Basic, type
Wording
homomorphism of P and #2 (from the name)
English
Let $P$ be an extension of $R$ and $S$. Let $\mathrm{P'}$ be an extension of $\mathrm{R'}$ and $\mathrm{S'}$. Then the homomorphisms of $P$ and $\mathrm{P'}$ are a basic type.
Algebra.Extension.Hom.compdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a homomorphism of $\mathrm{P'}$ and $\mathrm{P''}$. Let $g$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the composition of $f$ and $g$ is a homomorphism of $P$ and $\mathrm{P''}$.
Algebra.Extension.Hom.iddefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the identity hom of P (from the docstring)
English
Let $P$ be an extension of $R$ and $S$. Then the identity hom of $P$ is a homomorphism of $P$ and $P$.
Algebra.Extension.Hom.mapKerdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the map kernel of f and halg (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$ such that $\EqtMACRoH {\operatorname{algebraMap} (\operatorname{Ring} (P), \operatorname{Ring} (\mathrm{P'}))}{\operatorname{toRingHom} (f)}$. Then the map kernel of $f$ and $\mathrm{halg}$ is a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{ker} (P)}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{ker} (\mathrm{P'})}{x_{9}})}$.
Algebra.Extension.Hom.ofAlgHomdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the homomorphism of f and H (from the name)
English
Let $f$ be an algebra homomorphism of the set of rings of $P$ and the set of rings of $\mathrm{P'}$ such that the composition of the algebra homomorphism of the set of rings of $\mathrm{P'}$ and $\mathrm{S'}$ and $f$ is equal to the composition of the algebra homomorphism of $S$ and $\mathrm{S'}$ and the algebra homomorphism of the set of rings of $P$ and $S$. Then the homomorphism of $f$ and $H$ is a homomorphism of $P$ and $\mathrm{P'}$.
Algebra.Extension.Hom.toAlgHomdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the algebra homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the algebra homomorphism of $f$ is an algebra homomorphism of the set of rings of $P$ and the set of rings of $\mathrm{P'}$.
Algebra.Extension.Hom.toRingHomdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the underlying ring homomorphism of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the underlying ring homomorphism of $\mathrm{self}$ is a ring homomorphism of the set of rings of $P$ and the set of rings of $\mathrm{P'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Algebra.Extension.RingdefMathlib.RingTheory.Extension.Basic, type
Wording
ring of self (from the name)
English
Let $\mathrm{self}$ be an extension of $R$ and $S$. Then a ring of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
Algebra.Extension.baseChangedefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the base change of P (from the docstring)
English
Let $P$ be an extension of $R$ and $S$. Then the base change of $P$ is an extension of $T$ and the set of tensor products of $T$ and $S$.
Algebra.Extension.cotangentEquivdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the cotangent equivalence of P (from the name)
English
Let $P$ be an extension of $R$ and $S$. Then the cotangent equivalence of $P$ is a linear equivalence of the set of tensor products of $S$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (P)}{x_{3}})}$ and $\operatorname{Cotangent}$ applied to $P$.
Algebra.Extension.cotangentEquivCotangentKerdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the cotangent equivalence cotangent kernel (from the name)
English
The cotangent equivalence cotangent kernel is a linear equivalence of $\operatorname{Cotangent}$ applied to $P$ and $\operatorname{Cotangent}$ applied to the kernel of $P$.
Algebra.Extension.infinitesimaldefMathlib.RingTheory.Extension.Basic, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{infinitesimal}$ applied to $P$ is an extension of $R$ and $S$.
Algebra.Extension.kerdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the kernel of P (from the docstring)
English
Let $P$ be an extension of $R$ and $S$. Then the kernel of $P$ is an ideal of the set of rings of $P$ defined as the kernel of the algebra map of the set of rings of $P$ and $S$.
Algebra.Extension.localizationdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the localization of M and P (from the name)
English
Let $M$ be a submonoid of $S$. Let $P$ be an extension of $R$ and $S$. Then the localization of $M$ and $P$ is an extension of $R$ and $\mathrm{S'}$.
Algebra.Extension.ofSurjectivedefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the extension of f and h (from the name)
English
Let $f$ be an algebra homomorphism of $P$ and $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the extension of $f$ and $h$ is an extension of $R$ and $S$.
Algebra.Extension.selfdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the self of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the self of $R$ and $S$ is an extension of $R$ and $S$.
Algebra.Extension.toBaseChangedefMathlib.RingTheory.Extension.Basic, function or constant
Wording
the base change of T (from the name)
English
Let $T$ be a set. Then the base change of $T$ is a homomorphism of $P$ and the base change of $P$.
Algebra.Extension.toInfinitesimaldefMathlib.RingTheory.Extension.Basic, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{toInfinitesimal}$ applied to $P$ is a homomorphism of $P$ and $\operatorname{infinitesimal}$ applied to $P$.
Algebra.Extension.σdefMathlib.RingTheory.Extension.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an extension of $R$ and $S$. Let $x_{3}$ be an element of $S$. Then $\mathrm{Algebra\_\_Extension\_\_\_u3c3\_}$ applied to $\mathrm{self}$ and $x_{3}$ is a ring of $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $x_{3}$.

Mathlib.RingTheory.Extension.Cotangent.BaseChange

Algebra.Extension.tensorCotangentOfFlatdefMathlib.RingTheory.Extension.Cotangent.BaseChange, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Let $T$ be a set. Then $\operatorname{tensorCotangentOfFlat}$ applied to $P$ and $T$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{Cotangent}$ applied to $P$ and $\operatorname{Cotangent}$ applied to the base change of $P$.
Algebra.Extension.tensorCotangentSpacedefMathlib.RingTheory.Extension.Cotangent.BaseChange, function or constant
Wording
the cotangent space of P and T (from the docstring)
English
Let $P$ be an extension of $R$ and $S$. Let $T$ be a set. Then the cotangent space of $P$ and $T$ is a linear equivalence of the set of tensor products of $T$ and the set of cotangent spaces of $P$ and the set of cotangent spaces of the base change of $P$.
Algebra.Extension.tensorH1CotangentOfFlatdefMathlib.RingTheory.Extension.Cotangent.BaseChange, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Let $T$ be a set. Then $\operatorname{tensorH1CotangentOfFlat}$ applied to $P$ and $T$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{H1Cotangent}$ applied to the base change of $P$ defined as the linear equivalence of $\operatorname{tensorToH1Cotangent}$ applied to $P$ and $T$ and $\mathrm{Algebra\_\_Extension\_\_tensorToH1Cotangent\_bijective\_of\_flat}$ applied to $P$ and $T$.
Algebra.Extension.tensorToH1CotangentdefMathlib.RingTheory.Extension.Cotangent.BaseChange, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Let $T$ be a set. Then $\operatorname{tensorToH1Cotangent}$ applied to $P$ and $T$ is a linear map of the set of tensor products of $T$ and $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{H1Cotangent}$ applied to the base change of $P$ defined as the lift base change of $T$ and $\operatorname{restrictScalars}$ applied to $R$ and the map of the base change of $T$.
Algebra.tensorH1CotangentOfFlatdefMathlib.RingTheory.Extension.Cotangent.BaseChange, function or constant
Wording
no wording
English
Let $R$, $S$ and $T$ be sets. Then $\operatorname{tensorH1CotangentOfFlat}$ applied to $R$, $S$ and $T$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{H1Cotangent}$ applied to $R$ and $S$ and $\operatorname{H1Cotangent}$ applied to $T$ and the set of tensor products of $T$ and $S$ defined as the composition of the composition of $\operatorname{tensorH1CotangentOfFlat}$ applied to the extension of the self of $R$ and $S$ and $T$ and $\operatorname{restrictScalars}$ applied to $T$ and the equivalence of the base change from base change of the self of $R$ and $S$ and $T$ and the base change to base change of the self of $R$ and $S$ and $T$ and $\operatorname{restrictScalars}$ applied to $T$ and $\operatorname{equivH1Cotangent}$ applied to the base change of $T$ and the self of $R$ and $S$.

Mathlib.RingTheory.Extension.Cotangent.Basic

Algebra.Extension.CotangentSpacedefMathlib.RingTheory.Extension.Cotangent.Basic, type
Wording
cotangent space of P (from the name)
English
Let $P$ be an extension of $R$ and $S$. Then a cotangent space of $P$ is an element of the function that maps $P$ to the set of tensor products of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and the set of rings of $P$.
Algebra.Extension.CotangentSpace.mapdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the map of $f$ is a linear map of the set of cotangent spaces of $P$ and the set of cotangent spaces of $\mathrm{P'}$ defined as the lift base change of $S$ and the composition of $\operatorname{restrictScalars}$ applied to the set of rings of $P$ and $\operatorname{mk}$ applied to the set of rings of $\mathrm{P'}$, $\mathrm{S'}$, $\mathrm{KaehlerDifferential}$ applied to $\mathrm{R'}$ and the set of rings of $\mathrm{P'}$ and $1$ and the map of the set of rings of $P$ and the set of rings of $\mathrm{P'}$.
Algebra.Extension.H1CotangentdefMathlib.RingTheory.Extension.Cotangent.Basic, type
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then an element of $\operatorname{H1Cotangent}$ applied to $P$ is an element of the function that maps $P$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{cotangentComplex} (P))}{x_{3}})}$.
Algebra.Extension.H1Cotangent.equivdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the equivalence of x5 and x6 (from the name)
English
Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{3}$. Then the equivalence of $x_{5}$ and $x_{6}$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to $x_{3}$ and $\operatorname{H1Cotangent}$ applied to $x_{4}$.
Algebra.Extension.H1Cotangent.mapdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the map of $f$ is a linear map of $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{H1Cotangent}$ applied to $\mathrm{P'}$.
Algebra.Extension.Hom.subdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the difference of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $P$ and $\mathrm{P'}$. Then the difference of $f$ and $g$ is a linear map of the set of cotangent spaces of $P$ and $\operatorname{Cotangent}$ applied to $\mathrm{P'}$.
Algebra.Extension.Hom.subToKerdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the difference to kernel of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $P$ and $\mathrm{P'}$. Then the difference to kernel of $f$ and $g$ is a linear map of the set of rings of $P$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{ker} (\mathrm{P'})}{x_{9}})}$.
Algebra.Extension.cotangentComplexdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the cotangent complex of P (from the name)
English
Let $P$ be an extension of $R$ and $S$. Then the cotangent complex of $P$ is a linear map of $\operatorname{Cotangent}$ applied to $P$ and the set of cotangent spaces of $P$.
Algebra.Extension.h1CotangentιdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the cotangent inclusion (from the name)
English
The cotangent inclusion is a linear map of $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{Cotangent}$ applied to $P$ defined as the subtype of the kernel of the cotangent complex of $P$.
Algebra.Extension.toKaehlerdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{toKaehler}$ applied to $P$ is a linear map of the set of cotangent spaces of $P$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ defined as the map base change of the set of rings of $P$ and $S$.
Algebra.Generators.H1Cotangent.equivdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the equivalence of P and #2 (from the name)
English
Let $P$ be a generator of $S$ and $x_{3}$. Let $\mathrm{P'}$ be a generator of $S$ and $x_{4}$. Then the equivalence of $P$ and $\mathrm{P'}$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to the extension of $P$ and $\operatorname{H1Cotangent}$ applied to the extension of $\mathrm{P'}$ defined as the equivalence of the extension homomorphism of the default homomorphism of $P$ and $\mathrm{P'}$ and the extension homomorphism of the default homomorphism of $\mathrm{P'}$ and $P$.
Algebra.Generators.cotangentRestrictdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
no wording
English
Let $P$ be a generator of $S$ and $x_{3}$. Assume that $u$ is injective. Then $\operatorname{cotangentRestrict}$ applied to $P$ and $\mathrm{hu}$ is a linear map of $\operatorname{Cotangent}$ applied to the extension of $P$ and $\FinsuppMACRoQ {x_{4}}{S}$ defined as the composition of $\operatorname{lcomapDomain}$ applied to $u$ and $\mathrm{hu}$ and the composition of $\operatorname{toLinearMap}$ applied to the representation of the cotangent space basis of $P$ and the cotangent complex of the extension of $P$.
Algebra.Generators.cotangentSpaceBasisdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the cotangent space basis of P (from the name)
English
Let $P$ be a generator of $S$ and $x_{3}$. Then the cotangent space basis of $P$ is a basis of $S$ and the set of cotangent spaces of the extension of $P$ defined as the base change of $S$ and the multivariate polynomial basis of $R$ and $x_{3}$.
Algebra.Generators.equivH1CotangentdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
no wording
English
Let $P$ be a generator of $S$ and $x_{3}$. Then $\operatorname{equivH1Cotangent}$ applied to $P$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to the extension of $P$ and $\operatorname{H1Cotangent}$ applied to $R$ and $S$ defined as the equivalence of $P$ and the self of $R$ and $S$.
Algebra.H1CotangentdefMathlib.RingTheory.Extension.Cotangent.Basic, type
Wording
no wording
English
Let $R$ and $S$ be sets. Then an element of $\operatorname{H1Cotangent}$ applied to $R$ and $S$ is an element of the function that maps $R$ and $S$ to $\operatorname{H1Cotangent}$ applied to the extension of the self of $R$ and $S$.
Algebra.H1Cotangent.mapdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the map of T and #4 (from the name)
English
Let $R$, $S$, $\mathrm{S'}$ and $T$ be sets. Then the map of $\mathrm{S'}$ and $T$ is a linear map of $\operatorname{H1Cotangent}$ applied to $R$ and $\mathrm{S'}$ and $\operatorname{H1Cotangent}$ applied to $S$ and $T$ defined as the map of the extension homomorphism of the default homomorphism of the self of $R$ and $\mathrm{S'}$ and the self of $S$ and $T$.
Algebra.H1Cotangent.mapEquivdefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the map equivalence of #4 (from the name)
English
Let $R$, $S$ and $\mathrm{S'}$ be sets. Let $e$ be an algebra isomorphism of $S$ and $\mathrm{S'}$. Then the map equivalence of $e$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to $R$ and $S$ and $\operatorname{H1Cotangent}$ applied to $R$ and $\mathrm{S'}$.
KaehlerDifferential.cotangentComplexBaseChangedefMathlib.RingTheory.Extension.Cotangent.Basic, function or constant
Wording
the cotangent complex base change of P and A (from the name)
English
Let $R$, $S$, $P$ and $A$ be sets. Then the cotangent complex base change of $P$ and $A$ is a linear map of the set of tensor products of $A$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{algebraMap} (P , S))}{x_{8}})}$ and the set of tensor products of $A$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $P$.

Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Algebra.Generators.compLocalizationAwayAlgHomdefMathlib.RingTheory.Extension.Cotangent.LocalizationAway, function or constant
Wording
no wording
English
Let $T$ be a set. Let $g$ be an element of $S$. Let $P$ be a generator of $S$ and $x$. Then $\operatorname{compLocalizationAwayAlgHom}$ applied to $T$, $g$ and $P$ is an algebra homomorphism of the set of rings of the composition of $\operatorname{localizationAway}$ applied to $T$ and $g$ and $P$ and $\operatorname{Away}$ applied to $\operatorname{mk}$ applied to the exponentiation of the kernel of $P$ to $2$ and $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_}$ applied to $P$ and $g$ defined as the algebra evaluation of $\operatorname{elim}$ applied to the function that maps $x_{7}$ to the inverse self of $\operatorname{mk}$ applied to the exponentiation of the kernel of $P$ to $2$ and $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_}$ applied to $P$ and $g$ and the function that maps $i$ to $\operatorname{algebraMap}$ applied to the set of rings of $P$, $\operatorname{Away}$ applied to $\operatorname{mk}$ applied to the exponentiation of the kernel of $P$ to $2$ and $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_}$ applied to $P$ and $g$ and $\operatorname{X}$ applied to $i$.
Algebra.Generators.cotangentCompAwaySecdefMathlib.RingTheory.Extension.Cotangent.LocalizationAway, function or constant
Wording
no wording
English
Let $g$ be an element of $S$. Let $P$ be a generator of $S$ and $x$. Let $x_{7}$ be an element of $\operatorname{Cotangent}$ applied to the extension of the composition of $\operatorname{localizationAway}$ applied to $T$ and $g$ and $P$. Then $\operatorname{cotangentCompAwaySec}$ applied to $g$, $P$ and $x_{7}$ is a linear map of $\operatorname{Cotangent}$ applied to the extension of $\operatorname{localizationAway}$ applied to $T$ and $g$ and $\operatorname{Cotangent}$ applied to the extension of the composition of $\operatorname{localizationAway}$ applied to $T$ and $g$ and $P$ defined as $\operatorname{constr}$ applied to $\operatorname{basisCotangentAway}$ applied to $T$ and $g$, $T$ and the function that maps $x_{9}$ to $x_{7}$.
Algebra.Generators.cotangentCompLocalizationAwayEquivdefMathlib.RingTheory.Extension.Cotangent.LocalizationAway, function or constant
Wording
no wording
English
Let $g$ be an element of $S$. Let $P$ be a generator of $S$ and $x$ such that $\operatorname{map}$ applied to the extension homomorphism of the generator of $\operatorname{localizationAway}$ applied to $T$ and $g$ and $P$ and $x_{7}$ is equal to $\operatorname{cMulXSubOneCotangent}$ applied to $T$ and $g$. Then $\operatorname{cotangentCompLocalizationAwayEquiv}$ applied to $g$, $P$ and $\mathrm{hx}$ is a linear equivalence of $\operatorname{Cotangent}$ applied to the extension of the composition of $\operatorname{localizationAway}$ applied to $T$ and $g$ and $P$ and $\mathrm{Prod}$ applied to the set of tensor products of $T$ and $\operatorname{Cotangent}$ applied to the extension of $P$ and $\operatorname{Cotangent}$ applied to the extension of $\operatorname{localizationAway}$ applied to $T$ and $g$.

Mathlib.RingTheory.Extension.ExtendScalars

Algebra.Extension.cotangentExtendScalarsEquivdefMathlib.RingTheory.Extension.ExtendScalars, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{cotangentExtendScalarsEquiv}$ applied to $P$ is a linear equivalence of $\operatorname{Cotangent}$ applied to $\operatorname{extendScalars}$ applied to $P$ and $\operatorname{Cotangent}$ applied to $P$ defined as the identity map of $S$ and $\operatorname{Cotangent}$ applied to $\operatorname{extendScalars}$ applied to $P$.
Algebra.Extension.extendScalarsdefMathlib.RingTheory.Extension.ExtendScalars, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{extendScalars}$ applied to $P$ is an extension of the set of rings of $P$ and $S$ defined as $\operatorname{mk}$ applied to the set of rings of $P$, $\mathrm{Algebra\_\_Extension\_\_\_u3c3\_}$ applied to $P$ and $\mathrm{Algebra\_\_Extension\_\_algebraMap\_\_u3c3\_}$ applied to $P$.
Algebra.Extension.h1CotangentEquivCotangentdefMathlib.RingTheory.Extension.ExtendScalars, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{h1CotangentEquivCotangent}$ applied to $P$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to the set of rings of $P$ and $S$ and $\operatorname{Cotangent}$ applied to $P$.
Algebra.Extension.h1CotangentEquivOfSurjectivedefMathlib.RingTheory.Extension.ExtendScalars, function or constant
Wording
the cotangent equivalence of P and h (from the name)
English
Let $P$ be an extension of $R$ and $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and the set of rings of $P$. Then the cotangent equivalence of $P$ and $h$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{Cotangent}$ applied to $P$.
Algebra.Extension.h1CotangentExtendScalarsEquivdefMathlib.RingTheory.Extension.ExtendScalars, function or constant
Wording
the first homology of the naive cotangent complex of P (from the docstring)
English
Let $P$ be an extension of $R$ and $S$. Then the first homology of the naive cotangent complex of $P$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to $\operatorname{extendScalars}$ applied to $P$ and $\operatorname{H1Cotangent}$ applied to the set of rings of $P$ and $S$.
Algebra.Extension.toExtendScalarsdefMathlib.RingTheory.Extension.ExtendScalars, function or constant
Wording
no wording
English
Let $P$ be an extension of $R$ and $S$. Then $\operatorname{toExtendScalars}$ applied to $P$ is a homomorphism of $P$ and $\operatorname{extendScalars}$ applied to $P$.

Mathlib.RingTheory.Extension.Generators

Algebra.Extension.defaultHomdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the default homomorphism of P (from the name)
English
Let $R$ and $S$ be sets. Let $P$ be an extension of $R$ and $S$. Then the default homomorphism of $P$ is a homomorphism of the extension of the self of $R$ and $S$ and $P$.
Algebra.GeneratorsstructureMathlib.RingTheory.Extension.Generators, type
Wording
generator of S and x (from the name)
English
Let $R$, $S$ and $x$ be sets. Then the generators of $S$ and $x$ are a basic type.
Algebra.Generators.HomstructureMathlib.RingTheory.Extension.Generators, type
Wording
homomorphism of P and #2 (from the name)
English
Let $P$ be a generator of $S$ and $x$. Let $\mathrm{P'}$ be a generator of $\mathrm{S'}$ and $x_{4}$. Then the homomorphisms of $P$ and $\mathrm{P'}$ are a basic type.
Algebra.Generators.Hom.compdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a homomorphism of $\mathrm{P'}$ and $\mathrm{P''}$. Let $g$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the composition of $f$ and $g$ is a homomorphism of $P$ and $\mathrm{P''}$.
Algebra.Generators.Hom.equivAlgHomdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the equivalence algebra homomorphism (from the name)
English
The equivalence algebra homomorphism is an element of $\EquivMACRoAE {\operatorname{Hom} (P , \mathrm{P'})}{(\SubtypeSet {f}{\mathrm{forall} (\operatorname{Ring} (P), \lambda x_{11} . \EqtMACRoH {\operatorname{aeval} (\operatorname{val} (\mathrm{P'}), f (x_{11}))}{\operatorname{algebraMap} (S , \mathrm{S'} , \operatorname{aeval} (\operatorname{val} (P), x_{11}))})})}$.
Algebra.Generators.Hom.iddefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the identity hom of P (from the docstring)
English
Let $P$ be a generator of $S$ and $x$. Then the identity hom of $P$ is a homomorphism of $P$ and $P$.
Algebra.Generators.Hom.toAlgHomdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the algebra homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the algebra homomorphism of $f$ is an algebra homomorphism of the set of rings of $P$ and the set of rings of $\mathrm{P'}$ defined as the algebra evaluation of $\operatorname{val}$ applied to $f$.
Algebra.Generators.Hom.toExtensionHomdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the extension homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Then the extension homomorphism of $f$ is a homomorphism of the extension of $P$ and the extension of $\mathrm{P'}$.
Algebra.Generators.Hom.valdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the value of self and x9 (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $P$ and $\mathrm{P'}$. Let $x_{9}$ be an element of $x$. Then the value of $\mathrm{self}$ and $x_{9}$ is a ring of $\mathrm{P'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{9}$.
Algebra.Generators.RingdefMathlib.RingTheory.Extension.Generators, type
Wording
ring of P (from the name)
English
Let $P$ be a generator of $S$ and $x$. Then a ring of $P$ is an element of the function that maps $P$ to the set of multivariate polynomials of $x$ and $R$.
Algebra.Generators.baseChangedefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the base change of T and P (from the name)
English
Let $T$ be a set. Let $P$ be a generator of $S$ and $x$. Then the base change of $T$ and $P$ is a generator of the set of tensor products of $T$ and $S$ and $x$.
Algebra.Generators.baseChangeFromBaseChangedefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the base change from base change of P and T (from the name)
English
Let $P$ be a generator of $S$ and $x$. Let $T$ be a set. Then the base change from base change of $P$ and $T$ is a homomorphism of the base change of the extension of $P$ and the extension of the base change of $T$ and $P$.
Algebra.Generators.baseChangeToBaseChangedefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the base change to base change of P and T (from the name)
English
Let $P$ be a generator of $S$ and $x$. Let $T$ be a set. Then the base change to base change of $P$ and $T$ is a homomorphism of the extension of the base change of $T$ and $P$ and the base change of the extension of $P$.
Algebra.Generators.compdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the composition of Q and P (from the name)
English
Let $Q$ be a generator of $T$ and $x_{4}$. Let $P$ be a generator of $S$ and $x$. Then the composition of $Q$ and $P$ is a generator of $T$ and $\mathrm{Sum}$ applied to $x_{4}$ and $x$.
Algebra.Generators.defaultHomdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the default homomorphism of P and #2 (from the name)
English
Let $P$ be a generator of $S$ and $x$. Let $\mathrm{P'}$ be a generator of $\mathrm{S'}$ and $x_{4}$. Then the default homomorphism of $P$ and $\mathrm{P'}$ is a homomorphism of $P$ and $\mathrm{P'}$.
Algebra.Generators.extenddefMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $P$ be a generator of $S$ and $x$. Let $b$ be a function from elements of $x_{4}$ to elements of $S$. Then $\operatorname{extend}$ applied to $P$ and $b$ is a generator of $S$ and $\mathrm{Sum}$ applied to $x$ and $x_{4}$.
Algebra.Generators.extendScalarsdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $S$ be a set. Let $P$ be a generator of $T$ and $x$. Then $\operatorname{extendScalars}$ applied to $S$ and $P$ is a generator of $T$ and $x$.
Algebra.Generators.iddefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the identity (from the name)
English
The identity is a generator of $R$ and $\mathrm{PEmpty}$.
Algebra.Generators.kerdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the kernel of P (from the docstring)
English
Let $P$ be a generator of $S$ and $x$. Then the kernel of $P$ is an ideal of the set of rings of $P$ defined as the kernel of the extension of $P$.
Algebra.Generators.kerCompPreimagedefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the kernel composition preimage of P and x8 (from the name)
English
Let $Q$ be a generator of $T$ and $x_{4}$. Let $P$ be a generator of $S$ and $x$. Let $x_{8}$ be an element of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (Q)}{x_{10}})}$. Then the kernel composition preimage of $P$ and $x_{8}$ is an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{comp} (Q , P))}{x_{9}})}$ defined as the sum of the coefficient of $x_{8}$ and the function that maps $n$ and $r$ to $\operatorname{rename} (\operatorname{inr} , \mathrm{Algebra\_\_Generators\_\_\_u3c3\_} (P , r))\times \operatorname{monomial} (\operatorname{mapDomain} (\operatorname{inl} , n), 1)$.
Algebra.Generators.localizationAwaydefMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $S$ be a set. Let $r$ be an element of $R$. Then $\operatorname{localizationAway}$ applied to $S$ and $r$ is a generator of $S$ and $\mathrm{Unit}$.
Algebra.Generators.mvPolynomialdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the multivariate polynomial of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the multivariate polynomial of $R$ and $x$ is a generator of the set of multivariate polynomials of $x$ and $R$ and $x$.
Algebra.Generators.naivedefMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $s$ be an element of $\mathrm{optParam}$ applied to the set of functions from quotients of the set of multivariate polynomials of $x_{1}$ and $R$ and $I$ to multivariate polynomials of $x_{1}$ and $R$ and $\operatorname{surjInv}$ applied to $\mathrm{Ideal\_\_Quotient\_\_mk\_surjective}$ such that $\mathrm{autoParam}$ holds for the proposition that for all quotients $x_{2}$ of the set of multivariate polynomials of $x_{1}$ and $R$ and $I$, $\EqtMACRoH {\operatorname{mk} (I , s (x_{2}))}{x_{2}}$ and $\mathrm{Algebra\_\_Generators\_\_naive\_\_\_auto\_1}$. Then $\operatorname{naive}$ applied to $s$ and $\mathrm{hs}$ is a generator of the set of quotients of the set of multivariate polynomials of $x_{1}$ and $R$ and $I$ and $x_{1}$.
Algebra.Generators.ofAlgEquivdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the generator of P and e (from the name)
English
Let $P$ be a generator of $S$ and $x$. Let $e$ be an algebra isomorphism of $S$ and $T$. Then the generator of $P$ and $e$ is a generator of $T$ and $x$.
Algebra.Generators.ofAlgHomdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the generator of f and h (from the name)
English
Let $f$ be an algebra homomorphism of the set of multivariate polynomials of $I$ and $R$ and $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the generator of $f$ and $h$ is a generator of $S$ and $I$.
Algebra.Generators.ofCompdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the generator of Q and P (from the name)
English
Let $Q$ be a generator of $T$ and $x_{4}$. Let $P$ be a generator of $S$ and $x$. Then the generator of $Q$ and $P$ is a homomorphism of the composition of $Q$ and $P$ and $Q$.
Algebra.Generators.ofSetdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the generator of hs (from the name)
English
Assume that $\operatorname{adjoin}$ applied to $R$ and $s$ is equal to the top. Then the generator of $\mathrm{hs}$ is a generator of $S$ and the set of elements of $s$.
Algebra.Generators.ofSurjectivedefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the generator of val and h (from the name)
English
Let $\mathrm{val}$ be a function from elements of $x$ to elements of $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra evaluation of $\mathrm{val}$. Then the generator of $\mathrm{val}$ and $h$ is a generator of $S$ and $x$.
Algebra.Generators.ofSurjectiveAlgebraMapdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the generator of h (from the name)
English
Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then the generator of $h$ is a generator of $S$ and $\mathrm{PEmpty}$.
Algebra.Generators.reindexdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the reindexing of P and e (from the name)
English
Let $P$ be a generator of $S$ and $x_{4}$. Let $e$ be an equivalence from $x$ to $x_{4}$. Then the reindexing of $P$ and $e$ is a generator of $S$ and $x$.
Algebra.Generators.selfdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the self of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the self of $R$ and $S$ is a generator of $S$ and $S$.
Algebra.Generators.toCompdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the composition of Q and P (from the name)
English
Let $Q$ be a generator of $T$ and $x_{4}$. Let $P$ be a generator of $S$ and $x$. Then the composition of $Q$ and $P$ is a homomorphism of $P$ and the composition of $Q$ and $P$.
Algebra.Generators.toExtendScalarsdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $P$ be a generator of $T$ and $x$. Then $\operatorname{toExtendScalars}$ applied to $P$ is a homomorphism of $P$ and $\operatorname{extendScalars}$ applied to $S$ and $P$.
Algebra.Generators.toExtensiondefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the extension of P (from the docstring)
English
Let $P$ be a generator of $S$ and $x$. Then the extension of $P$ is an extension of $R$ and $S$.
Algebra.Generators.valdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
the value of self and x4 (from the name)
English
Let $\mathrm{self}$ be a generator of $S$ and $x$. Let $x_{4}$ be an element of $x$. Then the value of $\mathrm{self}$ and $x_{4}$ is an element of $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
Algebra.Generators.σdefMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $P$ be a generator of $S$ and $x$. Let $x_{4}$ be an element of $S$. Then $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_}$ applied to $P$ and $x_{4}$ is a ring of $P$ defined as $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_'}$ applied to $P$ and $x_{4}$.
Algebra.Generators.σ'defMathlib.RingTheory.Extension.Generators, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a generator of $S$ and $x$. Let $x_{4}$ be an element of $S$. Then $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_'}$ applied to $\mathrm{self}$ and $x_{4}$ is a multivariate polynomial of $x$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.

Mathlib.RingTheory.Extension.Presentation.Basic

Algebra.PresentationstructureMathlib.RingTheory.Extension.Presentation.Basic, type
Wording
presentation of x and x1 (from the name)
English
Let $R$, $S$, $x$ and $x_{1}$ be sets. Then the presentations of $x$ and $x_{1}$ are a basic type.
Algebra.Presentation.QuotientdefMathlib.RingTheory.Extension.Presentation.Basic, type
Wording
quotient of P (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Then a quotient of $P$ is an element of the function that maps $P$ to the set of quotients of the set of rings of $\operatorname{toGenerators}$ applied to $P$ and the kernel of $\operatorname{toGenerators}$ applied to $P$.
Algebra.Presentation.baseChangedefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the base change of T and P (from the name)
English
Let $T$ be a set. Let $P$ be a presentation of $x$ and $x_{1}$. Then the base change of $T$ and $P$ is a presentation of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the base change of $T$ and $\operatorname{toGenerators}$ applied to $P$, the function that maps $i$ to $\operatorname{map}$ applied to the algebra map of $R$ and $T$ and the assignment of $P$ and $i$ and $\mathrm{Algebra\_\_Presentation\_\_span\_range\_relation\_eq\_ker\_baseChange}$ applied to $T$ and $P$.
Algebra.Presentation.compdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the composition of Q and P (from the name)
English
Let $Q$ be a presentation of $x_{5}$ and $x_{6}$. Let $P$ be a presentation of $x$ and $x_{1}$. Then the composition of $Q$ and $P$ is a presentation of $\mathrm{Sum}$ applied to $x_{5}$ and $x$ and $\mathrm{Sum}$ applied to $x_{6}$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toGenerators}$ applied to $Q$ and $\operatorname{toGenerators}$ applied to $P$, $\operatorname{elim}$ applied to $\operatorname{compRelationAux}$ applied to $Q$ and $P$ and the function that maps $\mathrm{rp}$ to $\operatorname{rename}$ applied to $\operatorname{inr}$ and the assignment of $P$ and $\mathrm{rp}$ and $\mathrm{Algebra\_\_Presentation\_\_span\_range\_relation\_eq\_ker\_comp}$ applied to $Q$ and $P$.
Algebra.Presentation.dimensiondefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the dimension of P (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Then the dimension of $P$ is a natural number defined as the difference between the cardinality of $x$ and the cardinality of $x_{1}$.
Algebra.Presentation.iddefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the identity of R (from the name)
English
Let $R$ be a set. Then the identity of $R$ is a presentation of $\mathrm{PEmpty}$ and $\mathrm{PEmpty}$ defined as the presentation of $\mathrm{Function\_\_bijective\_id}$.
Algebra.Presentation.localizationAwaydefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
no wording
English
Let $S$ be a set. Let $r$ be an element of $R$. Then $\operatorname{localizationAway}$ applied to $S$ and $r$ is a presentation of $\mathrm{Unit}$ and $\mathrm{Unit}$.
Algebra.Presentation.mvPolynomialdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the multivariate polynomial of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the multivariate polynomial of $R$ and $x$ is a presentation of $x$ and $\mathrm{PEmpty}$.
Algebra.Presentation.naivedefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the naive presentation of s and hs (from the docstring)
English
Let $s$ be an element of $\mathrm{optParam}$ applied to the set of functions from quotients of the set of multivariate polynomials of $x_{1}$ and $R$ and the span of the range of $v$ to multivariate polynomials of $x_{1}$ and $R$ and $\operatorname{surjInv}$ applied to $\mathrm{Ideal\_\_Quotient\_\_mk\_surjective}$ such that $\mathrm{autoParam}$ holds for the proposition that for all quotients $x_{3}$ of the set of multivariate polynomials of $x_{1}$ and $R$ and the span of the range of $v$, $\operatorname{mk}$ applied to the span of the range of $v$ and $s$ applied to $x_{3}$ is equal to $x_{3}$ and $\mathrm{Algebra\_\_Presentation\_\_naive\_\_\_auto\_1}$. Then the naive presentation of $s$ and $\mathrm{hs}$ is a presentation of $x_{1}$ and $x$.
Algebra.Presentation.ofAlgEquivdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the presentation of P and e (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Let $e$ be an algebra isomorphism of $S$ and $T$. Then the presentation of $P$ and $e$ is a presentation of $x$ and $x_{1}$.
Algebra.Presentation.ofBijectiveAlgebraMapdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the presentation of h (from the name)
English
Assume that $\operatorname{coe}$ applied to the algebra map of $R$ and $S$ is bijective. Then the presentation of $h$ is a presentation of $\mathrm{PEmpty}$ and $\mathrm{PEmpty}$.
Algebra.Presentation.ofFinitePresentationdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the presentation of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the presentation of $R$ and $S$ is a presentation of $\mathrm{Fin}$ applied to the presentation of $R$ and $S$ and $\mathrm{Fin}$ applied to the presentation of $R$ and $S$.
Algebra.Presentation.ofFinitePresentationRelsdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the presentation of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the presentation of $R$ and $S$ is a natural number.
Algebra.Presentation.ofFinitePresentationVarsdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the presentation of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the presentation of $R$ and $S$ is a natural number defined as $\operatorname{choose}$ applied to $\mathrm{Algebra\_\_Presentation\_\_exists\_presentation\_fin}$ applied to $R$ and $S$.
Algebra.Presentation.quotientEquivdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the quotient equivalence of P (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Then the quotient equivalence of $P$ is an algebra isomorphism of the set of quotients of $P$ and $S$.
Algebra.Presentation.reindexdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the reindexing of e and f (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Let $e$ be an equivalence from $x_{5}$ to $x$. Let $f$ be an equivalence from $x_{6}$ to $x_{1}$. Then the reindexing of $e$ and $f$ is a presentation of $x_{5}$ and $x_{6}$.
Algebra.Presentation.relationdefMathlib.RingTheory.Extension.Presentation.Basic, function or constant
Wording
the assignment of self and x5 (from the docstring)
English
Let $\mathrm{self}$ be a presentation of $x$ and $x_{1}$. Let $x_{5}$ be an element of $x_{1}$. Then the assignment of $\mathrm{self}$ and $x_{5}$ is a ring of $\operatorname{toGenerators}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{5}$.

Mathlib.RingTheory.Extension.Presentation.Core

Algebra.PreSubmersivePresentation.ofHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the submersive presentation of P and x5 (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then the submersive presentation of $P$ and $x_{5}$ is a submersive presentation of $x$ and $x_{1}$.
Algebra.Presentation.CoredefMathlib.RingTheory.Extension.Presentation.Core, type
Wording
no wording
English
Let $P$ be a presentation of $x$ and $x_{1}$. Then an element of $\operatorname{Core}$ applied to $P$ is an element of the function that maps $P$ to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{core} (P)}{x_{5}})}$.
Algebra.Presentation.HasCoeffsclassMathlib.RingTheory.Extension.Presentation.Core, predicate
Wording
no wording
English
Let $P$ be a presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then we can say that $\operatorname{HasCoeffs}$ holds for $P$ and $x_{5}$.
Algebra.Presentation.ModelOfHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, type
Wording
model of x5 (from the docstring)
English
Let $x_{5}$ be a set. Then a model of $x_{5}$ is an element of the function that maps $x_{5}$ to the set of quotients of the set of multivariate polynomials of $x$ and $x_{5}$ and the span of the range of $\operatorname{relationOfHasCoeffs}$ applied to $x_{5}$.
Algebra.Presentation.coeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
no wording
English
Let $P$ be a presentation of $x$ and $x_{1}$. Then $\operatorname{coeffs}$ applied to $P$ is an element of $\wp R$ defined as the union of the function that maps $i$ to $\operatorname{coeffs}$ applied to the assignment of $P$ and $i$.
Algebra.Presentation.coredefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the core of P (from the docstring)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Then the core of $P$ is a subalgebra of $\Integer$ and $R$ defined as $\operatorname{adjoin}$ applied to $\Integer$ and $\operatorname{coeffs}$ applied to $P$.
Algebra.Presentation.relationOfHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the relation of x5 and r (from the name)
English
Let $x_{5}$ be a set. Let $r$ be an element of $x_{1}$. Then the relation of $x_{5}$ and $r$ is a multivariate polynomial of $x$ and $x_{5}$ defined as $\operatorname{choose}$ applied to $\mathrm{Algebra\_\_Presentation\_\_HasCoeffs\_\_relation\_mem\_range\_map}$ applied to $x_{5}$ and $r$.
Algebra.Presentation.tensorModelOfHasCoeffsEquivdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the tensor model of x5 (from the name)
English
Let $x_{5}$ be a set. Then the tensor model of $x_{5}$ is an algebra isomorphism of the set of tensor products of $R$ and the set of models of $x_{5}$ and $S$ defined as the algebra isomorphism of the tensor model of $P$ and $x_{5}$ and the tensor model of $P$ and $x_{5}$.
Algebra.Presentation.tensorModelOfHasCoeffsHomdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the tensor model of P and x5 (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then the tensor model of $P$ and $x_{5}$ is an algebra homomorphism of the set of tensor products of $R$ and the set of models of $x_{5}$ and $S$.
Algebra.Presentation.tensorModelOfHasCoeffsInvdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the tensor model of P and x5 (from the name)
English
Let $P$ be a presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then the tensor model of $P$ and $x_{5}$ is an algebra homomorphism of $S$ and the set of tensor products of $R$ and the set of models of $x_{5}$.
Algebra.SubmersivePresentation.HasCoeffsclassMathlib.RingTheory.Extension.Presentation.Core, predicate
Wording
no wording
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then we can say that $\operatorname{HasCoeffs}$ holds for $P$ and $x_{5}$.
Algebra.SubmersivePresentation.coeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
no wording
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then $\operatorname{coeffs}$ applied to $P$ is an element of $\wp R$ defined as the union of the union of $\operatorname{coeffs}$ applied to $\operatorname{toPresentation}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$ and $\operatorname{coeffs}$ applied to $\mathrm{Algebra\_\_Generators\_\_\_u3c3\_}$ applied to $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$ and the underlying value in the base of $\operatorname{inv}$ applied to the unit of $\mathrm{Algebra\_\_SubmersivePresentation\_\_jacobian\_isUnit}$ applied to $P$ and the union of the function that maps $i$ to $\operatorname{coeffs}$ applied to the jacobian relation of $P$ and $i$.
Algebra.SubmersivePresentation.invJacobianOfHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
no wording
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then $\operatorname{invJacobianOfHasCoeffs}$ applied to $P$ and $x_{5}$ is a multivariate polynomial of $x$ and $x_{5}$.
Algebra.SubmersivePresentation.jacobianOfHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
no wording
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then $\operatorname{jacobianOfHasCoeffs}$ applied to $P$ and $x_{5}$ is a multivariate polynomial of $x$ and $x_{5}$ defined as the determinant of the Jacobi matrix of the submersive presentation of $\operatorname{toPreSubmersivePresentation}$ applied to $P$ and $x_{5}$.
Algebra.SubmersivePresentation.jacobianRelationsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the jacobian relation of P and s (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $s$ be an element of $x_{1}$. Then the jacobian relation of $P$ and $s$ is a multivariate polynomial of $x$ and $R$.
Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the jacobian relation of P and i (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Let $i$ be an element of $x_{1}$. Then the jacobian relation of $P$ and $i$ is a multivariate polynomial of $x$ and $x_{5}$.
Algebra.SubmersivePresentation.ofHasCoeffsdefMathlib.RingTheory.Extension.Presentation.Core, function or constant
Wording
the submersive presentation of P and x5 (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be a set. Then the submersive presentation of $P$ and $x_{5}$ is a submersive presentation of $x$ and $x_{1}$.

Mathlib.RingTheory.Extension.Presentation.Submersive

Algebra.PreSubmersivePresentationstructureMathlib.RingTheory.Extension.Presentation.Submersive, type
Wording
submersive presentation of x and x1 (from the name)
English
Let $R$, $S$, $x$ and $x_{1}$ be sets. Then the submersive presentations of $x$ and $x_{1}$ are a basic type.
Algebra.PreSubmersivePresentation.aevalDifferentialdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the algebra evaluation differential of P (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the algebra evaluation differential of $P$ is a linear map of the set of functions from elements of $x_{1}$ to elements of $S$ and the set of functions from elements of $x_{1}$ to elements of $S$ defined as $\operatorname{constr}$ applied to the basis function of $S$ and $x_{1}$, $S$ and the function that maps $j_{1}$ and $i_{1}$ to $\operatorname{aeval}$ applied to $\operatorname{val}$ applied to $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ and $\operatorname{pderiv}$ applied to the map of $P$ and $i_{1}$ and the assignment of $\operatorname{toPresentation}$ applied to $P$ and $j_{1}$.
Algebra.PreSubmersivePresentation.baseChangedefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the base change of T and P (from the name)
English
Let $T$ be a set. Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the base change of $T$ and $P$ is a submersive presentation of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the base change of $T$ and $\operatorname{toPresentation}$ applied to $P$, $\operatorname{map}$ applied to $P$ and $\mathrm{Algebra\_\_PreSubmersivePresentation\_\_map\_inj}$ applied to $P$.
Algebra.PreSubmersivePresentation.basisdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the standard basis of P (from the docstring)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the standard basis of $P$ is a basis of the set of rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ and the set of functions from elements of $x_{1}$ to rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ defined as the basis function of the set of rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ and $x_{1}$.
Algebra.PreSubmersivePresentation.compdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the composition of Q and P (from the name)
English
Let $Q$ be a submersive presentation of $x_{5}$ and $x_{6}$. Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the composition of $Q$ and $P$ is a submersive presentation of $\mathrm{Sum}$ applied to $x_{5}$ and $x$ and $\mathrm{Sum}$ applied to $x_{6}$ and $x_{1}$.
Algebra.PreSubmersivePresentation.differentialdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the differential of P (from the docstring)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the differential of $P$ is a linear map of the set of functions from elements of $x_{1}$ to rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ and the set of functions from elements of $x_{1}$ to rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ defined as $\operatorname{constr}$ applied to the standard basis of $P$, the set of rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ and the function that maps $j_{1}$ and $i_{1}$ to $\operatorname{pderiv}$ applied to the map of $P$ and $i_{1}$ and the assignment of $\operatorname{toPresentation}$ applied to $P$ and $j_{1}$.
Algebra.PreSubmersivePresentation.jacobiMatrixdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the Jacobi matrix of P (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the Jacobi matrix of $P$ is a matrix of $x_{1}$ and the set of rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$ defined as $\operatorname{toMatrix}$ applied to the standard basis of $P$, the standard basis of $P$ and the differential of $P$.
Algebra.PreSubmersivePresentation.jacobiandefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
no wording
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then $\operatorname{jacobian}$ applied to $P$ is an element of $S$ defined as $\operatorname{algebraMap}$ applied to the set of rings of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $P$, $S$ and $\operatorname{det}$ applied to the differential of $P$.
Algebra.PreSubmersivePresentation.localizationAwaydefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
no wording
English
Let $S$ be a set. Let $r$ be an element of $R$. Then $\operatorname{localizationAway}$ applied to $S$ and $r$ is a submersive presentation of $\mathrm{Unit}$ and $\mathrm{Unit}$ defined as $\operatorname{mk}$ applied to $\operatorname{localizationAway}$ applied to $S$ and $r$, the function that maps $x_{3}$ to $\operatorname{unit}$ and the function that maps $x_{4}$, $x_{5}$ and $h_{1}$ to $h_{1}$.
Algebra.PreSubmersivePresentation.mapdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the map of self and x5 (from the name)
English
Let $\mathrm{self}$ be a submersive presentation of $x$ and $x_{1}$. Let $x_{5}$ be an element of $x_{1}$. Then the map of $\mathrm{self}$ and $x_{5}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{5}$.
Algebra.PreSubmersivePresentation.mvPolynomialdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the multivariate polynomial of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the multivariate polynomial of $R$ and $x$ is a submersive presentation of $x$ and $\mathrm{PEmpty}$.
Algebra.PreSubmersivePresentation.naivedefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
no wording
English
Let $a$ be an injective function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\mathrm{optParam}$ applied to the set of functions from quotients of the set of multivariate polynomials of $x_{1}$ and $R$ and the span of the range of $v$ to multivariate polynomials of $x_{1}$ and $R$ and $\operatorname{surjInv}$ applied to $\mathrm{Ideal\_\_Quotient\_\_mk\_surjective}$ such that $\mathrm{autoParam}$ holds for the proposition that for all quotients $x_{3}$ of the set of multivariate polynomials of $x_{1}$ and $R$ and the span of the range of $v$, $\operatorname{mk}$ applied to the span of the range of $v$ and $s$ applied to $x_{3}$ is equal to $x_{3}$ and $\mathrm{Algebra\_\_PreSubmersivePresentation\_\_naive\_\_\_auto\_1}$. Then $\operatorname{naive}$ applied to $a$, $\mathrm{ha}$, $s$ and $\mathrm{hs}$ is a submersive presentation of $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to the naive presentation of $s$ and $\mathrm{hs}$, $a$ and $\mathrm{ha}$.
Algebra.PreSubmersivePresentation.ofAlgEquivdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the submersive presentation of P and e (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $e$ be an algebra isomorphism of $S$ and $T$. Then the submersive presentation of $P$ and $e$ is a submersive presentation of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the presentation of $\operatorname{toPresentation}$ applied to $P$ and $e$, $\operatorname{map}$ applied to $P$ and $\mathrm{Algebra\_\_PreSubmersivePresentation\_\_map\_inj}$ applied to $P$.
Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMapdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the submersive presentation of h (from the name)
English
Assume that $\operatorname{coe}$ applied to the algebra map of $R$ and $S$ is bijective. Then the submersive presentation of $h$ is a submersive presentation of $\mathrm{PEmpty}$ and $\mathrm{PEmpty}$.
Algebra.PreSubmersivePresentation.reindexdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the reindexing of e and f (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $e$ be an equivalence from $x_{5}$ to $x$. Let $f$ be an equivalence from $x_{6}$ to $x_{1}$. Then the reindexing of $e$ and $f$ is a submersive presentation of $x_{5}$ and $x_{6}$.
Algebra.SubmersivePresentationstructureMathlib.RingTheory.Extension.Presentation.Submersive, type
Wording
submersive presentation of x and x1 (from the name)
English
Let $R$, $S$, $x$ and $x_{1}$ be sets. Then the submersive presentations of $x$ and $x_{1}$ are a basic type.
Algebra.SubmersivePresentation.aevalDifferentialEquivdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the algebra evaluation differential equivalence of P (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the algebra evaluation differential equivalence of $P$ is a linear equivalence of the set of functions from elements of $x_{1}$ to elements of $S$ and the set of functions from elements of $x_{1}$ to elements of $S$.
Algebra.SubmersivePresentation.baseChangedefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the base change of T and P (from the name)
English
Let $T$ be a set. Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the base change of $T$ and $P$ is a submersive presentation of $x$ and $x_{1}$.
Algebra.SubmersivePresentation.basisDerivdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the basis derivative of P (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the basis derivative of $P$ is a basis of $S$ and the set of functions from elements of $x_{1}$ to elements of $S$ defined as the map of the basis function of $S$ and $x_{1}$ and the algebra evaluation differential equivalence of $P$.
Algebra.SubmersivePresentation.compdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the composition of Q and P (from the name)
English
Let $Q$ be a submersive presentation of $x_{5}$ and $x_{6}$. Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the composition of $Q$ and $P$ is a submersive presentation of $\mathrm{Sum}$ applied to $x_{5}$ and $x$ and $\mathrm{Sum}$ applied to $x_{6}$ and $x_{1}$.
Algebra.SubmersivePresentation.iddefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the identity of R (from the name)
English
Let $R$ be a set. Then the identity of $R$ is a submersive presentation of $\mathrm{PEmpty}$ and $\mathrm{PEmpty}$ defined as the submersive presentation of $\mathrm{Function\_\_bijective\_id}$.
Algebra.SubmersivePresentation.localizationAwaydefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
no wording
English
Let $S$ be a set. Let $r$ be an element of $R$. Then $\operatorname{localizationAway}$ applied to $S$ and $r$ is a submersive presentation of $\mathrm{Unit}$ and $\mathrm{Unit}$.
Algebra.SubmersivePresentation.mvPolynomialdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the multivariate polynomial of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the multivariate polynomial of $R$ and $x$ is a submersive presentation of $x$ and $\mathrm{PEmpty}$.
Algebra.SubmersivePresentation.ofAlgEquivdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the submersive presentation of P and e (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $e$ be an algebra isomorphism of $S$ and $T$. Then the submersive presentation of $P$ and $e$ is a submersive presentation of $x$ and $x_{1}$.
Algebra.SubmersivePresentation.ofBijectiveAlgebraMapdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the submersive presentation of h (from the name)
English
Assume that $\operatorname{coe}$ applied to the algebra map of $R$ and $S$ is bijective. Then the submersive presentation of $h$ is a submersive presentation of $\mathrm{PEmpty}$ and $\mathrm{PEmpty}$.
Algebra.SubmersivePresentation.ofSubsingletondefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the submersive presentation of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the submersive presentation of $R$ and $S$ is a submersive presentation of $\mathrm{PUnit}$ and $\mathrm{PUnit}$.
Algebra.SubmersivePresentation.reindexdefMathlib.RingTheory.Extension.Presentation.Submersive, function or constant
Wording
the reindexing of e and f (from the name)
English
Let $P$ be a submersive presentation of $x$ and $x_{1}$. Let $e$ be an equivalence from $x_{5}$ to $x$. Let $f$ be an equivalence from $x_{6}$ to $x_{1}$. Then the reindexing of $e$ and $f$ is a submersive presentation of $x_{5}$ and $x_{6}$.

Mathlib.RingTheory.FilteredAlgebra.Basic

IsFiltrationclassMathlib.RingTheory.FilteredAlgebra.Basic, predicate
Wording
no wording
English
Let $F$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{F\_lt}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{IsFiltration}$ holds for $F$ and $\mathrm{F\_lt}$.
IsModuleFiltrationclassMathlib.RingTheory.FilteredAlgebra.Basic, predicate
Wording
no wording
English
Let $F$ be a function from elements of $x$ to elements of $x_{2}$. Let $\mathrm{F\_lt}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x$ to elements of $x_{2}$. Let $\mathrm{F'}$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Let $\mathrm{F'\_lt}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x_{1}$ to elements of $x_{3}$. Then we can say that $\mathrm{IsModuleFiltration}$ holds for $F$, $\mathrm{F\_lt}$, $\mathrm{F'}$ and $\mathrm{F'\_lt}$.
IsRingFiltrationclassMathlib.RingTheory.FilteredAlgebra.Basic, predicate
Wording
no wording
English
Let $F$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{F\_lt}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{IsRingFiltration}$ holds for $F$ and $\mathrm{F\_lt}$.

Mathlib.RingTheory.Filtration

Ideal.FiltrationstructureMathlib.RingTheory.Filtration, type
Wording
filtration of I and M (from the name)
English
Let $I$ be an ideal of $R$. Let $M$ be a set. Then the filtrations of $I$ and $M$ are a basic type.
Ideal.Filtration.NdefMathlib.RingTheory.Filtration, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a filtration of $I$ and $M$. Let $x_{3}$ be a natural number. Then $\operatorname{N}$ applied to $\mathrm{self}$ and $x_{3}$ is a submodule of $R$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.
Ideal.Filtration.StabledefMathlib.RingTheory.Filtration, predicate
Wording
F is stable (from the name)
English
Let $F$ be a filtration of $I$ and $M$. Then $F$ is stable, if there exists a natural number $x_{3}$, such that for all natural numbers $n$, if $n \geq x_{3}$, then $\EqtMACRoH {\HSMulhSMulMACRoAL {I}{\operatorname{N} (F , n)}}{\operatorname{N} (F , n + 1)}$.
Ideal.Filtration.submoduledefMathlib.RingTheory.Filtration, function or constant
Wording
the submodule of F (from the name)
English
Let $F$ be a filtration of $I$ and $M$. Then the submodule of $F$ is a submodule of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{reesAlgebra} (I)}{x_{3}})}$ and the set of polynomial modules of $R$ and $M$.
Ideal.Filtration.submoduleInfHomdefMathlib.RingTheory.Filtration, function or constant
Wording
the submodule infimum homomorphism of M and I (from the name)
English
Let $M$ be a set. Let $I$ be an ideal of $R$. Then the submodule infimum homomorphism of $M$ and $I$ is an infimum homomorphism of the set of filtrations of $I$ and $M$ and the set of submodules of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{reesAlgebra} (I)}{x_{3}})}$ and the set of polynomial modules of $R$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{submodule}$ and $\mathrm{Ideal\_\_Filtration\_\_inf\_submodule}$.
Ideal.stableFiltrationdefMathlib.RingTheory.Filtration, function or constant
Wording
the stable filtration of I and N (from the name)
English
Let $I$ be an ideal of $R$. Let $N$ be a submodule of $R$ and $M$. Then the stable filtration of $I$ and $N$ is a filtration of $I$ and $M$.
Ideal.trivialFiltrationdefMathlib.RingTheory.Filtration, function or constant
Wording
the trivial filtration of I and N (from the name)
English
Let $I$ be an ideal of $R$. Let $N$ be a submodule of $R$ and $M$. Then the trivial filtration of $I$ and $N$ is a filtration of $I$ and $M$.

Mathlib.RingTheory.FiniteLength

IsFiniteLengthinductiveMathlib.RingTheory.FiniteLength, predicate
Wording
no wording
English
Let $R$ and $M$ be sets. Then we can say that $\mathrm{IsFiniteLength}$ holds for $R$ and $M$.
IsFiniteLength.belowinductiveMathlib.RingTheory.FiniteLength, predicate
Wording
no wording
English
Assume that $\mathrm{IsFiniteLength}$ holds for $R$ and $M$. Then we can say that $\operatorname{below}$ holds for $t$.

Mathlib.RingTheory.FinitePresentation

AlgHom.FinitePresentationdefMathlib.RingTheory.FinitePresentation, predicate
Wording
f is a finite presentation (from the name)
English
Let $f$ be an algebra homomorphism of $A$ and $B$. Then $f$ is a finite presentation, if $\operatorname{toRingHom}$ applied to $f$ is a finite presentation.
Algebra.FinitePresentationclassMathlib.RingTheory.FinitePresentation, predicate
Wording
no wording
English
Let $R$ and $A$ be sets. Then we can say that $\operatorname{FinitePresentation}$ holds for $R$ and $A$.
RingHom.FinitePresentationdefMathlib.RingTheory.FinitePresentation, predicate
Wording
f is a finite presentation (from the name)
English
Let $f$ be a ring homomorphism of $A$ and $B$. Then $f$ is a finite presentation, if $\operatorname{FinitePresentation}$ holds for $A$ and $B$.

Mathlib.RingTheory.FiniteType

AlgHom.FiniteTypedefMathlib.RingTheory.FiniteType, predicate
Wording
f is a finite type (from the name)
English
Let $f$ be an algebra homomorphism of $A$ and $B$. Then $f$ is a finite type, if $\operatorname{toRingHom}$ applied to $f$ is a finite type.
Algebra.FiniteTypeclassMathlib.RingTheory.FiniteType, predicate
Wording
no wording
English
Let $R$ and $A$ be sets. Then we can say that $\operatorname{FiniteType}$ holds for $R$ and $A$.
RingHom.FiniteTypedefMathlib.RingTheory.FiniteType, predicate
Wording
f is a finite type (from the name)
English
Let $f$ be a ring homomorphism of $A$ and $B$. Then $f$ is a finite type, if $\operatorname{FiniteType}$ holds for $A$ and $B$.

Mathlib.RingTheory.Finiteness.Cardinality

Module.Finite.kerReprdefMathlib.RingTheory.Finiteness.Cardinality, function or constant
Wording
the kernel of R and M (from the docstring)
English
Let $R$ and $M$ be sets. Then the kernel of $R$ and $M$ is a submodule of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to $\operatorname{choose}$ applied to $\mathrm{Module\_\_Finite\_\_exists\_fin'}$ applied to $R$ and $M$ to elements of $R$.
Module.Finite.kerReprₛdefMathlib.RingTheory.Finiteness.Cardinality, function or constant
Wording
the kernel representation of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the kernel representation of $R$ and $M$ is a module congruence relation of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to $\operatorname{choose}$ applied to $\mathrm{Module\_\_Finite\_\_exists\_fin'}$ applied to $R$ and $M$ to elements of $R$.
Module.Finite.reprdefMathlib.RingTheory.Finiteness.Cardinality, type
Wording
representation of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the representations of $R$ and $M$ are a basic type.
Module.Finite.reprEquivdefMathlib.RingTheory.Finiteness.Cardinality, function or constant
Wording
the representative of R and M (from the docstring)
English
Let $R$ and $M$ be sets. Then the representative of $R$ and $M$ is a linear equivalence of the set of representations of $R$ and $M$ and $M$.
Module.Finite.reprEquivₛdefMathlib.RingTheory.Finiteness.Cardinality, function or constant
Wording
the representative of R and M (from the docstring)
English
Let $R$ and $M$ be sets. Then the representative of $R$ and $M$ is a linear equivalence of the set of representations of $R$ and $M$ and $M$.
Module.Finite.reprₛdefMathlib.RingTheory.Finiteness.Cardinality, type
Wording
representation of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a representation of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of quotients of the set of functions from elements of $\mathrm{Fin}$ applied to $\operatorname{choose}$ applied to $\mathrm{Module\_\_Finite\_\_exists\_fin'}$ applied to $R$ and $M$ to elements of $R$ and the kernel representation of $R$ and $M$.

Mathlib.RingTheory.Finiteness.Cofinite

Submodule.CoFGdefMathlib.RingTheory.Finiteness.Cofinite, predicate
Wording
no wording
English
Let $S$ be a submodule of $R$ and $M$. Then $\operatorname{CoFG}$ holds for $S$, if $\operatorname{Finite}$ holds for $R$ and the set of quotients of $M$ and $S$.

Mathlib.RingTheory.Finiteness.Defs

AlgHom.FinitedefMathlib.RingTheory.Finiteness.Defs, predicate
Wording
f is finite (from the name)
English
Let $f$ be an algebra homomorphism of $A$ and $B$. Then $f$ is finite, if $\operatorname{toRingHom}$ applied to $f$ is finite.
Ideal.FGdefMathlib.RingTheory.Finiteness.Defs, predicate
Wording
no wording
English
Let $I$ be an ideal of $R$. Then $\operatorname{FG}$ holds for $I$, if there exists a finite set $S$ of $R$, such that the span of $S$ is equal to $I$.
Module.FiniteclassMathlib.RingTheory.Finiteness.Defs, predicate
Wording
no wording
English
Let $R$ and $M$ be sets. Then we can say that $\operatorname{Finite}$ holds for $R$ and $M$.
RingHom.FinitedefMathlib.RingTheory.Finiteness.Defs, predicate
Wording
f is finite (from the name)
English
Let $f$ be a ring homomorphism of $A$ and $B$. Then $f$ is finite, if $\operatorname{Finite}$ holds for $A$ and $B$.
Submodule.FGdefMathlib.RingTheory.Finiteness.Defs, predicate
Wording
no wording
English
Let $N$ be a submodule of $R$ and $M$. Then $\operatorname{FG}$ holds for $N$, if there exists a finite set $S$ of $M$, such that the span of $R$ and $S$ is equal to $N$.

Mathlib.RingTheory.Finiteness.Finsupp

LinearMap.finsuppLinearMapdefMathlib.RingTheory.Finiteness.Finsupp, function or constant
Wording
the finitely supported function linear map of S (from the name)
English
Let $S$ be a set. Then the finitely supported function linear map of $S$ is a linear map of the set of finitely supported functions from $x$ to the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $\FinsuppMACRoQ {x}{N}$.

Mathlib.RingTheory.Flat.Basic

Module.FlatclassMathlib.RingTheory.Flat.Basic, predicate
Wording
M is flat with respect to R (from the name)
English
Let $R$ and $M$ be sets. Then we can say that $M$ is flat with respect to $R$.
Submodule.toBaseChange.toLinearEquivdefMathlib.RingTheory.Flat.Basic, function or constant
Wording
the linear equivalence of A and p (from the name)
English
Let $A$ be a set. Let $p$ be a submodule of $R$ and $M$. Then the linear equivalence of $A$ and $p$ is a linear equivalence of the set of tensor products of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{baseChange} (A , p)}{x_{6}})}$.

Mathlib.RingTheory.Flat.Equalizer

AlgHom.tensorEqualizerdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the tensor equalizer of f and g (from the name)
English
Let $S$ and $T$ be sets. Let $f$ and $g$ be algebra homomorphisms of $A$ and $B$. Then the tensor equalizer of $f$ and $g$ is an algebra homomorphism of the set of tensor products of $T$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{equalizer} (\operatorname{map} (\operatorname{id} (S , T), f), \operatorname{map} (\operatorname{id} (S , T), g))}{x_{11}})}$.
AlgHom.tensorEqualizerEquivdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the tensor equalizer equivalence of f and g (from the name)
English
Let $S$ and $T$ be sets. Let $f$ and $g$ be algebra homomorphisms of $A$ and $B$. Then the tensor equalizer equivalence of $f$ and $g$ is an algebra isomorphism of the set of tensor products of $T$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{equalizer} (\operatorname{map} (\operatorname{id} (S , T), f), \operatorname{map} (\operatorname{id} (S , T), g))}{x_{11}})}$.
Algebra.kerTensorProductMapIdToAlgHomEquivdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the kernel tensor product map identity to algebra homomorphism equivalence of A and h2 (from the name)
English
Let $R$, $S$, $T$ and $A$ be sets such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $S$ and $T$. Then the kernel tensor product map identity to algebra homomorphism equivalence of $A$ and $h_{2}$ is a linear equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{map} (\operatorname{id} (A , A), \operatorname{toAlgHom} (S , T)))}{x_{8}})}$ and the set of tensor products of the set of tensor products of $A$ and $S$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{algebraMap} (S , T))}{x_{9}})}$.
LinearMap.kerLTensorEquivOfSurjectivedefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the kernel tensor equivalence of f (from the name)
English
Let $f$ be a linear map of $N$ and $P$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $A$ be a set. Then the kernel tensor equivalence of $f$ is a linear equivalence of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{lTensor} (A , f))}{x_{7}})}$ and the set of tensor products of $A$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{8}})}$.
LinearMap.tensorEqLocusdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
no wording
English
Let $S$ and $M$ be sets. Let $f$ and $g$ be linear maps of $N$ and $P$. Then $\operatorname{tensorEqLocus}$ applied to $S$, $M$, $f$ and $g$ is a linear map of the set of tensor products of $M$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (f , g)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (\operatorname{lTensor} (S , M , f), \operatorname{lTensor} (S , M , g))}{x_{11}})}$ defined as the lift of $\operatorname{tensorEqLocusBil}$ applied to $S$, $M$, $f$ and $g$.
LinearMap.tensorEqLocusBildefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
no wording
English
Let $S$ and $M$ be sets. Let $f$ and $g$ be linear maps of $N$ and $P$. Then $\operatorname{tensorEqLocusBil}$ applied to $S$, $M$, $f$ and $g$ is a linear map of $M$ and the set of linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (f , g)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (\operatorname{lTensor} (S , M , f), \operatorname{lTensor} (S , M , g))}{x_{11}})}$.
LinearMap.tensorEqLocusEquivdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
no wording
English
Let $S$ and $M$ be sets. Let $f$ and $g$ be linear maps of $N$ and $P$. Then $\operatorname{tensorEqLocusEquiv}$ applied to $S$, $M$, $f$ and $g$ is a linear equivalence of the set of tensor products of $M$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (f , g)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (\operatorname{lTensor} (S , M , f), \operatorname{lTensor} (S , M , g))}{x_{11}})}$.
LinearMap.tensorEqLocusInvdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
no wording
English
Let $S$ and $M$ be sets. Let $f$ and $g$ be linear maps of $N$ and $P$. Then $\operatorname{tensorEqLocusInv}$ applied to $S$, $M$, $f$ and $g$ is a linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (\operatorname{lTensor} (S , M , f), \operatorname{lTensor} (S , M , g))}{x_{10}})}$ and the set of tensor products of $M$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{eqLocus} (f , g)}{x_{11}})}$.
LinearMap.tensorKerdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the tensor kernel of f (from the name)
English
Let $S$ and $M$ be sets. Let $f$ be a linear map of $N$ and $P$. Then the tensor kernel of $f$ is a linear map of the set of tensor products of $M$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{lTensor} (S , M , f))}{x_{11}})}$ defined as the lift of $\operatorname{tensorKerBil}$ applied to $S$, $M$ and $f$.
LinearMap.tensorKerBildefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
no wording
English
Let $S$ and $M$ be sets. Let $f$ be a linear map of $N$ and $P$. Then $\operatorname{tensorKerBil}$ applied to $S$, $M$ and $f$ is a linear map of $M$ and the set of linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{lTensor} (S , M , f))}{x_{11}})}$.
LinearMap.tensorKerEquivdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the tensor kernel equivalence of f (from the name)
English
Let $S$ and $M$ be sets. Let $f$ be a linear map of $N$ and $P$. Then the tensor kernel equivalence of $f$ is a linear equivalence of the set of tensor products of $M$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{lTensor} (S , M , f))}{x_{11}})}$.
LinearMap.tensorKerInvdefMathlib.RingTheory.Flat.Equalizer, function or constant
Wording
the tensor kernel inverse of f (from the name)
English
Let $S$ and $M$ be sets. Let $f$ be a linear map of $N$ and $P$. Then the tensor kernel inverse of $f$ is a linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{lTensor} (S , M , f))}{x_{10}})}$ and the set of tensor products of $M$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{11}})}$.
RingHom.HasStableEqualizersdefMathlib.RingTheory.Flat.Equalizer, predicate
Wording
P has stable equalizers (from the name)
English
Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then $R$ has stable equalizers, if for all sets $R$, $S$, $A$ and $B$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all elements $x_{1}$ of $\mathrm{CommRing}$ applied to $S$, for all elements $x_{2}$ of $\mathrm{CommRing}$ applied to $A$, for all elements $x_{3}$ of $\mathrm{CommRing}$ applied to $B$, for all elements $x_{4}$ of $\mathrm{Algebra}$ applied to $R$ and $A$, for all elements $x_{5}$ of $\mathrm{Algebra}$ applied to $R$ and $S$, for all elements $x_{6}$ of $\mathrm{Algebra}$ applied to $R$ and $B$, for all algebra homomorphisms $f$ and $g$ of $A$ and $B$, if $R$ holds for $R$, $A$, $x$, $x_{2}$ and the algebra map of $R$ and $A$, then if $R$ holds for $R$, $B$, $x$, $x_{3}$ and the algebra map of $R$ and $B$, then $\operatorname{coe}$ applied to the tensor equalizer of $f$ and $g$ is bijective.

Mathlib.RingTheory.Flat.EquationalCriterion

Module.IsTrivialRelationdefMathlib.RingTheory.Flat.EquationalCriterion, predicate
Wording
no wording
English
Let $f$ be a function from elements of $x_{3}$ to elements of $R$. Let $x_{5}$ be a function from elements of $x_{3}$ to elements of $M$. Then $\operatorname{IsTrivialRelation}$ holds for $f$ and $x_{5}$, if there exists a natural number $k$, such that there exists a function $a$ from elements of $x_{3}$ and elements of $\mathrm{Fin}$ applied to $k$ to elements of $R$, such that there exists a function $y$ from elements of $\mathrm{Fin}$ applied to $k$ to elements of $M$, such that for all elements $i$ of $x_{3}$, $\EqtMACRoH {x_{5} (i)}{\FinsetSum {\FinsetunivMACRoAC}{j}{(\HSMulhSMulMACRoAL {a (i , j)}{y (j)})}}$ and for all elements $j_{1}$ of $\mathrm{Fin}$ applied to $k$, $\EqtMACRoH {\FinsetSum {\FinsetunivMACRoAC}{i_{1}}{(f (i_{1})\times a (i_{1} , j_{1}))}}{0}$.

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Module.FaithfullyFlatclassMathlib.RingTheory.Flat.FaithfullyFlat.Basic, predicate
Wording
M is faithfully flat with respect to R (from the name)
English
generation took over the time limit
Submodule.baseChangeOrderEmbeddingdefMathlib.RingTheory.Flat.FaithfullyFlat.Basic, function or constant
Wording
the base change order embedding of M and A (from the name)
English
Let $R$, $M$ and $A$ be sets. Then the base change order embedding of $M$ and $A$ is an order embedding of the set of submodules of $R$ and $M$ and the set of submodules of $A$ and the set of tensor products of $A$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{baseChange}$ applied to $A$ and the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Submodule\_\_baseChange\_injective}$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Submodule\_\_baseChange\_le\_iff}$.

Mathlib.RingTheory.Flat.Rank

RingHom.finrankdefMathlib.RingTheory.Flat.Rank, function or constant
Wording
the rank of f and x2 (from the docstring)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be a prime spectrum of $R$. Then the rank of $f$ and $x_{2}$ is a natural number defined as the rank at stalk of $S$ and $x_{2}$.

Mathlib.RingTheory.FormalGroup.Basic

FormalGroupstructureMathlib.RingTheory.FormalGroup.Basic, type
Wording
formal group of R (from the name)
English
Let $R$ be a set. Then the formal groups of $R$ are a basic type.
FormalGroup.IsCommclassMathlib.RingTheory.FormalGroup.Basic, predicate
Wording
F is commutative (from the name)
English
Let $F$ be a formal group of $R$. Then we can say that $F$ is commutative.
FormalGroup.PointdefMathlib.RingTheory.FormalGroup.Basic, type
Wording
point of F and x1 (from the name)
English
Let $F$ be a formal group of $R$. Let $x_{1}$ be a set. Then a point of $F$ and $x_{1}$ is an element of the function that maps $F$ and $x_{1}$ to $\SubtypeSet {f}{\operatorname{HasSubst} (f)}$.
FormalGroup.XzerodefMathlib.RingTheory.FormalGroup.Basic, function or constant
Wording
no wording
English
Let $F$ be a formal group of $R$. Then there is a power series of $R$. Proof. Let $F$ be arbitrary. By PowerSeries__X. By 0. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By F. By FormalGroup__toPowerSeries. By MvPowerSeries__subst.
FormalGroup.mapdefMathlib.RingTheory.FormalGroup.Basic, function or constant
Wording
the map of F and f (from the name)
English
Let $F$ be a formal group of $R$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $F$ and $f$ is a formal group of $S$.
FormalGroup.toPowerSeriesdefMathlib.RingTheory.FormalGroup.Basic, function or constant
Wording
the power series of self (from the name)
English
Let $\mathrm{self}$ be a formal group of $R$. Then the power series of $\mathrm{self}$ is a multivariate power series of $\mathrm{Fin}$ applied to $2$ and $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FormalGroup.zeroXdefMathlib.RingTheory.FormalGroup.Basic, function or constant
Wording
the zero of F (from the name)
English
Let $F$ be a formal group of $R$. Then the zero of $F$ is a power series of $R$ defined as the substitution of $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecCons}$ applied to $\operatorname{X}$ and $\operatorname{vecEmpty}$ and the power series of $F$.
FormalGroup.𝔾ₐdefMathlib.RingTheory.FormalGroup.Basic, function or constant
Wording
no wording
English
$\mathrm{FormalGroup\_\_\_u1d53e\_\_u2090\_}$ is a formal group of $R$.
FormalGroup.𝔾ₘdefMathlib.RingTheory.FormalGroup.Basic, function or constant
Wording
no wording
English
$\mathrm{FormalGroup\_\_\_u1d53e\_\_u2098\_}$ is a formal group of $R$.

Mathlib.RingTheory.FractionalIdeal.Basic

FractionalIdealdefMathlib.RingTheory.FractionalIdeal.Basic, type
Wording
fractional ideal of S and P (from the name)
English
Let $S$ be a submonoid of $R$. Let $P$ be a set. Then a fractional ideal of $S$ and $P$ is an element of the function that maps $S$ and $P$ to $\SubtypeSet {I}{\mathrm{IsFractional} (I , S)}$.
FractionalIdeal.coeIdealdefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the coercion ideal of I (from the name)
English
Let $I$ be an ideal of $R$. Then the coercion ideal of $I$ is a fractional ideal of $S$ and $P$ defined as the coercion submodule of $P$ and $I$.
FractionalIdeal.coeIdealHomdefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the coercion ideal homomorphism of S and P (from the name)
English
Let $S$ be a submonoid of $R$. Let $P$ be a set. Then the coercion ideal homomorphism of $S$ and $P$ is a ring homomorphism of the set of ideals of $R$ and the set of fractional ideals of $S$ and $P$.
FractionalIdeal.coeSubmoduleHomdefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the coercion submodule homomorphism of S and P (from the name)
English
Let $S$ be a submonoid of $R$. Let $P$ be a set. Then the coercion submodule homomorphism of $S$ and $P$ is a ring homomorphism of the set of fractional ideals of $S$ and $P$ and the set of submodules of $R$ and $P$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coeToSubmodule}$ and $\mathrm{FractionalIdeal\_\_coe\_one}$ and $\mathrm{FractionalIdeal\_\_coe\_mul}$, $\mathrm{FractionalIdeal\_\_coe\_zero}$ and $\mathrm{FractionalIdeal\_\_coe\_add}$.
FractionalIdeal.coeToSubmoduledefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the coercion to submodule of I (from the name)
English
Let $I$ be a fractional ideal of $S$ and $P$. Then the coercion to submodule of $I$ is a submodule of $R$ and $P$ defined as $I$.
FractionalIdeal.copydefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the copy of p and s (from the name)
English
Let $p$ be a fractional ideal of $S$ and $P$. Let $s$ be an element of $\wp P$ such that $\EqtMACRoH {s}{p}$. Then the copy of $p$ and $s$ is a fractional ideal of $S$ and $P$ defined as the copy of the coercion to submodule of $p$ and $s$.
FractionalIdeal.dendefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the denominator of I (from the name)
English
Let $I$ be a fractional ideal of $S$ and $P$. Then the denominator of $I$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$.
FractionalIdeal.equivNumdefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the linear equivalence between the fractional ideal of h_nz (from the docstring)
English
Assume that $\operatorname{den} (I)\neq 0$. Then the linear equivalence between the fractional ideal of $\mathrm{h\_nz}$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (I)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{num} (I)}{x_{4}})}$.
FractionalIdeal.equivNumOfIsLocalizationdefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the equivalence numerator of I (from the name)
English
Let $I$ be a fractional ideal of $S$ and $P$. Then the equivalence numerator of $I$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (I)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{num} (I)}{x_{4}})}$.
FractionalIdeal.equivNumOfIsSMulRegulardefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the linear equivalence between the fractional ideal of reg (from the docstring)
English
Assume that the denominator of $I$ is a multiplicative regular. Then the linear equivalence between the fractional ideal of $\mathrm{reg}$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (I)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{num} (I)}{x_{4}})}$.
FractionalIdeal.muldefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the product of I and J (from the name)
English
Let $I$ and $J$ be fractional ideals of $S$ and $P$. Then the product of $I$ and $J$ is a fractional ideal of $S$ and $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{FractionalIdeal\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_RingTheory\_\_FractionalIdeal\_\_Basic\_\_1107666208\_\_\_hygCtx\_\_\_hyg\_\_2}$, $I$ and $J$.
FractionalIdeal.numdefMathlib.RingTheory.FractionalIdeal.Basic, function or constant
Wording
the numerator of I (from the name)
English
Let $I$ be a fractional ideal of $S$ and $P$. Then the numerator of $I$ is an ideal of $R$ defined as the preimage of the linear map of $R$ and $P$ and $\HSMulhSMulMACRoAL {\operatorname{den} (I)}{\operatorname{coeToSubmodule} (I)}$.
IsFractionaldefMathlib.RingTheory.FractionalIdeal.Basic, predicate
Wording
I is fractional with respect to S (from the name)
English
Let $S$ be a submonoid of $R$. Let $I$ be a submodule of $R$ and $P$. Then $I$ is fractional with respect to $S$, if there exists an element $a$ of $R$, such that $a$ is an element of $S$ and for all elements $b$ of $P$, if $b$ is an element of $I$, then $\HSMulhSMulMACRoAL {a}{b}$ is an integer.

Mathlib.RingTheory.FractionalIdeal.Extended

FractionalIdeal.extendeddefMathlib.RingTheory.FractionalIdeal.Extended, function or constant
Wording
no wording
English
Let $L$ be a set. Assume that $M$ is less than or equal to the preimage of $f$ and $N$. Let $I$ be a fractional ideal of $M$ and $K$. Then $\operatorname{extended}$ applied to $L$, $\mathrm{hf}$ and $I$ is a fractional ideal of $N$ and $L$ defined as the span of $B$ and the image of $\operatorname{coe}$ applied to the map of $f$ and $I$.
FractionalIdeal.extendedHomdefMathlib.RingTheory.FractionalIdeal.Extended, function or constant
Wording
the extended homomorphism of L and B (from the name)
English
Let $L$ and $B$ be sets. Then the extended homomorphism of $L$ and $B$ is a ring homomorphism of the set of fractional ideals of the non zero divisor of $A$ and $K$ and the set of fractional ideals of the non zero divisor of $B$ and $L$.
FractionalIdeal.extendedHom'defMathlib.RingTheory.FractionalIdeal.Extended, function or constant
Wording
the extended homomorphism of L and hf (from the name)
English
Let $L$ be a set. Assume that $M$ is less than or equal to the preimage of $f$ and $N$. Then the extended homomorphism of $L$ and $\mathrm{hf}$ is a ring homomorphism of the set of fractional ideals of $M$ and $K$ and the set of fractional ideals of $N$ and $L$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{extended}$ applied to $L$ and $\mathrm{hf}$ and $\mathrm{FractionalIdeal\_\_extended\_one}$ applied to $L$ and $\mathrm{hf}$ and $\mathrm{FractionalIdeal\_\_extended\_mul}$ applied to $L$ and $\mathrm{hf}$, $\mathrm{FractionalIdeal\_\_extended\_zero}$ applied to $L$ and $\mathrm{hf}$ and $\mathrm{FractionalIdeal\_\_extended\_add}$ applied to $L$ and $\mathrm{hf}$.

Mathlib.RingTheory.FractionalIdeal.Norm

FractionalIdeal.absNormdefMathlib.RingTheory.FractionalIdeal.Norm, function or constant
Wording
the absolute norm of the fractional ideal (from the docstring)
English
The absolute norm of the fractional ideal is a monoid with zero homomorphism of the set of fractional ideals of the non zero divisor of $R$ and $K$ and $\Rational$.

Mathlib.RingTheory.FractionalIdeal.Operations

FractionalIdeal.adjoinIntegraldefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
no wording
English
Let $S$ be a submonoid of $R$. Let $x_{3}$ be an integral element of $P$. Then $\operatorname{adjoinIntegral}$ applied to $S$, $x_{3}$ and $\mathrm{hx}$ is a fractional ideal of $S$ and $P$ defined as $\operatorname{toSubmodule}$ applied to $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{3}$.
FractionalIdeal.canonicalEquivdefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the canonical equivalence of S (from the name)
English
Let $S$ be a submonoid of $R$. Let $P$ and $\mathrm{P'}$ be sets. Then the canonical equivalence of $S$ is a ring isomorphism of the set of fractional ideals of $S$ and $P$ and the set of fractional ideals of $S$ and $\mathrm{P'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{FractionalIdeal\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_RingTheory\_\_FractionalIdeal\_\_Operations\_\_2300950166\_\_\_hygCtx\_\_\_hyg\_\_2}$, $S$, $P$ and $\mathrm{P'}$.
FractionalIdeal.mapdefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the map of g and x5 (from the name)
English
Let $g$ be an algebra homomorphism of $P$ and $\mathrm{P'}$. Let $x_{5}$ be a fractional ideal of $S$ and $P$. Then the map of $g$ and $x_{5}$ is a fractional ideal of $S$ and $\mathrm{P'}$ defined as the map of the linear map of $g$ and the coercion to submodule of $x_{5}$.
FractionalIdeal.mapEquivdefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the map equivalence of g (from the name)
English
Let $g$ be an algebra isomorphism of $P$ and $\mathrm{P'}$. Then the map equivalence of $g$ is a ring isomorphism of the set of fractional ideals of $S$ and $P$ and the set of fractional ideals of $S$ and $\mathrm{P'}$.
FractionalIdeal.ringEquivOfRingEquivdefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the ring isomorphism of f (from the name)
English
Let $K$ and $L$ be sets. Let $f$ be a ring isomorphism of $R$ and $S$. Then the ring isomorphism of $f$ is a ring isomorphism of the set of fractional ideals of the non zero divisor of $R$ and $K$ and the set of fractional ideals of the non zero divisor of $S$ and $L$.
FractionalIdeal.spanFinsetdefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the span finite set of s and f (from the name)
English
Let $x$ be a set. Let $s$ be a finite set of $x_{4}$. Let $f$ be a function from elements of $x_{4}$ to elements of $K$. Then the span finite set of $s$ and $f$ is a fractional ideal of the non zero divisor of $x$ and $K$ defined as the span of $x$ and the image of $f$ and $s$.
FractionalIdeal.spanSingletondefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the span singleton of S (from the name)
English
Let $S$ be a submonoid of $R$. Then the span singleton of $S$ is a monoid with zero homomorphism of $P$ and the set of fractional ideals of $S$ and $P$.
FractionalIdeal.unitsMulEquivSubmoduledefMathlib.RingTheory.FractionalIdeal.Operations, function or constant
Wording
the unit multiplicative equivalence submodule (from the name)
English
The unit multiplicative equivalence submodule is a multiplicative equivalence of the set of units of the set of fractional ideals of $S$ and $P$ and the set of units of the set of submodules of $R$ and $P$.

Mathlib.RingTheory.FreeCommRing

FreeCommRingdefMathlib.RingTheory.FreeCommRing, type
Wording
free commutative ring of x (from the name)
English
Let $x$ be a set. Then a free commutative ring of $x$ is an element of the function that maps $x$ to the set of monoid algebras of $\Integer$ and the set of multiplicatives of the set of multisets of $x$.
FreeCommRing.IsSupporteddefMathlib.RingTheory.FreeCommRing, predicate
Wording
no wording
English
Let $x_{1}$ be a free commutative ring of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{IsSupported}$ holds for $x_{1}$ and $s$, if $x_{1}$ is an element of the closure of the image of $\operatorname{of}$ and $s$.
FreeCommRing.liftdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from elements of $x$ to elements of $R$ to the set of ring homomorphisms of the set of free commutative rings of $x$ and $R$.
FreeCommRing.mapdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a ring homomorphism of the set of free commutative rings of $x$ and the set of free commutative rings of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.
FreeCommRing.ofdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free commutative ring of $x$ defined as $\operatorname{single}$ applied to $\operatorname{ofAdd}$ applied to $\operatorname{singleton}$ applied to $x_{1}$ and $1$.
FreeCommRing.restrictiondefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the restriction of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the restriction of $s$ is a ring homomorphism of the set of free commutative rings of $x$ and the set of free commutative rings of the set of elements of $s$ defined as $\operatorname{lift}$ applied to the function that maps $a_{1}$ to $\mathrm{dite}$ applied to $\MembershipmemMACRoT {s}{a_{1}}$, the function that maps $H$ to $\operatorname{of}$ applied to $a_{1}$ and the function that maps $H_{1}$ to $0$.
FreeRing.castFreeCommRingdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the cast free commutative ring of x1 (from the name)
English
Let $x_{1}$ be a free ring of $x$. Then the cast free commutative ring of $x_{1}$ is a free commutative ring of $x$ defined as the coercion of the free commutative ring and $x_{1}$.
FreeRing.coeRingHomdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the coercion ring homomorphism of x (from the name)
English
Let $x$ be a set. Then the coercion ring homomorphism of $x$ is a ring homomorphism of the set of free rings of $x$ and the set of free commutative rings of $x$ defined as the free commutative ring.
FreeRing.subsingletonEquivFreeCommRingdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the subsingleton equivalence free commutative ring of x (from the name)
English
Let $x$ be a set. Then the subsingleton equivalence free commutative ring of $x$ is a ring isomorphism of the set of free rings of $x$ and the set of free commutative rings of $x$.
FreeRing.toFreeCommRingdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the free commutative ring (from the name)
English
The free commutative ring is a ring homomorphism of the set of free rings of $x$ and the set of free commutative rings of $x$ defined as $\operatorname{lift}$ applied to $\operatorname{of}$.
freeCommRingEquivMvPolynomialIntdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the free commutative ring isomorphism multivariate polynomial integer of x (from the name)
English
Let $x$ be a set. Then the free commutative ring isomorphism multivariate polynomial integer of $x$ is a ring isomorphism of the set of free commutative rings of $x$ and the set of multivariate polynomials of $x$ and $\Integer$.
freeCommRingPEmptyEquivIntdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the free commutative ring on the empty type (from the docstring)
English
The free commutative ring on the empty type is a ring isomorphism of the set of free commutative rings of $\mathrm{PEmpty}$ and $\Integer$ defined as the composition of the free commutative ring isomorphism multivariate polynomial integer of $\mathrm{PEmpty}$ and $\operatorname{isEmptyRingEquiv}$ applied to $\Integer$ and $\mathrm{PEmpty}$.
freeCommRingPUnitEquivPolynomialIntdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the free commutative ring (from the docstring)
English
The free commutative ring is a ring isomorphism of the set of free commutative rings of $\mathrm{PUnit}$ and the set of polynomials of $\Integer$ defined as the composition of the free commutative ring isomorphism multivariate polynomial integer of $\mathrm{PUnit}$ and the ring isomorphism of the unique algebra isomorphism of $\Integer$ and $\mathrm{PUnit}$.
freeRingPEmptyEquivIntdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the free ring on the empty type (from the docstring)
English
The free ring on the empty type is a ring isomorphism of the set of free rings of $\mathrm{PEmpty}$ and $\Integer$ defined as the composition of the subsingleton equivalence free commutative ring of $\mathrm{PEmpty}$ and the free commutative ring on the empty type.
freeRingPUnitEquivPolynomialIntdefMathlib.RingTheory.FreeCommRing, function or constant
Wording
the free ring (from the docstring)
English
The free ring is a ring isomorphism of the set of free rings of $\mathrm{PUnit}$ and the set of polynomials of $\Integer$ defined as the composition of the subsingleton equivalence free commutative ring of $\mathrm{PUnit}$ and the free commutative ring.

Mathlib.RingTheory.FreeRing

FreeRingdefMathlib.RingTheory.FreeRing, type
Wording
free ring of x (from the name)
English
Let $x$ be a set. Then a free ring of $x$ is an element of the function that maps $x$ to the set of monoid algebras of $\Integer$ and the set of free monoids of $x$.
FreeRing.liftdefMathlib.RingTheory.FreeRing, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from elements of $x$ to elements of $R$ to the set of ring homomorphisms of the set of free rings of $x$ and $R$ defined as the composition of the composition of the lift and the lift of $R$ and the set of free monoids of $x$ and the inverse of the equivalence integer algebra homomorphism of the set of monoid algebras of $\Integer$ and the set of free monoids of $x$ and $R$.
FreeRing.mapdefMathlib.RingTheory.FreeRing, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a ring homomorphism of the set of free rings of $x$ and the set of free rings of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.
FreeRing.ofdefMathlib.RingTheory.FreeRing, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free ring of $x$ defined as $\operatorname{single}$ applied to $\operatorname{of}$ applied to $x_{1}$ and $1$.

Mathlib.RingTheory.Frobenius

AlgHom.IsArithFrobAtdefMathlib.RingTheory.Frobenius, predicate
Wording
no wording
English
Let $x_{3}$ be an algebra homomorphism of $S$ and $S$. Let $Q$ be an ideal of $S$. Then $\operatorname{IsArithFrobAt}$ holds for $x_{3}$ and $Q$, if for all elements $x_{4}$ of $S$, the difference between $x_{3}$ applied to $x_{4}$ and the exponentiation of $x_{4}$ to the cardinality of the set of quotients of $R$ and $\operatorname{under}$ applied to $R$ and $Q$ is an element of $Q$.
AlgHom.IsArithFrobAt.localizedefMathlib.RingTheory.Frobenius, function or constant
Wording
no wording
English
Assume that $\operatorname{IsArithFrobAt}$ holds for $x_{3}$ and $Q$. Then $\operatorname{localize}$ applied to $H$ is an algebra homomorphism of $\operatorname{AtPrime}$ applied to $Q$ and $\operatorname{AtPrime}$ applied to $Q$.
AlgHom.IsArithFrobAt.restrictdefMathlib.RingTheory.Frobenius, function or constant
Wording
no wording
English
Assume that $\operatorname{IsArithFrobAt}$ holds for $x_{3}$ and $Q$. Then $\operatorname{restrict}$ applied to $H$ is an algebra homomorphism of the set of quotients of $S$ and $Q$ and the set of quotients of $S$ and $Q$.
IsArithFrobAtdefMathlib.RingTheory.Frobenius, predicate
Wording
no wording
English
Let $R$ be a set. Let $x_{5}$ be an element of $M$. Let $Q$ be an ideal of $S$. Then $\mathrm{IsArithFrobAt}$ holds for $R$, $x_{5}$ and $Q$, if $\operatorname{IsArithFrobAt}$ holds for the algebra homomorphism of $x_{5}$ and $Q$.
arithFrobAtdefMathlib.RingTheory.Frobenius, function or constant
Wording
no wording
English
Let $R$ and $G$ be sets. Let $Q$ be an ideal of $S$. Then $\mathrm{arithFrobAt}$ applied to $R$, $G$ and $Q$ is an element of $G$.

Mathlib.RingTheory.GradedAlgebra.AlgHom

GradedAlgHomstructureMathlib.RingTheory.GradedAlgebra.AlgHom, type
Wording
graded algebra homomorphism of x8 and x9 (from the name)
English
Let $R$ be a set. Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then the graded algebra homomorphisms of $x_{8}$ and $x_{9}$ are a basic type.
GradedAlgHom.compdefMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
the composition of g and f (from the name)
English
Let $g$ be a graded algebra homomorphism of $x_{11}$ and $x_{12}$. Let $f$ be a graded algebra homomorphism of $x_{10}$ and $x_{11}$. Then the composition of $g$ and $f$ is a graded algebra homomorphism of $x_{10}$ and $x_{12}$.
GradedAlgHom.iddefMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
the identity of R and x6 (from the name)
English
Let $R$ be a set. Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $A$. Then the identity of $R$ and $x_{6}$ is a graded algebra homomorphism of $x_{6}$ and $x_{6}$.
GradedAlgHom.mk'defMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
no wording
English
Let $f$ be a graded ring homomorphism of $x_{8}$ and $x_{9}$ such that for all elements $c$ of $R$, for all elements $x_{12}$ of $A$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {c}{x_{12}})}{\HSMulhSMulMACRoAL {c}{f (x_{12})}}$. Then $\operatorname{mk'}$ applied to $f$ and $h$ is a graded algebra homomorphism of $x_{8}$ and $x_{9}$.
GradedAlgHom.ofClassdefMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
the graded algebra homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the graded algebra homomorphism of $f$ is a graded algebra homomorphism of $x_{8}$ and $x_{9}$.
GradedAlgHom.restrictScalarsdefMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
no wording
English
Let $x_{12}$ be a set. Let $f$ be a graded algebra homomorphism of $x_{8}$ and $x_{9}$. Then $\operatorname{restrictScalars}$ applied to $x_{12}$ and $f$ is a graded algebra homomorphism of the function that maps $x_{17}$ to $\operatorname{restrictScalars}$ applied to $x_{12}$ and $x_{8}$ applied to $x_{17}$ and the function that maps $x_{18}$ to $\operatorname{restrictScalars}$ applied to $x_{12}$ and $x_{9}$ applied to $x_{18}$ defined as $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $x_{12}$ and $\operatorname{toAlgHom}$ applied to $f$ and $\mathrm{GradedAlgHom\_\_map\_mem}$ applied to $f$.
GradedAlgHom.toEnddefMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
the end (from the name)
English
The end is a monoid homomorphism of the set of graded algebra homomorphisms of $x_{6}$ and $x_{6}$ and the set of algebra homomorphisms of $A$ and $A$.
GradedAlgHom.toGradedRingHomdefMathlib.RingTheory.GradedAlgebra.AlgHom, function or constant
Wording
the graded ring homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a graded algebra homomorphism of $x_{8}$ and $x_{9}$. Then the graded ring homomorphism of $\mathrm{self}$ is a graded ring homomorphism of $x_{8}$ and $x_{9}$ defined as $\operatorname{mk}$ applied to $\operatorname{toRingHom}$ applied to $\operatorname{toAlgHom}$ applied to $\mathrm{self}$ and $\mathrm{GradedAlgHom\_\_map\_mem}$ applied to $\mathrm{self}$.

Mathlib.RingTheory.GradedAlgebra.Basic

DirectSum.IsInternal.coeAlgEquivdefMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
the canonical isomorphism of hM (from the docstring)
English
Assume that $M$ is internal. Then the canonical isomorphism of $\mathrm{hM}$ is an algebra isomorphism of the set of direct sums of $x_{3}$ and the function that maps $i$ to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {M (i)}{x_{6}})}$ and $A$.
DirectSum.decomposeAlgEquivdefMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
no wording
English
Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $A$. Then $\operatorname{decomposeAlgEquiv}$ applied to $x_{6}$ is an algebra isomorphism of $A$ and the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6} (i)}{x_{8}})}$.
DirectSum.decomposeRingEquivdefMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
no wording
English
Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{decomposeRingEquiv}$ applied to $x_{6}$ is a ring isomorphism of $A$ and the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6} (i)}{x_{8}})}$.
GradedAlgebradefMathlib.RingTheory.GradedAlgebra.Basic, type
Wording
graded algebra of x6 (from the name)
English
Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $A$. Then a graded algebra of $x_{6}$ is an element of the function that maps $x_{6}$ to the proposition that $x_{6}$ is a graded ring.
GradedAlgebra.projdefMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
the projection of x6 and i (from the name)
English
Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $i$ be an element of $x$. Then the projection of $x_{6}$ and $i$ is a linear map of $A$ and $A$ defined as the composition of the subtype of $x_{6}$ applied to $i$ and the composition of $\operatorname{lapply}$ applied to $i$ and the linear map of the algebra homomorphism of $\operatorname{decomposeAlgEquiv}$ applied to $x_{6}$.
GradedRingclassMathlib.RingTheory.GradedAlgebra.Basic, predicate
Wording
x6 is a graded ring (from the name)
English
Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $x_{6}$ is a graded ring.
GradedRing.projdefMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
the projection of x6 and i (from the name)
English
Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Let $i$ be an element of $x$. Then the projection of $x_{6}$ and $i$ is an additive monoid homomorphism of $A$ and $A$ defined as the composition of the subtype of $x_{6}$ applied to $i$ and the composition of the evaluation additive monoid homomorphism of $i$ and the additive monoid homomorphism of the ring homomorphism of $\operatorname{decomposeRingEquiv}$ applied to $x_{6}$.
GradedRing.projZeroRingHomdefMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
the projection zero ring homomorphism of x7 (from the name)
English
Let $x_{7}$ be a function from elements of $x$ to elements of $x_{1}$. Then the projection zero ring homomorphism of $x_{7}$ is a ring homomorphism of $A$ and $A$.
GradedRing.projZeroRingHom'defMathlib.RingTheory.GradedAlgebra.Basic, function or constant
Wording
the projection zero ring homomorphism of x7 (from the name)
English
Let $x_{7}$ be a function from elements of $x$ to elements of $x_{1}$. Then the projection zero ring homomorphism of $x_{7}$ is a ring homomorphism of $A$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{7} (0)}{x_{9}})}$.

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

HomogeneousIdealdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, type
Wording
homogeneous ideal of x4 (from the name)
English
Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Then a homogeneous ideal of $x_{4}$ is an element of the function that maps $x_{4}$ to the set of homogeneous submodules of $x_{4}$ and $x_{4}$.
HomogeneousIdeal.irrelevantdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
no wording
English
Let $x_{7}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{irrelevant}$ applied to $x_{7}$ is a homogeneous ideal of $x_{7}$.
HomogeneousIdeal.toIdealdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
the ideal of I (from the name)
English
Let $I$ be a homogeneous ideal of $x_{4}$. Then the ideal of $I$ is an ideal of $A$ defined as $\operatorname{toSubmodule}$ applied to $I$.
Ideal.IsHomogeneousdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, predicate
Wording
no wording
English
Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $I$ be an ideal of $A$. Then $\operatorname{IsHomogeneous}$ holds for $x_{4}$ and $I$, if $\operatorname{IsHomogeneous}$ holds for $I$ and $x_{4}$.
Ideal.homogeneousCoredefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
no wording
English
Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $I$ be an ideal of $A$. Then $\operatorname{homogeneousCore}$ applied to $x_{4}$ and $I$ is a homogeneous ideal of $x_{4}$.
Ideal.homogeneousCore'defMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
no wording
English
Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $I$ be an ideal of $A$. Then $\operatorname{homogeneousCore'}$ applied to $x_{4}$ and $I$ is an ideal of $A$ defined as the span of the image of $\operatorname{IsHomogeneousElem}$ applied to $x_{4}$ and the preimage of $\operatorname{IsHomogeneousElem}$ applied to $x_{4}$ and $I$.
Ideal.homogeneousCore.gidefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
no wording
English
Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{gi}$ applied to $x_{6}$ is a Galois coinsertion of $\operatorname{toIdeal}$ and $\operatorname{homogeneousCore}$ applied to $x_{6}$.
Ideal.homogeneousHulldefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
the homogeneous hull of x6 and I (from the name)
English
Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Let $I$ be an ideal of $A$. Then the homogeneous hull of $x_{6}$ and $I$ is a homogeneous ideal of $x_{6}$.
Ideal.homogeneousHull.gidefMathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, function or constant
Wording
no wording
English
Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{gi}$ applied to $x_{6}$ is a Galois insertion of $\operatorname{homogeneousHull}$ applied to $x_{6}$ and $\operatorname{toIdeal}$.

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

HomogeneousIdeal.comapdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Maps, function or constant
Wording
the preimage of f and I (from the name)
English
Let $f$ be a graded ring homomorphism of $x_{9}$ and $x_{10}$. Let $I$ be a homogeneous ideal of $x_{10}$. Then the preimage of $f$ and $I$ is a homogeneous ideal of $x_{9}$.
HomogeneousIdeal.mapdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Maps, function or constant
Wording
the map of f and I (from the name)
English
Let $f$ be a graded ring homomorphism of $x_{9}$ and $x_{10}$. Let $I$ be a homogeneous ideal of $x_{9}$. Then the map of $f$ and $I$ is a homogeneous ideal of $x_{10}$.

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

HomogeneousSubmodulestructureMathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule, type
Wording
homogeneous submodule of x7 and x8 (from the name)
English
Let $x_{7}$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{8}$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Then the homogeneous submodules of $x_{7}$ and $x_{8}$ are a basic type.
Submodule.IsHomogeneousdefMathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule, predicate
Wording
no wording
English
Let $p$ be a submodule of $A$ and $M$. Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{IsHomogeneous}$ holds for $p$ and $x_{5}$, if $\operatorname{IsHomogeneous}$ holds for $x_{5}$ and $p$.

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

HomogeneousSubsemiringstructureMathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring, type
Wording
homogeneous subsemiring of x5 (from the name)
English
Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Then the homogeneous subsemirings of $x_{5}$ are a basic type.
Subsemiring.homogeneousCoredefMathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring, function or constant
Wording
no wording
English
Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Let $R$ be a subsemiring of $A$. Then $\operatorname{homogeneousCore}$ applied to $x_{5}$ and $R$ is a homogeneous subsemiring of $x_{5}$.

‹ previous next ›