Definitions: Mathlib.RingTheory, part 5 of 6

OreLocalization.oreDivAddChar'defMathlib.RingTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $r$ and $\mathrm{r'}$ be elements of $X$. Let $s$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$. Let $\mathrm{s'}$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$. Then $\operatorname{oreDivAddChar'}$ applied to $r$, $\mathrm{r'}$, $s$ and $\mathrm{s'}$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r''}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s''}$ to the proposition that $\EqtMACRoH {\mathrm{s''} \times s}{\mathrm{r''} \times \mathrm{s'}}$ and $\EqtMACRoH {\operatorname{oreDiv} (r , s)+ \operatorname{oreDiv} (\mathrm{r'} , \mathrm{s'})}{\operatorname{oreDiv} (\HSMulhSMulMACRoAL {\mathrm{s''}}{r}+ \HSMulhSMulMACRoAL {\mathrm{r''}}{\mathrm{r'}}, \mathrm{s''} \times s)}$.

OreLocalization.zsmuldefMathlib.RingTheory.OreLocalization.Basic, function or constant

Wording

the integer multiple of x4 and x5 (from the name)

English

Let $x_{4}$ be an integer. Let $x_{5}$ be an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$. Then the integer multiple of $x_{4}$ and $x_{5}$ is an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$ defined as $\mathrm{zsmulRec}$ applied to $\mathrm{nsmulRec}$, $x_{4}$ and $x_{5}$.

Mathlib.RingTheory.OreLocalization.NonZeroDivisors

OreLocalization.invdefMathlib.RingTheory.OreLocalization.NonZeroDivisors, function or constant

Wording

the inverse of x2 (from the name)

English

Let $x_{2}$ be an element of $\mathrm{OreLocalization}$ applied to the non zero divisor of $R$ and $R$. Then the inverse of $x_{2}$ is an element of $\mathrm{OreLocalization}$ applied to the non zero divisor of $R$ and $R$.

Mathlib.RingTheory.OreLocalization.Ring

OreLocalization.numeratorRingHomdefMathlib.RingTheory.OreLocalization.Ring, function or constant

Wording

the numerator ring homomorphism (from the name)

English

The numerator ring homomorphism is a ring homomorphism of $R$ and $\mathrm{OreLocalization}$ applied to $S$ and $R$.

OreLocalization.universalHomdefMathlib.RingTheory.OreLocalization.Ring, function or constant

Wording

the universal homomorphism of f and fS (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $T$. Let $\mathrm{fS}$ be a monoid homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and $\UnitsMACRoAO {T}$ such that for all elements $s$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, $f$ applied to $s$ is equal to the underlying value in the base of $\mathrm{fS}$ applied to $s$. Then the universal homomorphism of $f$ and $\mathrm{fS}$ is a ring homomorphism of $\mathrm{OreLocalization}$ applied to $S$ and $R$ and $T$.

Mathlib.RingTheory.OrzechProperty

OrzechPropertyclassMathlib.RingTheory.OrzechProperty, predicate

Wording

no wording

English

Let $R$ be a set. Then we can say that $\mathrm{OrzechProperty}$ holds for $R$.

Mathlib.RingTheory.Perfection

ModPdefMathlib.RingTheory.Perfection, type

Wording

no wording

English

Let $O$ be a set. Let $p$ be a natural number. Then an element of $\mathrm{ModP}$ applied to $O$ and $p$ is an element of the function that maps $O$ and $p$ to the set of quotients of $O$ and the span of $\operatorname{singleton}$ applied to $p$.

ModP.preValdefMathlib.RingTheory.Perfection, function or constant

Wording

the value of p and x3 (from the name)

English

Let $K$ and $O$ be sets. Let $v$ be a valuation of $K$ and $\mathrm{NNReal}$. Let $p$ be a natural number. Let $x_{3}$ be an element of $\mathrm{ModP}$ applied to $O$ and $p$. Then the value of $p$ and $x_{3}$ is an element of $\mathrm{NNReal}$ defined as $\iteMACRoG {(\EqtMACRoH {x_{3}}{0})}{0}{v (\operatorname{algebraMap} (O , K , \operatorname{out} (x_{3})))}$.

PerfectiondefMathlib.RingTheory.Perfection, type

Wording

perfection of x and p (from the name)

English

Let $x$ be a set. Let $p$ be a natural number. Then a perfection of $x$ and $p$ is an element of the function that maps $x$ and $p$ to $\SubtypeSet {f}{\mathrm{forall} (\Natural , \lambda n . \EqtMACRoH {(f (n + 1)^ {p})}{f (n)})}$.

Perfection.coeffdefMathlib.RingTheory.Perfection, function or constant

Wording

the coefficient of p and n (from the name)

English

Let $R$ be a set. Let $p$ and $n$ be natural numbers. Then the coefficient of $p$ and $n$ is a ring homomorphism of the set of perfections of $R$ and $p$ and $R$.

Perfection.coeffMonoidHomdefMathlib.RingTheory.Perfection, function or constant

Wording

the coefficient monoid homomorphism of p and n (from the name)

English

Let $M$ be a set. Let $p$ and $n$ be natural numbers. Then the coefficient monoid homomorphism of $p$ and $n$ is a monoid homomorphism of the set of perfections of $M$ and $p$ and $M$.

Perfection.liftdefMathlib.RingTheory.Perfection, function or constant

Wording

the lift of p (from the name)

English

Let $p$ be a natural number. Let $R$ and $S$ be sets. Then the lift of $p$ is an equivalence from the set of ring homomorphisms of $R$ and $S$ to the set of ring homomorphisms of $R$ and the set of perfections of $S$ and $p$.

Perfection.liftMonoidHomdefMathlib.RingTheory.Perfection, function or constant

Wording

the lift monoid homomorphism of p (from the name)

English

Let $p$ be a natural number. Let $M$ and $N$ be sets. Then the lift monoid homomorphism of $p$ is a multiplicative equivalence of the set of monoid homomorphisms of $M$ and $N$ and the set of monoid homomorphisms of $M$ and the set of perfections of $N$ and $p$.

Perfection.mapdefMathlib.RingTheory.Perfection, function or constant

Wording

the map of p and x2 (from the name)

English

Let $p$ be a natural number. Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Then the map of $p$ and $x_{2}$ is a ring homomorphism of the set of perfections of $R$ and $p$ and the set of perfections of $S$ and $p$.

Perfection.mapMonoidHomdefMathlib.RingTheory.Perfection, function or constant

Wording

the map monoid homomorphism of p and x2 (from the name)

English

Let $p$ be a natural number. Let $x_{2}$ be a monoid homomorphism of $M$ and $N$. Then the map monoid homomorphism of $p$ and $x_{2}$ is a monoid homomorphism of the set of perfections of $M$ and $p$ and the set of perfections of $N$ and $p$.

Perfection.pthRootdefMathlib.RingTheory.Perfection, function or constant

Wording

no wording

English

Let $R$ be a set. Let $p$ be a natural number. Then $\operatorname{pthRoot}$ applied to $R$ and $p$ is a ring homomorphism of the set of perfections of $R$ and $p$ and the set of perfections of $R$ and $p$.

Perfection.pthRootMonoidHomdefMathlib.RingTheory.Perfection, function or constant

Wording

no wording

English

Let $M$ be a set. Let $p$ be a natural number. Then $\operatorname{pthRootMonoidHom}$ applied to $M$ and $p$ is a monoid homomorphism of the set of perfections of $M$ and $p$ and the set of perfections of $M$ and $p$.

Perfection.submonoiddefMathlib.RingTheory.Perfection, function or constant

Wording

the submonoid of M and p (from the name)

English

Let $M$ be a set. Let $p$ be a natural number. Then the submonoid of $M$ and $p$ is a submonoid of the set of functions from natural numbers to elements of $M$.

Perfection.subringdefMathlib.RingTheory.Perfection, function or constant

Wording

the subring of R and p (from the name)

English

Let $R$ be a set. Let $p$ be a natural number. Then the subring of $R$ and $p$ is a subring of the set of functions from natural numbers to elements of $R$.

Perfection.subsemiringdefMathlib.RingTheory.Perfection, function or constant

Wording

the subsemiring of R and p (from the name)

English

Let $R$ be a set. Let $p$ be a natural number. Then the subsemiring of $R$ and $p$ is a subsemiring of the set of functions from natural numbers to elements of $R$.

PerfectionMapstructureMathlib.RingTheory.Perfection, predicate

Wording

no wording

English

Let $p$ be a natural number. Let $x_{2}$ be a ring homomorphism of $P$ and $R$. Then we can say that $\mathrm{PerfectionMap}$ holds for $p$ and $x_{2}$.

PerfectionMap.equivdefMathlib.RingTheory.Perfection, function or constant

Wording

the equivalence of m (from the name)

English

Assume that $\mathrm{PerfectionMap}$ holds for $p$ and $x_{2}$. Then the equivalence of $m$ is a ring isomorphism of $P$ and the set of perfections of $R$ and $p$.

PerfectionMap.liftdefMathlib.RingTheory.Perfection, function or constant

Wording

the lift of p and x3 (from the name)

English

Let $p$ be a natural number. Let $R$, $S$ and $P$ be sets. Let $x_{3}$ be a ring homomorphism of $P$ and $S$ such that $\mathrm{PerfectionMap}$ holds for $p$ and $x_{3}$. Then the lift of $p$ and $x_{3}$ is an equivalence from the set of ring homomorphisms of $R$ and $S$ to the set of ring homomorphisms of $R$ and $P$.

PerfectionMap.mapdefMathlib.RingTheory.Perfection, function or constant

Wording

the map of p and x6 (from the name)

English

Let $p$ be a natural number such that $\mathrm{PerfectionMap}$ holds for $p$ and $x_{4}$ and $\mathrm{PerfectionMap}$ holds for $p$ and $x_{5}$. Let $x_{6}$ be a ring homomorphism of $R$ and $S$. Then the map of $p$ and $x_{6}$ is a ring homomorphism of $P$ and $Q$ defined as $\operatorname{lift}$ applied to $p$, $P$, $S$, $Q$, $x_{5}$, $n$ and the composition of $x_{6}$ and $x_{4}$.

PreTiltdefMathlib.RingTheory.Perfection, type

Wording

no wording

English

Let $O$ be a set. Let $p$ be a natural number. Then an element of $\mathrm{PreTilt}$ applied to $O$ and $p$ is an element of the function that maps $O$ and $p$ to the set of perfections of $\mathrm{ModP}$ applied to $O$ and $p$ and $p$.

PreTilt.coeffdefMathlib.RingTheory.Perfection, function or constant

Wording

the coefficient of n (from the name)

English

Let $n$ be a natural number. Then the coefficient of $n$ is a ring homomorphism of $\mathrm{PreTilt}$ applied to $O$ and $p$ and $\mathrm{ModP}$ applied to $O$ and $p$ defined as the coefficient of $p$ and $n$.

PreTilt.valdefMathlib.RingTheory.Perfection, function or constant

Wording

the value of v and p (from the name)

English

Let $K$ and $O$ be sets. Let $v$ be a valuation of $K$ and $\mathrm{NNReal}$ such that $\operatorname{Integers}$ holds for $v$ and $O$. Let $p$ be a natural number. Then the value of $v$ and $p$ is a valuation of $\mathrm{PreTilt}$ applied to $O$ and $p$ and $\mathrm{NNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{valAux}$ applied to $K$, $v$, $O$ and $p$ and $\mathrm{PreTilt\_\_valAux\_zero}$, $\mathrm{PreTilt\_\_valAux\_one}$ applied to $\mathrm{hv}$ and $\mathrm{PreTilt\_\_valAux\_mul}$ applied to $\mathrm{hv}$ and $\mathrm{PreTilt\_\_valAux\_add}$ applied to $\mathrm{hv}$.

TiltdefMathlib.RingTheory.Perfection, type

Wording

no wording

English

Let $K$ and $O$ be sets. Let $v$ be a valuation of $K$ and $\mathrm{NNReal}$ such that $\operatorname{Integers}$ holds for $v$ and $O$. Let $p$ be a natural number. Then an element of $\mathrm{Tilt}$ applied to $K$, $v$, $O$, $\mathrm{hv}$ and $p$ is an element of the function that maps $K$, $v$, $O$, $\mathrm{hv}$ and $p$ to the set of fraction rings of $\mathrm{PreTilt}$ applied to $O$ and $p$.

Mathlib.RingTheory.Perfectoid.BDeRham

BDeRhamdefMathlib.RingTheory.Perfectoid.BDeRham, type

Wording

no wording

English

Let $R$ be a set. Let $p$ be a natural number. Then an element of $\mathrm{BDeRham}$ applied to $R$ and $p$ is an element of the function that maps $R$ and $p$ to the set of localizations of the closure of the image of $\operatorname{coe}$ applied to $\operatorname{of}$ applied to the kernel of $\mathrm{fontaineThetaInvertP}$ applied to $R$ and $p$ and $\operatorname{Away}$ applied to $p$ and $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that the kernel of $\mathrm{fontaineThetaInvertP}$ applied to $R$ and $p$ is equal to the span of $\operatorname{singleton}$ applied to $a$.

BDeRhamPlusdefMathlib.RingTheory.Perfectoid.BDeRham, type

Wording

no wording

English

Let $R$ be a set. Let $p$ be a natural number. Then an element of $\mathrm{BDeRhamPlus}$ applied to $R$ and $p$ is an element of the function that maps $R$ and $p$ to the set of adic completions of the kernel of $\mathrm{fontaineThetaInvertP}$ applied to $R$ and $p$ and $\operatorname{Away}$ applied to $p$.

fontaineThetaInvertPdefMathlib.RingTheory.Perfectoid.BDeRham, function or constant

Wording

no wording

English

Let $R$ be a set. Let $p$ be a natural number. Then $\mathrm{fontaineThetaInvertP}$ applied to $R$ and $p$ is a ring homomorphism of $\operatorname{Away}$ applied to $p$ and $\operatorname{Away}$ applied to $p$.

Mathlib.RingTheory.Perfectoid.FontaineTheta

WittVector.fontaineThetadefMathlib.RingTheory.Perfectoid.FontaineTheta, function or constant

Wording

no wording

English

Let $R$ be a set. Let $p$ be a natural number. Then $\operatorname{fontaineTheta}$ applied to $R$ and $p$ is a ring homomorphism of the set of Witt vectors of $p$ and $\mathrm{PreTilt}$ applied to $R$ and $p$ and $R$ defined as the lift ring homomorphism of the span of $\operatorname{singleton}$ applied to $p$ and $\operatorname{fontaineThetaModPPow}$ applied to $R$ and $p$.

WittVector.fontaineThetaModPPowdefMathlib.RingTheory.Perfectoid.FontaineTheta, function or constant

Wording

no wording

English

Let $R$ be a set. Let $p$ and $n$ be natural numbers. Then $\operatorname{fontaineThetaModPPow}$ applied to $R$, $p$ and $n$ is a ring homomorphism of the set of Witt vectors of $p$ and $\mathrm{PreTilt}$ applied to $R$ and $p$ and the set of quotients of $R$ and the exponentiation of the span of $\operatorname{singleton}$ applied to $p$ to $n + 1$ defined as the composition of $\operatorname{ghostComponentModPPow}$ applied to $n$ and the composition of the map of the coefficient of $0$ and the map of the exponentiation of the ring homomorphism of the inverse of the Frobenius automorphism of $\mathrm{PreTilt}$ applied to $R$ and $p$ and $p$ to $n$.

WittVector.ghostComponentModPPowdefMathlib.RingTheory.Perfectoid.FontaineTheta, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{ghostComponentModPPow}$ applied to $n$ is a ring homomorphism of the set of Witt vectors of $p$ and the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $p$ and the set of quotients of $R$ and the exponentiation of the span of $\operatorname{singleton}$ applied to $p$ to $n + 1$.

Mathlib.RingTheory.Perfectoid.Untilt

PreTilt.untiltdefMathlib.RingTheory.Perfectoid.Untilt, function or constant

Wording

no wording

English

$\operatorname{untilt}$ is a monoid homomorphism of $\mathrm{PreTilt}$ applied to $O$ and $p$ and $O$ defined as the Teichmuller of $p$ and the span of $\operatorname{singleton}$ applied to $p$.

Mathlib.RingTheory.PiTensorProduct

PiTensorProduct.constantBaseRingEquivdefMathlib.RingTheory.PiTensorProduct, function or constant

Wording

the constant base ring isomorphism of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the constant base ring isomorphism of $x$ and $R$ is an algebra isomorphism of the set of product tensor products of $R$ and the function that maps $x_{3}$ to $R$ and $R$.

PiTensorProduct.liftAlgHomdefMathlib.RingTheory.PiTensorProduct, function or constant

Wording

the lift algebra homomorphism of f (from the name)

English

Let $f$ be a multilinear map of $A$ and $S$ such that $\EqtMACRoH {f (1)}{1}$ and for all functions $x_{6}$ from elements $i_{2}$ of $x$ to elements of $A$ applied to $i_{2}$, for all functions $y$ from elements $i_{1}$ of $x$ to elements of $A$ applied to $i_{1}$, $\EqtMACRoH {f (x_{6} \times y)}{f (x_{6})\times f (y)}$. Then the lift algebra homomorphism of $f$ is an algebra homomorphism of the set of product tensor products of $R$ and the function that maps $i$ to $A$ applied to $i$ and $S$.

PiTensorProduct.muldefMathlib.RingTheory.PiTensorProduct, function or constant

Wording

the multiplication in tensor product of rings (from the docstring)

English

The multiplication in tensor product of rings is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to $A$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $A$ applied to $i_{1}$ and the set of product tensor products of $R$ and the function that maps $i_{2}$ to $A$ applied to $i_{2}$ defined as $\mathrm{PiTensorProduct\_\_piTensorHomMap\_u2082\_\_\_app}$ applied to $\operatorname{tprod}$ applied to $R$ and the function that maps $x_{5}$ to the product of $R$ and $A$ applied to $x_{5}$.

PiTensorProduct.singleAlgHomdefMathlib.RingTheory.PiTensorProduct, function or constant

Wording

the single algebra homomorphism of i (from the name)

English

Let $i$ be an element of $x$. Then the single algebra homomorphism of $i$ is an algebra homomorphism of $A$ applied to $i$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $A$ applied to $i_{1}$.

PiTensorProduct.tprodMonoidHomdefMathlib.RingTheory.PiTensorProduct, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{tprodMonoidHom}$ applied to $R$ is a monoid homomorphism of the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $A$ applied to $i_{1}$.

Mathlib.RingTheory.PicardGroup

ClassGroup.equivPicdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{equivPic}$ applied to $R$ is a multiplicative equivalence of the set of ideal class groups of $R$ and $\operatorname{Pic}$ applied to $R$.

CommRing.PicdefMathlib.RingTheory.PicardGroup, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\operatorname{Pic}$ applied to $R$ is an element of the function that maps $R$ to the set of shrinks of the set of units of the set of skeletons of the set of semimodule categories of $R$.

CommRing.Pic.AsModuledefMathlib.RingTheory.PicardGroup, type

Wording

no wording

English

Let $M$ be an element of $\operatorname{Pic}$ applied to $R$. Then an element of $\operatorname{AsModule}$ applied to $M$ is an element of the function that maps $M$ to the set of carriers of $\operatorname{out}$ applied to the underlying value in the base of $\operatorname{symm}$ applied to the equivalence shrink of the set of units of the set of skeletons of the set of semimodule categories of $R$ and $M$.

CommRing.Pic.functordefMathlib.RingTheory.PicardGroup, function or constant

Wording

the functor (from the name)

English

The functor is a functor of the set of commutative semi ring categories and the set of commutative group categories.

CommRing.Pic.mapAlgebradefMathlib.RingTheory.PicardGroup, function or constant

Wording

the map algebra of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the map algebra of $R$ and $A$ is a monoid homomorphism of $\operatorname{Pic}$ applied to $R$ and $\operatorname{Pic}$ applied to $A$.

CommRing.Pic.mapRingHomdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the map ring homomorphism of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map ring homomorphism of $f$ is a monoid homomorphism of $\operatorname{Pic}$ applied to $R$ and $\operatorname{Pic}$ applied to $S$ defined as the map algebra of $R$ and $S$.

CommRing.Pic.mkdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\operatorname{mk}$ applied to $R$ and $M$ is an element of $\operatorname{Pic}$ applied to $R$.

CommRing.Pic.mk.linearEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

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

English

Let $R$ and $M$ be sets. Then the linear equivalence of $R$ and $M$ is a linear equivalence of $\operatorname{AsModule}$ applied to $\operatorname{mk}$ applied to $R$ and $M$ and $M$.

CommRing.relPicdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the relative Picard group of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the relative Picard group of $R$ and $A$ is a subgroup of $\operatorname{Pic}$ applied to $R$ defined as the multiplicative kernel of the map algebra of $R$ and $A$.

Module.Flat.submoduleAlgebradefMathlib.RingTheory.PicardGroup, function or constant

Wording

the submodule algebra of e (from the name)

English

Let $e$ be a linear equivalence of the set of tensor products of $A$ and $M$ and $A$. Then the submodule algebra of $e$ is a submodule of $R$ and $A$ defined as the range of the algebra of $e$.

Module.Flat.submoduleAlgebraEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the submodule algebra equivalence of e (from the name)

English

Let $e$ be a linear equivalence of the set of tensor products of $A$ and $M$ and $A$. Then the submodule algebra equivalence of $e$ is a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{submoduleAlgebra} (e)}{x_{5}})}$ and $M$ defined as the inverse of the linear equivalence of the algebra of $e$ and $\mathrm{Module\_\_Flat\_\_toAlgebra\_injective}$ applied to $e$.

Module.Flat.tensorSubmoduleAlgebraEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the tensor submodule algebra equivalence of e (from the name)

English

Let $e$ be a linear equivalence of the set of tensor products of $A$ and $M$ and $A$. Then the tensor submodule algebra equivalence of $e$ is a linear equivalence of the set of tensor products of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{submoduleAlgebra} (e)}{x_{5}})}$ and $A$.

Module.Flat.tensorSubmoduleAlgebraEquivMuldefMathlib.RingTheory.PicardGroup, function or constant

Wording

the tensor submodule algebra equivalence product of e and I (from the name)

English

Let $e$ be a linear equivalence of the set of tensor products of $A$ and $M$ and $A$. Let $I$ be a submodule of $R$ and $A$. Then the tensor submodule algebra equivalence product of $e$ and $I$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {I}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{submoduleAlgebra} (e)}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {(I \times \operatorname{submoduleAlgebra} (e))}{x_{7}})}$.

Module.Flat.toAlgebradefMathlib.RingTheory.PicardGroup, function or constant

Wording

the algebra of e (from the name)

English

Let $e$ be a linear equivalence of the set of tensor products of $A$ and $M$ and $A$. Then the algebra of $e$ is a linear map of $M$ and $A$ defined as the composition of $\operatorname{toLinearMap}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $e$ and the composition of the tensor of $M$ and the linear map of the algebra of $R$ and $A$ and $\operatorname{toLinearMap}$ applied to the inverse of $\operatorname{lid}$ applied to $R$ and $M$.

Module.InvertibleclassMathlib.RingTheory.PicardGroup, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then we can say that $\operatorname{Invertible}$ holds for $R$ and $M$.

Module.Invertible.algEquivOfRingdefMathlib.RingTheory.PicardGroup, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the algebra isomorphism of $R$ and $A$ is an algebra isomorphism of $R$ and $A$.

Module.Invertible.leftCancelEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $P$ be a set. Let $e$ be a linear equivalence of the set of tensor products of $M$ and $N$ and $R$. Then $\operatorname{leftCancelEquiv}$ applied to $P$ and $e$ is a linear equivalence of the set of tensor products of $M$ and the set of tensor products of $N$ and $P$ and $P$ defined as the composition of the composition of the inverse of the associator of $N$ and $P$ and the tensor of $P$ and $e$ and $\operatorname{lid}$ applied to $R$ and $P$.

Module.Invertible.linearEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

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

English

Let $R$ and $M$ be sets. Then the linear equivalence of $R$ and $M$ is a linear equivalence of the set of tensor products of the set of duals of $R$ and $M$ and $M$ and $R$ defined as the linear equivalence of $\mathrm{contractLeft}$ applied to $R$ and $M$ and $\operatorname{bijective}$.

Module.Invertible.linearEquivDualdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the linear equivalence dual of e (from the name)

English

Let $e$ be a linear equivalence of the set of tensor products of $M$ and $N$ and $R$. Then the linear equivalence dual of $e$ is a linear equivalence of $M$ and the set of duals of $R$ and $N$ defined as the linear equivalence of the curry of $\operatorname{toLinearMap}$ applied to $e$ and $\mathrm{Module\_\_Invertible\_\_bijective\_curry}$ applied to $e$.

Module.Invertible.linearEquivOfLeftInversedefMathlib.RingTheory.PicardGroup, function or constant

Wording

the linear equivalence of hfg (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Then the linear equivalence of $\mathrm{hfg}$ is a linear equivalence of $M$ and $N$.

Module.Invertible.linearEquivOfRightInversedefMathlib.RingTheory.PicardGroup, function or constant

Wording

the linear equivalence of hfg (from the name)

English

Assume that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Then the linear equivalence of $\mathrm{hfg}$ is a linear equivalence of $M$ and $N$.

Module.Invertible.rTensorEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the tensor equivalence of e (from the name)

English

Let $P$ and $Q$ be sets. Let $e$ be a linear equivalence of the set of tensor products of $M$ and $N$ and $R$. Then the tensor equivalence of $e$ is a linear equivalence of the set of linear maps of $P$ and $Q$ and the set of linear maps of the set of tensor products of $P$ and $M$ and the set of tensor products of $Q$ and $M$.

Module.Invertible.rTensorInvdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the tensor inverse of e (from the name)

English

Let $P$ and $Q$ be sets. Let $e$ be a linear equivalence of the set of tensor products of $M$ and $N$ and $R$. Then the tensor inverse of $e$ is a linear map of the set of linear maps of the set of tensor products of $P$ and $M$ and the set of tensor products of $Q$ and $M$ and the set of linear maps of $P$ and $Q$ defined as the composition of $\operatorname{toLinearMap}$ applied to the composition of the right congruence of $\operatorname{rightCancelEquiv}$ applied to $Q$ and $e$ and the left congruence of $\operatorname{rightCancelEquiv}$ applied to $P$ and $e$ and the tensor homomorphism of $N$.

Module.Invertible.rightCancelEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $P$ be a set. Let $e$ be a linear equivalence of the set of tensor products of $M$ and $N$ and $R$. Then $\operatorname{rightCancelEquiv}$ applied to $P$ and $e$ is a linear equivalence of the set of tensor products of the set of tensor products of $P$ and $M$ and $N$ and $P$ defined as the composition of the composition of the associator of $M$ and $N$ and the tensor of $P$ and $e$ and $\operatorname{rid}$ applied to $R$ and $P$.

Submodule.tensorEquivMuldefMathlib.RingTheory.PicardGroup, function or constant

Wording

the tensor equivalence product of I and J (from the name)

English

Let $I$ and $J$ be elements of $\UnitsMACRoAO {\mathrm{Submodule} (R , A)}$. Then the tensor equivalence product of $I$ and $J$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{val} (I)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{val} (J)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{val} (I \times J)}{x_{5}})}$.

Submodule.tensorInvEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

the tensor inverse equivalence of I (from the name)

English

Let $I$ be an element of $\UnitsMACRoAO {\mathrm{Submodule} (R , A)}$. Then the tensor inverse equivalence of $I$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{val} (I)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{val} (\operatorname{inv} (I))}{x_{4}})}$ and $R$.

Submodule.unitsQuotEquivRelPicdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{unitsQuotEquivRelPic}$ applied to $R$ and $A$ is a multiplicative equivalence of the set of quotients of $\UnitsMACRoAO {\mathrm{Submodule} (R , A)}$ and the range of the map of the monoid homomorphism of the span singleton of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{relPic} (R , A)}{x_{3}})}$.

Submodule.unitsToPicdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{unitsToPic}$ applied to $R$ and $A$ is a monoid homomorphism of the set of units of the set of submodules of $R$ and $A$ and $\operatorname{Pic}$ applied to $R$.

Submodule.unitsToPicEquivdefMathlib.RingTheory.PicardGroup, function or constant

Wording

no wording

English

Let $I$ be an element of $\UnitsMACRoAO {\mathrm{Submodule} (R , A)}$. Then $\operatorname{unitsToPicEquiv}$ applied to $I$ is a linear equivalence of $\operatorname{AsModule}$ applied to $\operatorname{unitsToPic}$ applied to $R$, $A$ and $I$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{val} (I)}{x_{3}})}$.

Mathlib.RingTheory.Polynomial.Basic

Ideal.degreeLEdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

no wording

English

Let $I$ be an ideal of the set of polynomials of $R$. Let $n$ be an element of $\mathrm{WithBot}$ applied to $\Natural$. Then $\operatorname{degreeLE}$ applied to $I$ and $n$ is a submodule of $R$ and the set of polynomials of $R$ defined as the minimum of $\operatorname{degreeLE}$ applied to $R$ and $n$ and the ideal of $I$.

Ideal.leadingCoeffdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

the leading coefficient of I (from the name)

English

Let $I$ be an ideal of the set of polynomials of $R$. Then the leading coefficient of $I$ is an ideal of $R$ defined as the supremum of the function that maps $n$ to $\operatorname{leadingCoeffNth}$ applied to $I$ and $n$.

Ideal.leadingCoeffNthdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

no wording

English

Let $I$ be an ideal of the set of polynomials of $R$. Let $n$ be a natural number. Then $\operatorname{leadingCoeffNth}$ applied to $I$ and $n$ is an ideal of $R$ defined as the map of $\operatorname{lcoeff}$ applied to $R$ and $n$ and $\operatorname{degreeLE}$ applied to $I$ and $n$.

Ideal.ofPolynomialdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

the ideal of I (from the name)

English

Let $I$ be an ideal of the set of polynomials of $R$. Then the ideal of $I$ is a submodule of $R$ and the set of polynomials of $R$.

Polynomial.degreeLEdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be an element of $\mathrm{WithBot}$ applied to $\Natural$. Then $\operatorname{degreeLE}$ applied to $R$ and $n$ is a submodule of $R$ and the set of polynomials of $R$ defined as the infimum of the function that maps $k$ to the infimum of the function that maps $h$ to the kernel of $\operatorname{lcoeff}$ applied to $R$ and $k$.

Polynomial.degreeLTdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then $\operatorname{degreeLT}$ applied to $R$ and $n$ is a submodule of $R$ and the set of polynomials of $R$ defined as the infimum of the function that maps $k$ to the infimum of the function that maps $h$ to the kernel of $\operatorname{lcoeff}$ applied to $R$ and $k$.

Polynomial.degreeLTEquivdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then $\operatorname{degreeLTEquiv}$ applied to $R$ and $n$ is a linear equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{1}})}$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$.

Polynomial.monicEquivDegreeLTdefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

no wording

English

Let $n$ be an element of $\Natural$. Then $\operatorname{monicEquivDegreeLT}$ applied to $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{\mathrm{and} (\operatorname{Monic} (p), \mathrm{Eq} (\operatorname{natDegree} (p), n))})}{(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{1}})})}$.

Polynomial.restrictiondefMathlib.RingTheory.Polynomial.Basic, function or constant

Wording

the restriction of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the restriction of $p$ is a polynomial of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{closure} (\operatorname{coeffs} (p))}{x_{1}})}$ defined as $\FinsetSum {\operatorname{support} (p)}{i}{\operatorname{monomial} (i , \operatorname{coeff} (p , i))}$.

Mathlib.RingTheory.Polynomial.Bernstein

bernsteinPolynomialdefMathlib.RingTheory.Polynomial.Bernstein, function or constant

Wording

the Bernstein polynomial of n and x1 (from the name)

English

Let $R$ be a set. Let $n$ and $x_{1}$ be natural numbers. Then the Bernstein polynomial of $n$ and $x_{1}$ is a polynomial of $R$ defined as $\operatorname{choose} (n , x_{1})\times \operatorname{X} ^ {x_{1}}\times (1 - \operatorname{X})^ {(n - x_{1})}$.

Mathlib.RingTheory.Polynomial.Chebyshev

Polynomial.Chebyshev.CdefMathlib.RingTheory.Polynomial.Chebyshev, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an integer. Then $\operatorname{C}$ applied to $R$ and $x_{1}$ is a polynomial of $R$.

Polynomial.Chebyshev.SdefMathlib.RingTheory.Polynomial.Chebyshev, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an integer. Then $\operatorname{S}$ applied to $R$ and $x_{1}$ is a polynomial of $R$.

Polynomial.Chebyshev.TdefMathlib.RingTheory.Polynomial.Chebyshev, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an integer. Then $\operatorname{T}$ applied to $R$ and $x_{1}$ is a polynomial of $R$.

Polynomial.Chebyshev.UdefMathlib.RingTheory.Polynomial.Chebyshev, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an integer. Then $\operatorname{U}$ applied to $R$ and $x_{1}$ is a polynomial of $R$.

Polynomial.Chebyshev.chebyshevTSequencedefMathlib.RingTheory.Polynomial.Chebyshev, function or constant

Wording

the Chebyshev sequence of R (from the name)

English

Let $R$ be a set. Then the Chebyshev sequence of $R$ is a sequence of $R$.

Mathlib.RingTheory.Polynomial.Content

Polynomial.IsPrimitivedefMathlib.RingTheory.Polynomial.Content, predicate

Wording

p is primitive (from the name)

English

Let $p$ be a polynomial of $R$. Then $p$ is primitive, if for all elements $r$ of $R$, if $\divides {\operatorname{C} (r)}{p}$, then $r$ is a unit.

Polynomial.contentdefMathlib.RingTheory.Polynomial.Content, function or constant

Wording

the content of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the content of $p$ is an element of $R$ defined as the greatest common divisor of the support of $p$ and $\operatorname{coe}$ applied to the coefficient of $p$.

Polynomial.primPartdefMathlib.RingTheory.Polynomial.Content, function or constant

Wording

the primitive part of p (from the docstring)

English

Let $p$ be a polynomial of $R$. Then the primitive part of $p$ is a polynomial of $R$ defined as $\iteMACRoG {(\EqtMACRoH {p}{0})}{1}{\operatorname{choose} (\mathrm{Polynomial\_\_C\_content\_dvd} (p))}$.

Mathlib.RingTheory.Polynomial.ContentIdeal

Polynomial.contentIdealdefMathlib.RingTheory.Polynomial.ContentIdeal, function or constant

Wording

the content ideal of p (from the docstring)

English

Let $p$ be a polynomial of $R$. Then the content ideal of $p$ is an ideal of $R$ defined as the span of $\operatorname{coeffs}$ applied to $p$.

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Polynomial.cyclotomicdefMathlib.RingTheory.Polynomial.Cyclotomic.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $R$ be a set. Then $\operatorname{cyclotomic}$ applied to $n$ and $R$ is a polynomial of $R$.

Polynomial.cyclotomic'defMathlib.RingTheory.Polynomial.Cyclotomic.Basic, function or constant

Wording

no wording

English

Let $n$ be an element of $\Natural$. Let $R$ be a set. Then $\operatorname{cyclotomic'}$ applied to $n$ and $R$ is a polynomial of $R$ defined as $\FinsetProd {\mathrm{primitiveRoots} (n , R)}{x_{1}}{(\operatorname{X} - \operatorname{C} (x_{1}))}$.

Mathlib.RingTheory.Polynomial.DegreeLT

Polynomial.degreeLT.addLinearEquivdefMathlib.RingTheory.Polynomial.DegreeLT, function or constant

Wording

the additive linear equivalence of m and n (from the name)

English

Let $R$ be a set. Let $m$ and $n$ be natural numbers. Then the additive linear equivalence of $m$ and $n$ is a linear equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m + n)}{x_{1}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{3}})}$ defined as the equivalence of the basis product of $m$ and $n$ and the identity of $\mathrm{Fin}$ applied to $m + n$.

Polynomial.degreeLT.basisdefMathlib.RingTheory.Polynomial.DegreeLT, function or constant

Wording

the basis of R and n (from the name)

English

Let $R$ be a set. Let $n$ be a natural number. Then the basis of $R$ and $n$ is a basis of $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{1}})}$ defined as the basis of $\operatorname{degreeLTEquiv}$ applied to $R$ and $n$.

Polynomial.degreeLT.basisProddefMathlib.RingTheory.Polynomial.DegreeLT, function or constant

Wording

the basis product of m and n (from the name)

English

Let $R$ be a set. Let $m$ and $n$ be natural numbers. Then the basis product of $m$ and $n$ is a basis of $R$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{2}})}$ defined as the reindexing of the product of the basis of $R$ and $m$ and the basis of $R$ and $n$ and the finite sum finite equivalence.

Polynomial.taylorLinearEquivdefMathlib.RingTheory.Polynomial.DegreeLT, function or constant

Wording

the Taylor linear equivalence of r and n (from the name)

English

Let $r$ be an element of $R$. Let $n$ be a natural number. Then the Taylor linear equivalence of $r$ and $n$ is a linear equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{2}})}$ defined as the linear equivalence of $\operatorname{degreeLT}$ applied to $R$ and $n$ and $\operatorname{degreeLT}$ applied to $R$ and $n$.

Mathlib.RingTheory.Polynomial.Dickson

Polynomial.dicksondefMathlib.RingTheory.Polynomial.Dickson, function or constant

Wording

no wording

English

Let $k$ and $x_{1}$ be natural numbers. Let $a$ be an element of $R$. Then $\operatorname{dickson}$ applied to $k$, $a$ and $x_{1}$ is a polynomial of $R$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Polynomial\_\_dickson\_\_\_f}$ applied to $k$ and $a$.

Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Polynomial.IsEisensteinAtstructureMathlib.RingTheory.Polynomial.Eisenstein.Basic, predicate

Wording

no wording

English

Let $f$ be a polynomial of $R$. Let $x_{1}$ be an ideal of $R$. Then we can say that $\operatorname{IsEisensteinAt}$ holds for $f$ and $x_{1}$.

Polynomial.IsWeaklyEisensteinAtstructureMathlib.RingTheory.Polynomial.Eisenstein.Basic, predicate

Wording

no wording

English

Let $f$ be a polynomial of $R$. Let $x_{1}$ be an ideal of $R$. Then we can say that $\operatorname{IsWeaklyEisensteinAt}$ holds for $f$ and $x_{1}$.

Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Polynomial.IsDistinguishedAtstructureMathlib.RingTheory.Polynomial.Eisenstein.Distinguished, predicate

Wording

no wording

English

Let $f$ be a polynomial of $R$. Let $I$ be an ideal of $R$. Then we can say that $\operatorname{IsDistinguishedAt}$ holds for $f$ and $I$.

Mathlib.RingTheory.Polynomial.GaussNorm

Polynomial.gaussNormdefMathlib.RingTheory.Polynomial.GaussNorm, function or constant

Wording

the Gauss norm of c and p (from the name)

English

Let $v$ be an element of $F$. Let $c$ be a real number. Let $p$ be a polynomial of $R$. Then the Gauss norm of $c$ and $p$ is a real number defined as $\mathrm{dite}$ applied to the proposition that the support of $p$ is nonempty, the function that maps $h$ to the supremum of the support of $p$ and the function that maps $i$ to $v (\operatorname{coeff} (p , i))\times c ^ {i}$ and the function that maps $h_{1}$ to $0$.

Mathlib.RingTheory.Polynomial.Hermite.Basic

Polynomial.hermitedefMathlib.RingTheory.Polynomial.Hermite.Basic, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{hermite}$ applied to $x$ is a polynomial of $\Integer$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Polynomial\_\_hermite\_\_\_f}$.

Mathlib.RingTheory.Polynomial.HilbertPoly

Polynomial.hilbertPolydefMathlib.RingTheory.Polynomial.HilbertPoly, function or constant

Wording

the Hilbert polynomial of p and d (from the name)

English

Let $p$ be a polynomial of $F$. Let $d$ be a natural number. Then the Hilbert polynomial of $p$ and $d$ is a polynomial of $F$.

Polynomial.hilbertPoly_linearMapdefMathlib.RingTheory.Polynomial.HilbertPoly, function or constant

Wording

the Hilbert polynomial linear map of F and d (from the name)

English

Let $F$ be a set. Let $d$ be a natural number. Then the Hilbert polynomial linear map of $F$ and $d$ is a linear map of the set of polynomials of $F$ and the set of polynomials of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $p$ to the Hilbert polynomial of $p$ and $d$ and the function that maps $p_{1}$ and $q$ to $\mathrm{Polynomial\_\_hilbertPoly\_add\_left}$ applied to $p_{1}$, $q$ and $d$ and the function that maps $r$ and $p_{2}$ to $\mathrm{Polynomial\_\_hilbertPoly\_smul}$ applied to $r$, $p_{2}$ and $d$.

Polynomial.preHilbertPolydefMathlib.RingTheory.Polynomial.HilbertPoly, function or constant

Wording

the Hilbert polynomial of d and k (from the name)

English

Let $F$ be a set. Let $d$ and $k$ be elements of $\Natural$. Then the Hilbert polynomial of $d$ and $k$ is a polynomial of $F$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (d !)}{\operatorname{comp} (\mathrm{ascPochhammer} (F , d), \operatorname{X} - \operatorname{C} (k)+ 1)}$.

Mathlib.RingTheory.Polynomial.IntegralNormalization

Polynomial.integralNormalizationdefMathlib.RingTheory.Polynomial.IntegralNormalization, function or constant

Wording

the integral normalization of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the integral normalization of $p$ is a polynomial of $R$ defined as the sum of $p$ and the function that maps $i$ and $a$ to $\operatorname{monomial}$ applied to $i$ and $\iteMACRoG {(\EqtMACRoH {\operatorname{degree} (p)}{i})}{1}{(a \times \operatorname{leadingCoeff} (p)^ {(\operatorname{natDegree} (p)- 1 - i)})}$.

Mathlib.RingTheory.Polynomial.Opposites

Polynomial.opRingEquivdefMathlib.RingTheory.Polynomial.Opposites, function or constant

Wording

the opposite ring isomorphism of R (from the name)

English

Let $R$ be a set. Then the opposite ring isomorphism of $R$ is a ring isomorphism of the set of multiplicative opposites of the set of polynomials of $R$ and the set of polynomials of the set of multiplicative opposites of $R$ defined as the composition of the composition of $\operatorname{op}$ applied to the finitely supported function isomorphism of $R$ and the composition of the opposite and the map domain ring isomorphism of the set of multiplicative opposites of $R$ and the inverse of the opposite additive equivalence and the inverse of the finitely supported function isomorphism of the set of multiplicative opposites of $R$.

Mathlib.RingTheory.Polynomial.Pochhammer

ascPochhammerdefMathlib.RingTheory.Polynomial.Pochhammer, function or constant

Wording

no wording

English

Let $S$ be a set. Let $x_{1}$ be a natural number. Then $\mathrm{ascPochhammer}$ applied to $S$ and $x_{1}$ is a polynomial of $S$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{ascPochhammer\_\_\_f}$ applied to $S$.

descPochhammerdefMathlib.RingTheory.Polynomial.Pochhammer, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be a natural number. Then $\mathrm{descPochhammer}$ applied to $R$ and $x_{1}$ is a polynomial of $R$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{descPochhammer\_\_\_f}$ applied to $R$.

Mathlib.RingTheory.Polynomial.Quotient

Ideal.polynomialQuotientEquivQuotientPolynomialdefMathlib.RingTheory.Polynomial.Quotient, function or constant

Wording

the polynomial quotient equivalence quotient polynomial of I (from the name)

English

Let $I$ be an ideal of $R$. Then the polynomial quotient equivalence quotient polynomial of $I$ is a ring isomorphism of the set of polynomials of the set of quotients of $R$ and $I$ and the set of quotients of the set of polynomials of $R$ and the map of $\operatorname{C}$ and $I$.

MvPolynomial.quotientEquivQuotientMvPolynomialdefMathlib.RingTheory.Polynomial.Quotient, function or constant

Wording

the quotient equivalence quotient multivariate polynomial of I (from the name)

English

Let $I$ be an ideal of $R$. Then the quotient equivalence quotient multivariate polynomial of $I$ is an algebra isomorphism of the set of multivariate polynomials of $x$ and the set of quotients of $R$ and $I$ and the set of quotients of the set of multivariate polynomials of $x$ and $R$ and the map of $\operatorname{C}$ and $I$.

Polynomial.quotientSpanCXSubCAlgEquivdefMathlib.RingTheory.Polynomial.Quotient, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $R$. Then $\operatorname{quotientSpanCXSubCAlgEquiv}$ applied to $x_{1}$ and $y$ is an algebra isomorphism of the set of quotients of the set of polynomials of $R$ and the span of $\operatorname{insert}$ applied to $\operatorname{C}$ applied to $x_{1}$ and $\operatorname{singleton}$ applied to $\operatorname{X} - \operatorname{C} (y)$ and the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $x_{1}$.

Polynomial.quotientSpanCXSubCXSubCAlgEquivdefMathlib.RingTheory.Polynomial.Quotient, function or constant

Wording

no wording

English

$\operatorname{quotientSpanCXSubCXSubCAlgEquiv}$ is an algebra isomorphism of 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{X} - \operatorname{C} (x_{1})$ and $\operatorname{singleton}$ applied to $\operatorname{X} - \operatorname{C} (y)$ and $R$ defined as the composition of $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{quotientSpanCXSubCAlgEquiv}$ applied to $\operatorname{X} - \operatorname{C} (x_{1})$ and $y$ and the quotient span difference algebra isomorphism of $x_{1}$.

Polynomial.quotientSpanXSubCAlgEquivdefMathlib.RingTheory.Polynomial.Quotient, function or constant

Wording

the quotient span difference algebra isomorphism of x1 (from the name)

English

Let $x_{1}$ be an element of $R$. Then the quotient span difference algebra isomorphism of $x_{1}$ is an algebra isomorphism of the set of quotients of the set of polynomials of $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{X} - \operatorname{C} (x_{1})$ and $R$.

Mathlib.RingTheory.Polynomial.Resultant.Basic

Polynomial.adjSylvesterdefMathlib.RingTheory.Polynomial.Resultant.Basic, function or constant

Wording

no wording

English

Let $f$ and $g$ be polynomials of $R$. Then $\operatorname{adjSylvester}$ applied to $f$ and $g$ is a linear map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m + n)}{x_{1}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{3}})}$ defined as $\operatorname{toLin}$ applied to the basis of $R$ and $m + n$, the reindexing of the product of the basis of $R$ and $m$ and the basis of $R$ and $n$ and the finite sum finite equivalence and the adjugate matrix of $\operatorname{sylvester}$ applied to $f$, $g$, $m$ and $n$.

Polynomial.discrdefMathlib.RingTheory.Polynomial.Resultant.Basic, function or constant

Wording

the discriminant of f (from the docstring)

English

Let $f$ be a polynomial of $R$. Then the discriminant of $f$ is an element of $R$ defined as the product of the determinant of $\operatorname{sylvesterDeriv}$ applied to $f$ and the exponentiation of $\operatorname{neg}$ applied to $1$ to the quotient of the product of the natural degree of $f$ and the difference between the natural degree of $f$ and $1$ and $2$.

Polynomial.resultantdefMathlib.RingTheory.Polynomial.Resultant.Basic, function or constant

Wording

the resultant of m and n (from the name)

English

Let $f$ and $g$ be polynomials of $R$. Let $m$ be an element of $\mathrm{optParam}$ applied to $\Natural$ and the natural degree of $f$. Let $n$ be an element of $\mathrm{optParam}$ applied to $\Natural$ and the natural degree of $g$. Then the resultant of $m$ and $n$ is an element of $R$ defined as the determinant of $\operatorname{sylvester}$ applied to $f$, $g$, $m$ and $n$.

Polynomial.sylvesterdefMathlib.RingTheory.Polynomial.Resultant.Basic, function or constant

Wording

no wording

English

Let $f$ and $g$ be polynomials of $R$. Let $m$ and $n$ be natural numbers. Then there is a matrix of $\mathrm{Fin}$ applied to $m + n$ and $R$. Proof. Let $f$ be arbitrary. Let $g$ be arbitrary. Let $m$ be arbitrary. Let $n$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. Let $x_{1}$ be arbitrary. By x1. By Fin__val. By x1. By Fin__val. By n. By plus. By Set__Icc. By i1. By Fin__val. By Membership__mem. By g. By i1. By Fin__val. By x1. By Fin__val. By minus. By Polynomial__coeff__app. By 0. By ite. Let $x_{2}$ be arbitrary. By x2. By Fin__val. By x2. By Fin__val. By m. By plus. By Set__Icc. By i1. By Fin__val. By Membership__mem. By f. By i1. By Fin__val. By x2. By Fin__val. By minus. By Polynomial__coeff__app. By 0. By ite. By j1. By Fin__addCases. By Matrix__of__app.

Polynomial.sylvesterDerivdefMathlib.RingTheory.Polynomial.Resultant.Basic, function or constant

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then there is a matrix of $\mathrm{Fin}$ applied to the sum of the difference between the natural degree of $f$ and $1$ and the natural degree of $f$ and $R$.

Polynomial.sylvesterMapdefMathlib.RingTheory.Polynomial.Resultant.Basic, function or constant

Wording

no wording

English

Let $f$ and $g$ be polynomials of $R$ such that the natural degree of $f$ is less than or equal to $m$ and the natural degree of $g$ is less than or equal to $n$. Then $\operatorname{sylvesterMap}$ applied to $f$, $g$, $\mathrm{hf}$ and $\mathrm{hg}$ is a linear map of $\mathrm{Prod}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , n)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (R , m + n)}{x_{3}})}$.

Mathlib.RingTheory.Polynomial.ScaleRoots

Polynomial.scaleRootsdefMathlib.RingTheory.Polynomial.ScaleRoots, function or constant

Wording

the polynomial with root of p and s (from the docstring)

English

Let $p$ be a polynomial of $R$. Let $s$ be an element of $R$. Then the polynomial with root of $p$ and $s$ is a polynomial of $R$ defined as $\FinsetSum {\operatorname{support} (p)}{i}{\operatorname{monomial} (i , \operatorname{coeff} (p , i)\times s ^ {(\operatorname{natDegree} (p)- i)})}$.

Mathlib.RingTheory.Polynomial.SeparableDegree

Polynomial.HasSeparableContractiondefMathlib.RingTheory.Polynomial.SeparableDegree, predicate

Wording

no wording

English

Let $q$ be a natural number. Let $f$ be a polynomial of $F$. Then $\operatorname{HasSeparableContraction}$ holds for $q$ and $f$, if there exists a polynomial $g$ of $F$, such that $\operatorname{IsSeparableContraction}$ holds for $q$, $f$ and $g$.

Polynomial.HasSeparableContraction.contractiondefMathlib.RingTheory.Polynomial.SeparableDegree, function or constant

Wording

the contraction of hf (from the name)

English

Assume that $\operatorname{HasSeparableContraction}$ holds for $q$ and $f$. Then the contraction of $\mathrm{hf}$ is a polynomial of $F$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$.

Polynomial.HasSeparableContraction.degreedefMathlib.RingTheory.Polynomial.SeparableDegree, function or constant

Wording

the separable degree of hf (from the docstring)

English

Assume that $\operatorname{HasSeparableContraction}$ holds for $q$ and $f$. Then the separable degree of $\mathrm{hf}$ is a natural number defined as the natural degree of the contraction of $\mathrm{hf}$.

Polynomial.IsSeparableContractiondefMathlib.RingTheory.Polynomial.SeparableDegree, predicate

Wording

no wording

English

Let $q$ be a natural number. Let $f$ and $g$ be polynomials of $F$. Then $\operatorname{IsSeparableContraction}$ holds for $q$, $f$ and $g$, if $g$ is separable and there exists a natural number $m$ such that $\EqtMACRoH {\operatorname{expand} (F , q ^ {m}, g)}{f}$.

Mathlib.RingTheory.Polynomial.ShiftedLegendre

Polynomial.shiftedLegendredefMathlib.RingTheory.Polynomial.ShiftedLegendre, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{shiftedLegendre}$ applied to $n$ is a polynomial of $\Integer$ defined as $\FinsetSum {\FinsetrangeMACRoN {(n + 1)}}{k}{(\operatorname{C} (\operatorname{neg} (1)^ {k}\times \operatorname{choose} (n , k)\times \operatorname{choose} (n + k , n))\times \operatorname{X} ^ {k})}$.

Mathlib.RingTheory.Polynomial.Subring

Polynomial.ofSubringdefMathlib.RingTheory.Polynomial.Subring, function or constant

Wording

the polynomial of T and p (from the name)

English

Let $T$ be a subring of $R$. Let $p$ be a polynomial of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {T}{x_{1}})}$. Then the polynomial of $T$ and $p$ is a polynomial of $R$ defined as $\FinsetSum {\operatorname{support} (p)}{i}{\operatorname{monomial} (i , \operatorname{coeff} (p , i))}$.

Polynomial.toSubringdefMathlib.RingTheory.Polynomial.Subring, function or constant

Wording

the subring of p and T (from the name)

English

Let $p$ be a polynomial of $R$. Let $T$ be a subring of $R$ such that $\operatorname{coeffs} (p)\leq T$. Then the subring of $p$ and $T$ is a polynomial of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {T}{x_{1}})}$ defined as $\FinsetSum {\operatorname{support} (p)}{i}{\operatorname{monomial} (i , \operatorname{coeff} (p , i))}$.

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

MvPolynomial.mapEquivMonicdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Let $n$ be a natural number. Then $\operatorname{mapEquivMonic}$ applied to $R$, $S$ and $n$ is an equivalence from the set of algebra homomorphisms of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ and $S$ to $\operatorname{MonicDegreeEq}$ applied to $S$ and $n$.

MvPolynomial.universalFactorizationMapdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the universal factorization map of m and k (from the name)

English

Let $R$ be a set. Let $n$, $m$ and $k$ be natural numbers such that $n = m + k$. Then the universal factorization map of $m$ and $k$ is an algebra homomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ and the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $m$ and $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $k$ and $R$ defined as $\operatorname{symm}$ applied to $\operatorname{mapEquivMonic}$ applied to $R$, the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $m$ and $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $k$ and $R$ and $n$ and the product of $\operatorname{mapEquivMonic}$ applied to $R$, the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $m$ and $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $k$ and $R$, $m$ and $\operatorname{includeLeft}$ and $\operatorname{mapEquivMonic}$ applied to $R$, the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $m$ and $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $k$ and $R$, $k$ and $\operatorname{includeRight}$.

MvPolynomial.universalFactorizationMapLiftEquivdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the universal factorization map lift equivalence of k and p (from the name)

English

Let $R$ and $S$ be sets. Let $n$, $m$ and $k$ be elements of $\Natural$ such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $S$ and $n$. Then the universal factorization map lift equivalence of $k$ and $p$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (f , \operatorname{universalFactorizationMap} (m , k))}{\operatorname{symm} (\operatorname{mapEquivMonic} (R , S , n), p)})})}{(\SubtypeSet {q}{(\EqtMACRoH {(\ProdfstMACRoZ {q}\times \ProdsndMACRoAA {q})}{p})})}$.

MvPolynomial.universalFactorizationMapPresentationdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the canonical presentation of R (from the docstring)

English

Let $R$ be a set. Let $n$, $m$ and $k$ be natural numbers such that $n = m + k$. Then the canonical presentation of $R$ is a submersive presentation of $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $m$ and $\mathrm{Fin}$ applied to $k$ and $\mathrm{Fin}$ applied to $n$.

Polynomial.MonicDegreeEq.freeMonicdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then $\operatorname{freeMonic}$ applied to $R$ and $n$ is an element of $\operatorname{MonicDegreeEq}$ applied to the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ and $n$ defined as $\operatorname{freeMonic}$ applied to $R$ and $n$.

Polynomial.UniversalCoprimeFactorizationRingdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, type

Wording

universal coprime factorization ring of hn and p (from the name)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then a universal coprime factorization ring of $\mathrm{hn}$ and $p$ is an element of the function that maps $m$, $k$, $\mathrm{hn}$ and $p$ to $\operatorname{Away}$ applied to $\operatorname{jacobian}$ applied to the presentation of $m$.

Polynomial.UniversalCoprimeFactorizationRing.factor₁defMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the factor of k and p (from the name)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the factor of $k$ and $p$ is an element of $\operatorname{MonicDegreeEq}$ applied to the set of universal coprime factorization rings of $\mathrm{hn}$ and $p$ and $m$ defined as the map of the factor of $k$ and $p$ and the algebra map of the set of universal factorization rings of $\mathrm{hn}$ and $p$ and the set of universal coprime factorization rings of $\mathrm{hn}$ and $p$.

Polynomial.UniversalCoprimeFactorizationRing.factor₂defMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the factor of k and p (from the name)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the factor of $k$ and $p$ is an element of $\operatorname{MonicDegreeEq}$ applied to the set of universal coprime factorization rings of $\mathrm{hn}$ and $p$ and $k$ defined as the map of the factor of $k$ and $p$ and the algebra map of the set of universal factorization rings of $\mathrm{hn}$ and $p$ and the set of universal coprime factorization rings of $\mathrm{hn}$ and $p$.

Polynomial.UniversalCoprimeFactorizationRing.homEquivdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the homomorphism equivalence of k and p (from the name)

English

Let $S$ be a set. Let $m$ and $k$ be elements of $\Natural$ such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the homomorphism equivalence of $k$ and $p$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (\operatorname{UniversalCoprimeFactorizationRing} (\mathrm{hn} , p), S)}{(\SubtypeSet {q}{\mathrm{and} (\EqtMACRoH {(\ProdfstMACRoZ {q}\times \ProdsndMACRoAA {q})}{\operatorname{map} (\operatorname{algebraMap} (R , S), p)}, \mathrm{IsCoprime} (\ProdfstMACRoZ {q}, \ProdsndMACRoAA {q}))})}$.

Polynomial.UniversalFactorizationRingdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, type

Wording

universal factorization ring of hn and p (from the name)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then a universal factorization ring of $\mathrm{hn}$ and $p$ is an element of the function that maps $m$, $k$, $\mathrm{hn}$ and $p$ to the set of tensor products of $R$ and the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $m$ and $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $k$ and $R$.

Polynomial.UniversalFactorizationRing.factor₁defMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the factor of k and p (from the name)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the factor of $k$ and $p$ is an element of $\operatorname{MonicDegreeEq}$ applied to the set of universal factorization rings of $\mathrm{hn}$ and $p$ and $m$ defined as the first element of $\operatorname{universalFactorizationMapLiftEquiv}$ applied to $R$, the set of universal factorization rings of $\mathrm{hn}$ and $p$, $n$, $m$, $k$, $\mathrm{hn}$, $\operatorname{monicDegreeEq}$ applied to $m$, $k$, $\mathrm{hn}$ and $p$ and $\operatorname{fromTensor}$ applied to $m$, $k$, $\mathrm{hn}$ and $p$.

Polynomial.UniversalFactorizationRing.factor₂defMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the factor of k and p (from the name)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the factor of $k$ and $p$ is an element of $\operatorname{MonicDegreeEq}$ applied to the set of universal factorization rings of $\mathrm{hn}$ and $p$ and $k$ defined as the second element of $\operatorname{universalFactorizationMapLiftEquiv}$ applied to $R$, the set of universal factorization rings of $\mathrm{hn}$ and $p$, $n$, $m$, $k$, $\mathrm{hn}$, $\operatorname{monicDegreeEq}$ applied to $m$, $k$, $\mathrm{hn}$ and $p$ and $\operatorname{fromTensor}$ applied to $m$, $k$, $\mathrm{hn}$ and $p$.

Polynomial.UniversalFactorizationRing.fromTensordefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

no wording

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then $\operatorname{fromTensor}$ applied to $m$, $k$, $\mathrm{hn}$ and $p$ is an algebra homomorphism of the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $m$ and $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $k$ and $R$ and the set of universal factorization rings of $\mathrm{hn}$ and $p$ defined as $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{includeRight}$.

Polynomial.UniversalFactorizationRing.homEquivdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the homomorphism equivalence of k and p (from the name)

English

Let $S$ be a set. Let $m$ and $k$ be elements of $\Natural$ such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the homomorphism equivalence of $k$ and $p$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (\operatorname{UniversalFactorizationRing} (\mathrm{hn} , p), S)}{(\SubtypeSet {q}{(\EqtMACRoH {(\ProdfstMACRoZ {q}\times \ProdsndMACRoAA {q})}{\operatorname{map} (\operatorname{algebraMap} (R , S), p)})})}$.

Polynomial.UniversalFactorizationRing.monicDegreeEqdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

no wording

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then $\operatorname{monicDegreeEq}$ applied to $m$, $k$, $\mathrm{hn}$ and $p$ is an element of $\operatorname{MonicDegreeEq}$ applied to the set of universal factorization rings of $\mathrm{hn}$ and $p$ and $n$ defined as the map of the algebra map of $R$ and the set of universal factorization rings of $\mathrm{hn}$ and $p$ and $p$.

Polynomial.UniversalFactorizationRing.presentationdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

the presentation of m (from the docstring)

English

Let $m$ and $k$ be natural numbers such that $n = m + k$. Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Then the presentation of $m$ is a submersive presentation of $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $m$ and $\mathrm{Fin}$ applied to $k$ and $\mathrm{Fin}$ applied to $n$ defined as the base change of $R$ and the canonical presentation of $R$.

Polynomial.freeMonicdefMathlib.RingTheory.Polynomial.UniversalFactorizationRing, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then $\operatorname{freeMonic}$ applied to $R$ and $n$ is a polynomial of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ defined as $\operatorname{X} ^ {n}+ \FinsetSum {\FinsetunivMACRoAC}{i}{(\operatorname{C} (\operatorname{X} (i))\times \operatorname{X} ^ {\operatorname{val} (i)})}$.

Mathlib.RingTheory.Polynomial.Wronskian

Polynomial.wronskiandefMathlib.RingTheory.Polynomial.Wronskian, function or constant

Wording

no wording

English

Let $a$ and $b$ be polynomials of $R$. Then $\operatorname{wronskian}$ applied to $a$ and $b$ is a polynomial of $R$ defined as $a \times \operatorname{derivative} (b)- \operatorname{derivative} (a)\times b$.

Polynomial.wronskianBilindefMathlib.RingTheory.Polynomial.Wronskian, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{wronskianBilin}$ applied to $R$ is a linear map of the set of polynomials of $R$ and the set of linear maps of the set of polynomials of $R$ and the set of polynomials of $R$ defined as the difference between the complement of the product of $R$ and the set of polynomials of $R$ and the formal derivative of the polynomial and the composition of the product of $R$ and the set of polynomials of $R$ and the formal derivative of the polynomial.

Mathlib.RingTheory.PolynomialAlgebra

PolyEquivTensor.equivdefMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

the equivalence of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the equivalence of $R$ and $A$ is an equivalence from the set of tensor products of $A$ and the set of polynomials of $R$ to the set of polynomials of $A$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to the function algebra homomorphism of $R$ and $A$, $\operatorname{invFun}$, $\mathrm{PolyEquivTensor\_\_left\_inv}$ applied to $R$ and $A$ and $\mathrm{PolyEquivTensor\_\_right\_inv}$ applied to $R$ and $A$.

PolyEquivTensor.invFundefMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

the inverse function of p (from the name)

English

Let $R$ and $A$ be sets. Let $p$ be a polynomial of $A$. Then the inverse function of $p$ is a tensor product of $A$ and the set of polynomials of $R$ defined as the evaluation of $\operatorname{tmul}$ applied to $R$, $1$ and $\operatorname{X}$ and $p$.

PolyEquivTensor.toFunAlgHomdefMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

the function algebra homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the function algebra homomorphism of $R$ and $A$ is an algebra homomorphism of the set of tensor products of $A$ and the set of polynomials of $R$ and the set of polynomials of $A$ defined as the algebra homomorphism of $\operatorname{toFunLinear}$ applied to $R$ and $A$.

PolyEquivTensor.toFunBilineardefMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

the function bilinear of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the function bilinear of $R$ and $A$ is a linear map of $A$ and the set of linear maps of the set of polynomials of $R$ and the set of polynomials of $A$ defined as the span singleton of the linear map of the algebra evaluation of $\operatorname{X}$.

PolyEquivTensor.toFunLineardefMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{toFunLinear}$ applied to $R$ and $A$ is a linear map of the set of tensor products of $A$ and the set of polynomials of $R$ and the set of polynomials of $A$ defined as the lift of $\operatorname{restrictScalars}$ applied to $R$ and the function bilinear of $R$ and $A$.

polyEquivTensordefMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

the polynomial equivalence tensor of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the polynomial equivalence tensor of $R$ and $A$ is an algebra isomorphism of the set of polynomials of $A$ and the set of tensor products of $A$ and the set of polynomials of $R$.

polyEquivTensor'defMathlib.RingTheory.PolynomialAlgebra, function or constant

Wording

the polynomial equivalence tensor of R and A (from the name)

English

Mathlib.RingTheory.PolynomialLaw.Basic

PolynomialLawstructureMathlib.RingTheory.PolynomialLaw.Basic, type

Wording

polynomial law of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the polynomial laws of $M$ and $N$ are a basic type.

PolynomialLaw.adddefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the sum of f and g (from the name)

English

Let $f$ and $g$ be polynomial laws of $M$ and $N$. Then the sum of $f$ and $g$ is a polynomial law of $M$ and $N$.

PolynomialLaw.compdefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a polynomial law of $N$ and $P$. Let $f$ be a polynomial law of $M$ and $N$. Then the composition of $g$ and $f$ is a polynomial law of $M$ and $P$.

PolynomialLaw.grounddefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the ground of f and x5 (from the name)

English

Let $f$ be a polynomial law of $M$ and $N$. Let $x_{5}$ be an element of $M$. Then the ground of $f$ and $x_{5}$ is an element of $N$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{lid}$ applied to $R$ and $N$, $\operatorname{comp}$ applied to $\operatorname{toFun'}$ applied to $f$ and $\operatorname{coe}$ applied to the inverse of $\operatorname{lid}$ applied to $R$ and $M$ and $x_{5}$.

PolynomialLaw.iddefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the identity (from the docstring)

English

The identity is a polynomial law of $M$ and $M$.

PolynomialLaw.lgrounddefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

no wording

English

$\operatorname{lground}$ is a linear map of the set of polynomial laws of $M$ and $N$ and the set of functions from elements of $M$ to elements of $N$.

PolynomialLaw.liftsdefMathlib.RingTheory.PolynomialLaw.Basic, type

Wording

lift of M and S (from the name)

English

Let $R$, $M$ and $S$ be sets. Then a lift of $M$ and $S$ is an element of the function that maps $R$, $M$ and $S$ to $\Sigma$ applied to the function that maps $s$ to the set of tensor products of the set of multivariate polynomials of $\mathrm{Fin}$ applied to the cardinality of $s$ and $R$ and $M$.

PolynomialLaw.negdefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the negation of f (from the name)

English

Let $f$ be a polynomial law of $M$ and $N$. Then the negation of $f$ is a polynomial law of $M$ and $N$.

PolynomialLaw.smuldefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the scalar multiple of r and f (from the name)

English

Let $r$ be an element of $R$. Let $f$ be a polynomial law of $M$ and $N$. Then the scalar multiple of $r$ and $f$ is a polynomial law of $M$ and $N$.

PolynomialLaw.toFundefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the polynomial law of f and x7 (from the name)

English

Let $S$ be a set. Let $f$ be a polynomial law of $M$ and $N$. Let $x_{7}$ be a tensor product of $S$ and $M$. Then the polynomial law of $f$ and $x_{7}$ is a tensor product of $S$ and $N$ defined as $\operatorname{extend}$ applied to $\mathrm{PolynomialLaw\_\_\_u3c0\_}$, the auxiliary lift of $S$, the function that maps $x_{7}$ to $0$ and $x_{7}$.

PolynomialLaw.toFun'defMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the function of self and x7 (from the name)

English

Let $\mathrm{self}$ be a polynomial law of $M$ and $N$. Let $S$ be a set. Let $x_{7}$ be a tensor product of $S$ and $M$. Then the function of $\mathrm{self}$ and $x_{7}$ is a tensor product of $S$ and $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $S$ and $x_{7}$.

PolynomialLaw.toFunLifteddefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the auxiliary lift of S (from the docstring)

English

Let $S$ be a set. Let $f$ be a polynomial law of $M$ and $N$. Let $x_{7}$ be a lift of $M$ and $S$. Then the auxiliary lift of $S$ is a tensor product of $S$ and $N$.

PolynomialLaw.πdefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

the projection of x5 (from the name)

English

Let $R$, $M$ and $S$ be sets. Let $x_{5}$ be a lift of $M$ and $S$. Then the projection of $x_{5}$ is a tensor product of $S$ and $M$.

PolynomialLaw.φdefMathlib.RingTheory.PolynomialLaw.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $s$ be a finite set of $S$. Then $\mathrm{PolynomialLaw\_\_\_u3c6\_}$ applied to $R$ and $s$ is an algebra homomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to the cardinality of $s$ and $R$ and $S$ defined as the algebra evaluation of the function that maps $n$ to $\operatorname{symm}$ applied to $\operatorname{equivFin}$ applied to $s$ and $n$.

Mathlib.RingTheory.PowerBasis

Module.Basis.PowerBasisdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the power basis of B and e (from the name)

English

Let $B$ be a basis of $R$ and $S$. Let $e$ be an equivalence from $x_{3}$ to $\mathrm{Fin}$ applied to the cardinality of $x_{3}$ such that for all elements $i$ of $x_{3}$, $\EqtMACRoH {B (i)}{x_{5} ^ {\operatorname{val} (e (i))}}$. Then the power basis of $B$ and $e$ is a power basis of $R$ and $S$.

PowerBasisstructureMathlib.RingTheory.PowerBasis, type

Wording

power basis of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the power bases of $R$ and $S$ are a basic type.

PowerBasis.basisdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the basis of self (from the name)

English

Let $\mathrm{self}$ be a power basis of $R$ and $S$. Then the basis of $\mathrm{self}$ is a basis of $R$ and $S$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

PowerBasis.dimdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the dimension of self (from the name)

English

Let $\mathrm{self}$ be a power basis of $R$ and $S$. Then the dimension of $\mathrm{self}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

PowerBasis.equivOfMinpolydefMathlib.RingTheory.PowerBasis, function or constant

Wording

the equivalence of pb and h (from the name)

English

Let $\mathrm{pb}$ be a power basis of $A$ and $S$. Let $\mathrm{pb'}$ be a power basis of $A$ and $\mathrm{S'}$ such that the minimal polynomial of $A$ and the generator of $\mathrm{pb}$ is equal to the minimal polynomial of $A$ and the generator of $\mathrm{pb'}$. Then the equivalence of $\mathrm{pb}$ and $\mathrm{pb'}$ is an algebra isomorphism of $S$ and $\mathrm{S'}$.

PowerBasis.equivOfRootdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the equivalence of pb and h (from the name)

English

Let $\mathrm{pb}$ be a power basis of $A$ and $S$. Let $\mathrm{pb'}$ be a power basis of $A$ and $\mathrm{S'}$ such that $\operatorname{aeval}$ applied to the generator of $\mathrm{pb}$ and the minimal polynomial of $A$ and the generator of $\mathrm{pb'}$ is equal to $0$ and $\operatorname{aeval}$ applied to the generator of $\mathrm{pb'}$ and the minimal polynomial of $A$ and the generator of $\mathrm{pb}$ is equal to $0$. Then the equivalence of $\mathrm{pb}$ and $\mathrm{pb'}$ is an algebra isomorphism of $S$ and $\mathrm{S'}$.

PowerBasis.gendefMathlib.RingTheory.PowerBasis, function or constant

Wording

the generator of self (from the name)

English

Let $\mathrm{self}$ be a power basis of $R$ and $S$. Then the generator of $\mathrm{self}$ is an element of $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

PowerBasis.liftdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the lift of pb and y (from the name)

English

Let $\mathrm{pb}$ be a power basis of $A$ and $S$. Let $y$ be an element of $\mathrm{S'}$ such that $\operatorname{aeval}$ applied to $y$ and the minimal polynomial of $A$ and the generator of $\mathrm{pb}$ is equal to $0$. Then the lift of $\mathrm{pb}$ and $y$ is an algebra homomorphism of $S$ and $\mathrm{S'}$.

PowerBasis.liftEquivdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the lift equivalence of pb (from the name)

English

Let $\mathrm{pb}$ be a power basis of $A$ and $S$. Then the lift equivalence of $\mathrm{pb}$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (S , \mathrm{S'})}{(\SubtypeSet {y}{(\EqtMACRoH {\operatorname{aeval} (y , \mathrm{minpoly} (A , \operatorname{gen} (\mathrm{pb})))}{0})})}$.

PowerBasis.liftEquiv'defMathlib.RingTheory.PowerBasis, function or constant

Wording

the lift equivalence of pb (from the name)

English

Let $\mathrm{pb}$ be a power basis of $A$ and $S$. Then the lift equivalence of $\mathrm{pb}$ is an element of $\EquivMACRoAE {\mathrm{AlgHom} (S , B)}{(\SubtypeSet {y}{(\MembershipmemMACRoT {\operatorname{aroots} (\mathrm{minpoly} (A , \operatorname{gen} (\mathrm{pb})), B)}{y})})}$.

PowerBasis.mapdefMathlib.RingTheory.PowerBasis, function or constant

Wording

the map of pb and e (from the name)

English

Let $\mathrm{pb}$ be a power basis of $R$ and $S$. Let $e$ be an algebra isomorphism of $S$ and $\mathrm{S'}$. Then the map of $\mathrm{pb}$ and $e$ is a power basis of $R$ and $\mathrm{S'}$.

PowerBasis.minpolyGendefMathlib.RingTheory.PowerBasis, function or constant

Wording

the minimal polynomial generator of pb (from the name)

English

Let $\mathrm{pb}$ be a power basis of $A$ and $S$. Then the minimal polynomial generator of $\mathrm{pb}$ is a polynomial of $A$ defined as $\operatorname{X} ^ {\operatorname{dim} (\mathrm{pb})}- \FinsetSum {\FinsetunivMACRoAC}{i}{(\operatorname{C} (\operatorname{coe} (\operatorname{repr} (\operatorname{basis} (\mathrm{pb})), \operatorname{gen} (\mathrm{pb})^ {\operatorname{dim} (\mathrm{pb})}, i))\times \operatorname{X} ^ {\operatorname{val} (i)})}$.

Mathlib.RingTheory.PowerSeries.Basic

Polynomial.coeToPowerSeries.algHomdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the algebra homomorphism of A (from the name)

English

Let $A$ be a set. Then the algebra homomorphism of $A$ is an algebra homomorphism of the set of polynomials of $R$ and the set of power series of $A$.

Polynomial.coeToPowerSeries.ringHomdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the ring homomorphism (from the name)

English

The ring homomorphism is a ring homomorphism of the set of polynomials of $R$ and the set of power series of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toPowerSeries}$ and $\mathrm{Polynomial\_\_coe\_one}$ and $\mathrm{Polynomial\_\_coe\_mul}$, $\mathrm{Polynomial\_\_coe\_zero}$ and $\mathrm{Polynomial\_\_coe\_add}$.

Polynomial.toPowerSeriesdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the power series of x1 (from the name)

English

Let $x_{1}$ be a polynomial of $R$. Then the power series of $x_{1}$ is a power series of $R$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{coeff}$ applied to $x_{1}$ and $n$.

PowerSeriesdefMathlib.RingTheory.PowerSeries.Basic, type

Wording

power series of R (from the name)

English

Let $R$ be a set. Then a power series of $R$ is an element of the function that maps $R$ to the set of multivariate power series of $\mathrm{Unit}$ and $R$.

PowerSeries.CdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

no wording

English

$\operatorname{C}$ is a ring homomorphism of $R$ and the set of power series of $R$ defined as $\operatorname{C}$.

PowerSeries.XdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

no wording

English

There is a power series of $R$. Proof. By Unit__unit. By MvPowerSeries__X.

PowerSeries.coeffdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the coefficient of n (from the name)

English

Let $n$ be a natural number. Then the coefficient of $n$ is a linear map of the set of power series of $R$ and $R$ defined as the coefficient of $\FinsuppsingleMACRoS {\operatorname{unit}}{n}$.

PowerSeries.constantCoeffdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the constant coefficient (from the docstring)

English

The constant coefficient is a ring homomorphism of the set of power series of $R$ and $R$ defined as the constant coefficient.

PowerSeries.evalNegHomdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the evaluation negation homomorphism (from the name)

English

The evaluation negation homomorphism is a ring homomorphism of the set of power series of $A$ and the set of power series of $A$ defined as $\operatorname{rescale}$ applied to $\operatorname{neg}$ applied to $1$.

PowerSeries.mapdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the map between formal power series induced by a map on the coefficients of f (from the docstring)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map between formal power series induced by a map on the coefficients of $f$ is a ring homomorphism of the set of power series of $R$ and the set of power series of $S$ defined as the map of $f$.

PowerSeries.mapAlgHomdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the map algebra homomorphism of x5 (from the name)

English

Let $x_{5}$ be an algebra homomorphism of $A$ and $B$. Then the map algebra homomorphism of $x_{5}$ is an algebra homomorphism of the set of power series of $A$ and the set of power series of $B$ defined as the map algebra homomorphism of $x_{5}$.

PowerSeries.mkdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from natural numbers to elements of $R$. Then there is a power series of $R$. Proof. Let $f$ be arbitrary. Let $s$ be arbitrary. By Unit__unit. By s. By f.

PowerSeries.monomialdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the monomial of n (from the name)

English

Let $n$ be a natural number. Then the monomial of $n$ is a linear map of $R$ and the set of power series of $R$ defined as the monomial of $\FinsuppsingleMACRoS {\operatorname{unit}}{n}$.

PowerSeries.rescaledefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $R$. Then $\operatorname{rescale}$ applied to $a$ is a ring homomorphism of the set of power series of $R$ and the set of power series of $R$.

PowerSeries.toSubringdefMathlib.RingTheory.PowerSeries.Basic, function or constant

Wording

the subring of p and T (from the name)

English

Let $p$ be a power series of $R$. Let $T$ be a subring of $R$ such that for all natural numbers $n$, $\MembershipmemMACRoT {T}{\operatorname{coeff} (n , p)}$. Then the subring of $p$ and $T$ is a power series of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {T}{x_{1}})}$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{coeff}$ applied to $n$ and $p$.

Mathlib.RingTheory.PowerSeries.Binomial

PowerSeries.binomialSeriesdefMathlib.RingTheory.PowerSeries.Binomial, function or constant

Wording

the binomial series of A and r (from the name)

English

Let $A$ be a set. Let $r$ be an element of $R$. Then the binomial series of $A$ and $r$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\HSMulhSMulMACRoAL {\operatorname{choose} (r , n)}{1}$.

Mathlib.RingTheory.PowerSeries.Catalan

PowerSeries.catalanSeriesdefMathlib.RingTheory.PowerSeries.Catalan, function or constant

Wording

the Catalan generating function (from the docstring)

English

The Catalan generating function is a power series of $\Natural$ defined as $\operatorname{mk}$ applied to $\mathrm{catalan}$.

Mathlib.RingTheory.PowerSeries.Derivative

PowerSeries.derivativedefMathlib.RingTheory.PowerSeries.Derivative, function or constant

Wording

the formal derivative (from the docstring)

English

The formal derivative is a derivation of the set of power series of $R$ and the set of power series of $R$ defined as $\operatorname{pderiv}$ applied to $\operatorname{unit}$.

Mathlib.RingTheory.PowerSeries.Evaluation

PowerSeries.HasEvaldefMathlib.RingTheory.PowerSeries.Evaluation, predicate

Wording

a has evaluations (from the name)

English

generation took over the time limit

PowerSeries.aevaldefMathlib.RingTheory.PowerSeries.Evaluation, function or constant

Wording

the algebra evaluation of ha (from the name)

English

Assume that $a$ has evaluations. Then the algebra evaluation of $\mathrm{ha}$ is an algebra homomorphism of the set of power series of $R$ and $S$.

PowerSeries.eval₂defMathlib.RingTheory.PowerSeries.Evaluation, function or constant

Wording

the evaluation of a and x5 (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $a$ be an element of $S$. Let $x_{5}$ be a power series of $R$. Then the evaluation of $a$ and $x_{5}$ is an element of $S$ defined as the evaluation of the function that maps $x_{5}$ to $a$ and $x_{5}$.

PowerSeries.eval₂HomdefMathlib.RingTheory.PowerSeries.Evaluation, function or constant

Wording

the evaluation homomorphism of h7 and ha (from the name)

English

Assume that $\operatorname{coe}$ applied to $x_{2}$ is continuous. Assume that $a$ has evaluations. Then the evaluation homomorphism of $h_{7}$ and $\mathrm{ha}$ is a ring homomorphism of the set of power series of $R$ and $S$.

PowerSeries.hasEvalIdealdefMathlib.RingTheory.PowerSeries.Evaluation, function or constant

Wording

no wording

English

$\operatorname{hasEvalIdeal}$ is an ideal of $S$.

Mathlib.RingTheory.PowerSeries.Exp

PowerSeries.expdefMathlib.RingTheory.PowerSeries.Exp, function or constant

Wording

the exponential of A (from the name)

English

Let $A$ be a set. Then the exponential of $A$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{algebraMap}$ applied to $\Rational$, $A$ and $\frac{ 1}{n !}$.

Mathlib.RingTheory.PowerSeries.Expand

PowerSeries.expanddefMathlib.RingTheory.PowerSeries.Expand, function or constant

Wording

the expand of p and hp (from the name)

English

Let $p$ be a natural number such that $p \neq 0$. Then the expand of $p$ and $\mathrm{hp}$ is an algebra homomorphism of the set of power series of $R$ and the set of power series of $R$ defined as the expand of $p$ and $\mathrm{hp}$.

Mathlib.RingTheory.PowerSeries.GaussNorm

PowerSeries.HasGaussNormdefMathlib.RingTheory.PowerSeries.GaussNorm, predicate

Wording

no wording

English

Let $v$ be a function from elements of $R$ to real numbers. Let $c$ be a real number. Let $f$ be a power series of $R$. Then $\operatorname{HasGaussNorm}$ holds for $v$, $c$ and $f$, if the range of the function that maps $t$ to $v (\operatorname{coeff} (t , f))\times c ^ {t}$ is bounded above.

PowerSeries.gaussNormdefMathlib.RingTheory.PowerSeries.GaussNorm, function or constant

Wording

the Gauss norm of c and f (from the name)

English

Let $v$ be a function from elements of $R$ to real numbers. Let $c$ be a real number. Let $f$ be a power series of $R$. Then the Gauss norm of $c$ and $f$ is a real number defined as the Gauss norm of the function that maps $x_{1}$ to $c$ and $f$.

Mathlib.RingTheory.PowerSeries.Inverse

PowerSeries.Inv_divided_by_X_pow_orderdefMathlib.RingTheory.PowerSeries.Inverse, function or constant

Wording

the inverse divided by power order of hf (from the name)

English

Assume that $f \neq 0$. Then the inverse divided by power order of $\mathrm{hf}$ is a power series of $k$ defined as the inverse of the quotient power order of $f$ and the first unit coefficient of $\mathrm{hf}$.

PowerSeries.Unit_of_divided_by_X_pow_orderdefMathlib.RingTheory.PowerSeries.Inverse, function or constant

Wording

the unit of f (from the name)

English

Let $f$ be a power series of $k$. Then the unit of $f$ is a unit of the set of power series of $k$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {f}{0}$, the function that maps $\mathrm{hf}$ to $1$ and the function that maps $\mathrm{hf1}$ to $\operatorname{mk}$ applied to the quotient power order of $f$, the inverse divided by power order of $\mathrm{hf1}$, $\mathrm{PowerSeries\_\_Inv\_divided\_by\_X\_pow\_order\_rightInv}$ applied to $\mathrm{hf1}$ and $\mathrm{PowerSeries\_\_Inv\_divided\_by\_X\_pow\_order\_leftInv}$ applied to $\mathrm{hf1}$.

PowerSeries.firstUnitCoeffdefMathlib.RingTheory.PowerSeries.Inverse, function or constant

Wording

the first unit coefficient of hf (from the name)

English

Assume that $f \neq 0$. Then the first unit coefficient of $\mathrm{hf}$ is a unit of $k$ defined as the unit of $\operatorname{constantCoeff}$ applied to the quotient power order of $f$.

PowerSeries.invdefMathlib.RingTheory.PowerSeries.Inverse, function or constant

Wording

the inverse of x1 (from the name)

English

Let $x_{1}$ be a power series of $k$. Then the inverse of $x_{1}$ is a power series of $k$ defined as the inverse of $x_{1}$.

PowerSeries.invOfUnitdefMathlib.RingTheory.PowerSeries.Inverse, function or constant

Wording

the inverse of x1 and u (from the name)

English

Let $x_{1}$ be a power series of $R$. Let $u$ be a unit of $R$. Then the inverse of $x_{1}$ and $u$ is a power series of $R$ defined as the inverse of $x_{1}$ and $u$.

PowerSeries.residueFieldOfPowerSeriesdefMathlib.RingTheory.PowerSeries.Inverse, function or constant

Wording

the residue field (from the name)

English

The residue field is a ring isomorphism of the set of residue fields of the set of power series of $k$ and $k$.

Mathlib.RingTheory.PowerSeries.Log

PowerSeries.logdefMathlib.RingTheory.PowerSeries.Log, function or constant

Wording

the logarithm of A (from the name)

English

Let $A$ be a set. Then the logarithm of $A$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\iteMACRoG {\mathrm{Eq} (n , 0)}{0}{\operatorname{algebraMap} (\Rational , A , \frac{ \operatorname{neg} (1)^ {(n + 1)}}{n})}$.

PowerSeries.logOfdefMathlib.RingTheory.PowerSeries.Log, function or constant

Wording

the logarithm of f (from the name)

English

Let $f$ be a power series of $A$. Then the logarithm of $f$ is a power series of $A$ defined as the substitution of $f - 1$ and the logarithm of $A$.

Mathlib.RingTheory.PowerSeries.Order

PowerSeries.divXPowOrderdefMathlib.RingTheory.PowerSeries.Order, function or constant

Wording

the quotient power order of f (from the name)

English

Let $f$ be a power series of $R$. Then the quotient power order of $f$ is a power series of $R$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{coeff}$ applied to the sum of $n$ and the natural number of the order of $f$ and $f$.

PowerSeries.divXPowOrderHomdefMathlib.RingTheory.PowerSeries.Order, function or constant

Wording

the quotient power order homomorphism (from the name)

English

The quotient power order homomorphism is a monoid homomorphism of the set of power series of $R$ and the set of power series of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $g$ to the quotient power order of $g$ and $\mathrm{PowerSeries\_\_divXPowOrder\_one}$ and the function that maps $f$ and $g_{1}$ to $\mathrm{PowerSeries\_\_divXPowOrder\_mul}$.

PowerSeries.orderdefMathlib.RingTheory.PowerSeries.Order, function or constant

Wording

the order of x1 (from the docstring)

English

Let $x_{1}$ be a power series of $R$. Then the order of $x_{1}$ is a natural number.

PowerSeries.orderHomdefMathlib.RingTheory.PowerSeries.Order, function or constant

Wording

the order homomorphism (from the name)

English

The order homomorphism is a monoid homomorphism of the set of power series of $R$ and the set of multiplicatives of the set of natural numbers defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $g$ to $\operatorname{ofAdd}$ applied to the order of $g$ and $\mathrm{PowerSeries\_\_order\_one}$ and $\mathrm{PowerSeries\_\_order\_mul}$.

Mathlib.RingTheory.PowerSeries.Restricted

PowerSeries.IsRestricteddefMathlib.RingTheory.PowerSeries.Restricted, predicate

Wording

c is restricted with respect to f (from the name)

English

Let $c$ be a real number. Let $f$ be a power series of $R$. Then $c$ is restricted with respect to $f$, if $f$ is restricted with respect to the function that maps $x_{1}$ to $c$.

PowerSeries.IsRestricted.addSubgroupdefMathlib.RingTheory.PowerSeries.Restricted, function or constant

Wording

the additive subgroup of c (from the name)

English

Let $c$ be a real number. Then the additive subgroup of $c$ is an additive subgroup of the set of power series of $R$ defined as the additive subgroup of the function that maps $x_{1}$ to $c$.

PowerSeries.IsRestricted.subringdefMathlib.RingTheory.PowerSeries.Restricted, function or constant

Wording

the subring of c (from the name)

English

Let $c$ be a real number. Then the subring of $c$ is a subring of the set of power series of $R$ defined as the subring of the function that maps $x_{1}$ to $c$.

Mathlib.RingTheory.PowerSeries.Schroder

PowerSeries.largeSchroderSeriesdefMathlib.RingTheory.PowerSeries.Schroder, function or constant

Wording

the large Schroder series (from the name)

English

The large Schroder series is a power series of $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{largeSchroder}$.

Mathlib.RingTheory.PowerSeries.Substitution

PowerSeries.HasSubstdefMathlib.RingTheory.PowerSeries.Substitution, predicate

Wording

a has substitutions (from the name)

English

Let $a$ be a multivariate power series of $x$ and $S$. Then $a$ has substitutions, if $\operatorname{constantCoeff}$ applied to $a$ is nilpotent.

PowerSeries.HasSubst.idealdefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

the ideal (from the name)

English

The ideal is an ideal of the set of multivariate power series of $x$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the proposition that $\operatorname{HasSubst}$ and the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{add}$ and $\operatorname{zero}$ and $\operatorname{smul}$.

PowerSeries.rescaleAlgHomdefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Then $\operatorname{rescaleAlgHom}$ applied to $r$ is an algebra homomorphism of the set of power series of $R$ and the set of power series of $R$ defined as $\operatorname{rescaleAlgHom}$ applied to the function that maps $x_{1}$ to $r$.

PowerSeries.substdefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

the substitution of a and f (from the name)

English

Let $a$ be a multivariate power series of $x_{1}$ and $S$. Let $f$ be a power series of $R$. Then the substitution of $a$ and $f$ is a multivariate power series of $x_{1}$ and $S$ defined as the substitution of the function that maps $x_{4}$ to $a$ and $f$.

PowerSeries.substAlgHomdefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

the substitution algebra homomorphism of ha (from the name)

English

Assume that $a$ has substitutions. Then the substitution algebra homomorphism of $\mathrm{ha}$ is an algebra homomorphism of the set of power series of $R$ and the set of multivariate power series of $x_{1}$ and $S$ defined as the substitution algebra homomorphism of $\operatorname{const}$ applied to $\mathrm{ha}$.

PowerSeries.substInvdefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

the substitution inverse of P (from the name)

English

Let $P$ be a power series of $R$. Then the substitution inverse of $P$ is a power series of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{substInvFun}$ applied to $P$.

PowerSeries.substInvFundefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

the substitution inverse function of P and x2 (from the name)

English

Let $P$ be a power series of $R$. Let $x_{2}$ be a natural number. Then the substitution inverse function of $P$ and $x_{2}$ is an element of $R$.

PowerSeries.substInvOfIsUnitdefMathlib.RingTheory.PowerSeries.Substitution, function or constant

Wording

the substitution inverse of P and #2 (from the name)

English

Let $P$ be a power series of $R$ such that $\operatorname{coeff}$ applied to $1$ and $P$ is a unit. Then the substitution inverse of $P$ and $\mathrm{hP'}$ is a power series of $R$ defined as the substitution inverse of $P$.

Mathlib.RingTheory.PowerSeries.Trunc

PowerSeries.truncdefMathlib.RingTheory.PowerSeries.Trunc, function or constant

Wording

the truncation of n (from the name)

English

Let $n$ be a natural number. Then the truncation of $n$ is a linear map of the set of power series of $R$ and the set of polynomials of $R$.

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Polynomial.IsDistinguishedAt.algEquivQuotientdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the algebra isomorphism quotient of H (from the name)

English

Assume that $\operatorname{IsDistinguishedAt}$ holds for $g$ and $I$. Then the algebra isomorphism quotient of $H$ is an algebra isomorphism of the set of quotients of the set of polynomials of $A$ and the span of $\operatorname{singleton}$ applied to $g$ and the set of quotients of the set of power series of $A$ and the span of $\operatorname{singleton}$ applied to the power series of $g$.

PowerSeries.IsWeierstrassDivisiondefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, predicate

Wording

no wording

English

Let $f$, $g$ and $q$ be power series of $A$. Let $r$ be a polynomial of $A$. Then $\operatorname{IsWeierstrassDivision}$ holds for $f$, $g$, $q$ and $r$, if $\operatorname{IsWeierstrassDivisionAt}$ holds for $f$, $g$, $q$, $r$ and the maximal ideal of $A$.

PowerSeries.IsWeierstrassDivisionAtstructureMathlib.RingTheory.PowerSeries.WeierstrassPreparation, predicate

Wording

no wording

English

Let $f$, $g$ and $q$ be power series of $A$. Let $r$ be a polynomial of $A$. Let $I$ be an ideal of $A$. Then we can say that $\operatorname{IsWeierstrassDivisionAt}$ holds for $f$, $g$, $q$, $r$ and $I$.

PowerSeries.IsWeierstrassDivisordefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, predicate

Wording

g is a Weierstrass divisor (from the name)

English

Let $g$ be a power series of $A$. Then $g$ is a Weierstrass divisor, if $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and the maximal ideal of $A$.

PowerSeries.IsWeierstrassDivisorAtdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, predicate

Wording

no wording

English

Let $g$ be a power series of $A$. Let $I$ be an ideal of $A$. Then $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and $I$, if $\operatorname{coeff}$ applied to the natural number of the order of $\operatorname{map}$ applied to $\operatorname{mk}$ applied to $I$ and $g$ and $g$ is a unit.

PowerSeries.IsWeierstrassDivisorAt.divdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the quotient of H and f (from the name)

English

Assume that $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and $I$. Let $f$ be a power series of $A$. Then the quotient of $H$ and $f$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to the quotient coefficient of $f$ and $i$.

PowerSeries.IsWeierstrassDivisorAt.divCoeffdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the quotient coefficient of f and i (from the name)

English

Assume that $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and $I$. Let $f$ be a power series of $A$. Let $i$ be an element of $\Natural$. Then the quotient coefficient of $f$ and $i$ is an element of $\SubtypeSet {x_{1}}{\mathrm{forall} (\Natural , \lambda n . \mathrm{SModEq} (\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}, \operatorname{coeff} (i , \operatorname{seq} (f , n)), x_{1}))}$.

PowerSeries.IsWeierstrassDivisorAt.moddefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

no wording

English

Assume that $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and $I$. Let $f$ be a power series of $A$. Then $\operatorname{mod}$ applied to $H$ and $f$ is a polynomial of $A$ defined as $\operatorname{trunc}$ applied to the natural number of the order of $\operatorname{map}$ applied to $\operatorname{mk}$ applied to $I$ and $g$ and the difference between $f$ and the product of $g$ and the quotient of $H$ and $f$.

PowerSeries.IsWeierstrassDivisorAt.mod'defMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

no wording

English

Assume that $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and $I$. Then $\operatorname{mod'}$ applied to $H$ is a linear map of the set of quotients of the set of power series of $A$ and the span of $\operatorname{singleton}$ applied to $g$ and the set of polynomials of $A$.

PowerSeries.IsWeierstrassDivisorAt.seqdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the sequence of f and x1 (from the name)

English

Assume that $\operatorname{IsWeierstrassDivisorAt}$ holds for $g$ and $I$. Let $f$ be a power series of $A$. Let $x_{1}$ be a natural number. Then the sequence of $f$ and $x_{1}$ is a power series of $A$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{PowerSeries\_\_IsWeierstrassDivisorAt\_\_seq\_\_\_f}$ applied to $H$ and $f$.

PowerSeries.IsWeierstrassFactorizationdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, predicate

Wording

no wording

English

Let $g$ and $h$ be power series of $A$. Let $f$ be a polynomial of $A$. Then $\operatorname{IsWeierstrassFactorization}$ holds for $g$, $f$ and $h$, if $\operatorname{IsWeierstrassFactorizationAt}$ holds for $g$, $f$, $h$ and the maximal ideal of $A$.

PowerSeries.IsWeierstrassFactorizationAtstructureMathlib.RingTheory.PowerSeries.WeierstrassPreparation, predicate

Wording

no wording

English

Let $g$ and $h$ be power series of $A$. Let $f$ be a polynomial of $A$. Let $I$ be an ideal of $A$. Then we can say that $\operatorname{IsWeierstrassFactorizationAt}$ holds for $g$, $f$, $h$ and $I$.

PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotientdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the algebra isomorphism quotient of H (from the name)

English

Assume that $\operatorname{IsWeierstrassFactorizationAt}$ holds for $g$, $f$, $h$ and $I$. Then the algebra isomorphism quotient of $H$ is an algebra isomorphism of the set of quotients of the set of polynomials of $A$ and the span of $\operatorname{singleton}$ applied to $f$ and the set of quotients of the set of power series of $A$ and the span of $\operatorname{singleton}$ applied to $g$.

PowerSeries.algEquivQuotientWeierstrassDistinguisheddefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

no wording

English

Assume that $\operatorname{map}$ applied to the quotient map of $A$ and $g$ is distinct from $0$. Then $\operatorname{algEquivQuotientWeierstrassDistinguished}$ applied to $\mathrm{hg}$ is an algebra isomorphism of the set of quotients of the set of polynomials of $A$ and the span of $\operatorname{singleton}$ applied to $\operatorname{weierstrassDistinguished}$ applied to $g$ and $\mathrm{hg}$ and the set of quotients of the set of power series of $A$ and the span of $\operatorname{singleton}$ applied to $g$ defined as the algebra isomorphism quotient of $\mathrm{PowerSeries\_\_isWeierstrassFactorization\_weierstrassDistinguished\_weierstrassUnit}$ applied to $\mathrm{hg}$.

PowerSeries.weierstrassDistinguisheddefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

no wording

English

Let $g$ be a power series of $A$ such that $\operatorname{map}$ applied to the quotient map of $A$ and $g$ is distinct from $0$. Then $\operatorname{weierstrassDistinguished}$ applied to $g$ and $\mathrm{hg}$ is a polynomial of $A$ defined as $\operatorname{choose}$ applied to $\mathrm{PowerSeries\_\_exists\_isWeierstrassFactorization}$ applied to $\mathrm{hg}$.

PowerSeries.weierstrassDivdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the quotient of f and g (from the docstring)

English

Let $f$ and $g$ be power series of $A$. Then the quotient of $f$ and $g$ is a power series of $A$ defined as $\mathrm{dite}$ applied to the proposition that $\operatorname{map}$ applied to the quotient map of $A$ and $g$ is distinct from $0$, the function that maps $\mathrm{hg}$ to the quotient of $\mathrm{PowerSeries\_\_IsWeierstrassDivisor\_\_of\_map\_ne\_zero}$ applied to $\mathrm{hg}$ and $f$ and the function that maps $\mathrm{hg1}$ to $0$.

PowerSeries.weierstrassModdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

no wording

English

Let $f$ and $g$ be power series of $A$. Then $\operatorname{weierstrassMod}$ applied to $f$ and $g$ is a polynomial of $A$ defined as $\mathrm{dite}$ applied to the proposition that $\operatorname{map}$ applied to the quotient map of $A$ and $g$ is distinct from $0$, the function that maps $\mathrm{hg}$ to $\operatorname{mod}$ applied to $\mathrm{PowerSeries\_\_IsWeierstrassDivisor\_\_of\_map\_ne\_zero}$ applied to $\mathrm{hg}$ and $f$ and the function that maps $\mathrm{hg1}$ to $0$.

PowerSeries.weierstrassUnitdefMathlib.RingTheory.PowerSeries.WeierstrassPreparation, function or constant

Wording

the Weierstrass unit of g and hg (from the name)

English

Let $g$ be a power series of $A$ such that $\operatorname{map}$ applied to the quotient map of $A$ and $g$ is distinct from $0$. Then the Weierstrass unit of $g$ and $\mathrm{hg}$ is a power series of $A$.

Mathlib.RingTheory.PowerSeries.WellKnown

PowerSeries.cosdefMathlib.RingTheory.PowerSeries.WellKnown, function or constant

Wording

no wording

English

Let $A$ be a set. Then there is a power series of $A$. Proof. Let $A$ be arbitrary. Let $n$ be arbitrary. By n. By even. By Rat. By A. By 1. By Neg__neg. By n. By 2. By div. By pow. By n. By factorial. By div. By Algebra__algebraMap__app. By 0. By ite. By PowerSeries__mk.

PowerSeries.invOneSubPowdefMathlib.RingTheory.PowerSeries.WellKnown, function or constant

Wording

the inverse one difference power of S and x1 (from the name)

English

Let $S$ be a set. Let $x_{1}$ be a natural number. Then the inverse one difference power of $S$ and $x_{1}$ is a unit of the set of power series of $S$.

PowerSeries.invUnitsSubdefMathlib.RingTheory.PowerSeries.WellKnown, function or constant

Wording

the inverse unit difference of u (from the name)

English

Let $u$ be a unit of $R$. Then the inverse unit difference of $u$ is a power series of $R$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\mathrm{divp}$ applied to $1$ and $u ^ {(n + 1)}$.

PowerSeries.sindefMathlib.RingTheory.PowerSeries.WellKnown, function or constant

Wording

the sin of A (from the name)

English

Let $A$ be a set. Then the sin of $A$ is a power series of $A$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\iteMACRoG {\mathrm{even} (n)}{0}{\operatorname{algebraMap} (\Rational , A , \frac{ \operatorname{neg} (1)^ {\frac{ n}{2}}}{n !})}$.

Mathlib.RingTheory.PrincipalIdealDomain

Ideal.nonPrincipalsdefMathlib.RingTheory.PrincipalIdealDomain, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{nonPrincipals}$ applied to $R$ is an element of the power set of the set of ideals of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $I$ to the proposition that $I$ is not principal.

IsBezoutclassMathlib.RingTheory.PrincipalIdealDomain, predicate

Wording

R is a Bezout (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a Bezout.

IsBezout.gcddefMathlib.RingTheory.PrincipalIdealDomain, function or constant

Wording

the greatest common divisor of x1 and y (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Then the greatest common divisor of $x_{1}$ and $y$ is an element of $R$ defined as the generator of the span of $\operatorname{insert}$ applied to $x_{1}$ and $\operatorname{singleton}$ applied to $y$.

PrincipalIdealRing.factorsdefMathlib.RingTheory.PrincipalIdealDomain, function or constant

Wording

the factor of a (from the name)

English

Let $a$ be an element of $R$. Then the factor of $a$ is a multiset of $R$.

Mathlib.RingTheory.QuasiFinite.Basic

Algebra.QuasiFiniteclassMathlib.RingTheory.QuasiFinite.Basic, predicate

Wording

no wording

English

Let $R$ and $S$ be sets. Then we can say that $\operatorname{QuasiFinite}$ holds for $R$ and $S$.

Algebra.QuasiFiniteAtdefMathlib.RingTheory.QuasiFinite.Basic, predicate

Wording

no wording

English

Let $R$ be a set. Let $p$ be an ideal of $S$. Then $\operatorname{QuasiFiniteAt}$ holds for $R$ and $p$, if $\operatorname{QuasiFinite}$ holds for $R$ and $\operatorname{AtPrime}$ applied to $p$.

Mathlib.RingTheory.QuasiFinite.Weakly

Algebra.WeaklyQuasiFiniteAtdefMathlib.RingTheory.QuasiFinite.Weakly, predicate

Wording

no wording

English

Let $R$ be a set. Let $q$ be an ideal of $S$. Then $\operatorname{WeaklyQuasiFiniteAt}$ holds for $R$ and $q$, if $\operatorname{QuasiFiniteAt}$ holds for $R$ and the map of $\operatorname{mk}$ applied to the map of the algebra map of $R$ and $S$ and $\operatorname{under}$ applied to $R$ and $q$ and $q$.

Mathlib.RingTheory.QuotSMulTop

QuotSMulTopdefMathlib.RingTheory.QuotSMulTop, type

Wording

quotient multiplicative top of r and M (from the name)

English

Let $r$ be an element of $R$. Let $M$ be a set. Then a quotient multiplicative top of $r$ and $M$ is an element of the function that maps $r$ and $M$ to the set of quotients of $M$ and $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$.

QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTopdefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the algebra map tensor equivalence tensor quotient multiplicative top of r (from the name)

English

Let $r$ be an element of $R$. Let $M$ and $S$ be sets. Then the algebra map tensor equivalence tensor quotient multiplicative top of $r$ is a linear equivalence of the set of quotient multiplicative tops of $\operatorname{algebraMap}$ applied to $R$, $S$ and $r$ and the set of tensor products of $S$ and $M$ and the set of tensor products of $S$ and the set of quotient multiplicative tops of $r$ and $M$.

QuotSMulTop.congrdefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the congruence of r and e (from the name)

English

Let $r$ be an element of $R$. Let $e$ be a linear equivalence of $\mathrm{M'}$ and $\mathrm{M''}$. Then the congruence of $r$ and $e$ is a linear equivalence of the set of quotient multiplicative tops of $r$ and $\mathrm{M'}$ and the set of quotient multiplicative tops of $r$ and $\mathrm{M''}$.

QuotSMulTop.equivQuotTensordefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the equivalence quotient tensor of r and M (from the name)

English

Let $r$ be an element of $R$. Let $M$ be a set. Then the equivalence quotient tensor of $r$ and $M$ is a linear equivalence of the set of quotient multiplicative tops of $r$ and $M$ and the set of tensor products of the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $r$ and $M$.

QuotSMulTop.equivTensorQuotdefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the equivalence tensor quotient of r and M (from the name)

English

Let $r$ be an element of $R$. Let $M$ be a set. Then the equivalence tensor quotient of $r$ and $M$ is a linear equivalence of the set of quotient multiplicative tops of $r$ and $M$ and the set of tensor products of $M$ and the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $r$.

QuotSMulTop.mapdefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the map of r (from the name)

English

Let $r$ be an element of $R$. Then the map of $r$ is a linear map of the set of linear maps of $M$ and $\mathrm{M'}$ and the set of linear maps of the set of quotient multiplicative tops of $r$ and $M$ and the set of quotient multiplicative tops of $r$ and $\mathrm{M'}$.

QuotSMulTop.quotSMulTopTensorEquivQuotSMulTopdefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the quotient multiplicative top tensor equivalence quotient multiplicative top of r (from the name)

English

Let $r$ be an element of $R$. Let $M$ and $\mathrm{M'}$ be sets. Then the quotient multiplicative top tensor equivalence quotient multiplicative top of $r$ is a linear equivalence of the set of tensor products of the set of quotient multiplicative tops of $r$ and $\mathrm{M'}$ and $M$ and the set of quotient multiplicative tops of $r$ and the set of tensor products of $\mathrm{M'}$ and $M$ defined as the composition of the composition of the tensor of $M$ and the equivalence quotient tensor of $r$ and $\mathrm{M'}$ and the associator of $\mathrm{M'}$ and $M$ and the inverse of the equivalence quotient tensor of $r$ and the set of tensor products of $\mathrm{M'}$ and $M$.

QuotSMulTop.tensorQuotSMulTopEquivQuotSMulTopdefMathlib.RingTheory.QuotSMulTop, function or constant

Wording

the tensor quotient multiplicative top equivalence quotient multiplicative top of r (from the name)

English

Let $r$ be an element of $R$. Let $M$ and $\mathrm{M'}$ be sets. Then the tensor quotient multiplicative top equivalence quotient multiplicative top of $r$ is a linear equivalence of the set of tensor products of $M$ and the set of quotient multiplicative tops of $r$ and $\mathrm{M'}$ and the set of quotient multiplicative tops of $r$ and the set of tensor products of $M$ and $\mathrm{M'}$ defined as the composition of the composition of the tensor of $M$ and the equivalence tensor quotient of $r$ and $\mathrm{M'}$ and the inverse of the associator of $\mathrm{M'}$ and the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $r$ and the inverse of the equivalence tensor quotient of $r$ and the set of tensor products of $M$ and $\mathrm{M'}$.

Mathlib.RingTheory.Radical.Basic

EuclideanDomain.divRadicaldefMathlib.RingTheory.Radical.Basic, function or constant

Wording

the quotient radical of a (from the name)

English

Let $a$ be an element of $E$. Then the quotient radical of $a$ is an element of $E$ defined as the quotient of $a$ and the radical of $a$.

UniqueFactorizationMonoid.primeFactorsdefMathlib.RingTheory.Radical.Basic, function or constant

Wording

the finite set of prime factors of a (from the docstring)

English

Let $a$ be an element of $M$. Then the finite set of prime factors of $a$ is a finite set of $M$ defined as the finite set of the normalized factor of $a$.

UniqueFactorizationMonoid.radicaldefMathlib.RingTheory.Radical.Basic, function or constant

Wording

the radical of a (from the docstring)

English

Let $a$ be an element of $M$. Then the radical of $a$ is an element of $M$ defined as $\FinsetProd {\operatorname{primeFactors} (a)}{a_{1}}{\mathrm{id} (a_{1})}$.

Mathlib.RingTheory.RamificationInertia.Inertia

Ideal.inertiaDegdefMathlib.RingTheory.RamificationInertia.Inertia, function or constant

Wording

the inertia degree of q and R (from the name)

English

Let $q$ be an ideal of $S$. Let $R$ be a set. Then the inertia degree of $q$ and $R$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that $q$ is prime, the function that maps $h$ to the rank of the set of residue fields of $\operatorname{under}$ applied to $R$ and $q$ and the set of residue fields of $q$ and the function that maps $h_{1}$ to $0$.

Mathlib.RingTheory.RamificationInertia.Ramification

Ideal.ramificationIdxdefMathlib.RingTheory.RamificationInertia.Ramification, function or constant

Wording

the ramification index of q and R (from the name)

English

Let $q$ be an ideal of $S$. Let $R$ be a set. Then the ramification index of $q$ and $R$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that $q$ is prime, the function that maps $h$ to the natural number of the length of $\operatorname{AtPrime}$ applied to $q$ and the set of quotients of $\operatorname{AtPrime}$ applied to $q$ and the map of the algebra map of $R$ and $\operatorname{AtPrime}$ applied to $q$ and $\operatorname{under}$ applied to $R$ and $q$ and the function that maps $h_{1}$ to $0$.

Mathlib.RingTheory.ReesAlgebra

reesAlgebradefMathlib.RingTheory.ReesAlgebra, function or constant

Wording

the Rees algebra of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the Rees algebra of $I$ is a subalgebra of $R$ and the set of polynomials of $R$.

Mathlib.RingTheory.Regular.Category

ModuleCat.smulShortComplexdefMathlib.RingTheory.Regular.Category, function or constant

Wording

the scalar multiple short complex of M and r (from the name)

English

Let $M$ be a module category of $R$. Let $r$ be an element of $R$. Then the scalar multiple short complex of $M$ and $r$ is a short complex of the set of module categories of $R$.

Mathlib.RingTheory.Regular.RegularSequence

Ideal.ofListdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

the ideal generated by a list of elements of rs (from the docstring)

English

Let $\mathrm{rs}$ be a list of elements of $R$. Then the ideal generated by a list of elements of $\mathrm{rs}$ is an ideal of $R$ defined as the span of $\operatorname{ofPred}$ applied to the function that maps $r$ to $\MembershipmemMACRoT {\mathrm{rs}}{r}$.

RingTheory.Sequence.IsRegularstructureMathlib.RingTheory.Regular.RegularSequence, predicate

Wording

rs is regular (from the name)

English

Let $M$ be a set. Let $\mathrm{rs}$ be a list of elements of $R$. Then we can say that $\mathrm{rs}$ is regular.

RingTheory.Sequence.IsRegular.ndrecIterModByRegulardefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

Let $\mathrm{nil}$ be a function from sets $M_{2}$ and elements $x_{6}$ of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is an additive commutative group and elements $x_{7}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R$ and $M_{2}$ and elements of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is nontrivial to elements of $\mathrm{motive}$ applied to $M_{2}$, $x_{6}$, $x_{7}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from sets $M_{1}$ and elements $x_{3}$ of $\mathrm{Proof}$ applied to the proposition that $M_{1}$ is an additive commutative group and elements $x_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R$ and $M_{1}$ and elements $r$ of $R$ and lists $\mathrm{rs1}$ of elements of $R$ and elements of $\mathrm{Proof}$ applied to the proposition that $r$ is a multiplicative regular and elements of $\mathrm{Proof}$ applied to the proposition that $\mathrm{rs1}$ is regular and elements of $\mathrm{motive}$ applied to the set of quotient multiplicative tops of $r$ and $M_{1}$, $\operatorname{addCommGroup}$ applied to $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$, $\operatorname{module}$ applied to $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$ and $\mathrm{rs1}$ to elements of $\mathrm{motive}$ applied to $M_{1}$, $x_{3}$, $x_{4}$ and $\operatorname{cons}$ applied to $r$ and $\mathrm{rs1}$. Assume that $\mathrm{rs}$ is regular. Then $\operatorname{ndrecIterModByRegular}$ applied to $M_{2}$, $x_{6}$, $x_{7}$, $\mathrm{nil}$, $M_{1}$, $x_{3}$, $x_{4}$, $r$, $\mathrm{rs1}$, $\mathrm{cons}$ and $h$ is an element of $\mathrm{motive}$ applied to $M$, $x_{1}$, $x_{2}$ and $\mathrm{rs}$ defined as the function that maps $\mathrm{nil}$, $M_{1}$, $x_{3}$, $x_{4}$, $r$, $\mathrm{rs1}$, $\mathrm{cons}$ and $h$ to $\operatorname{recIterModByRegular}$ applied to $M_{2}$, the function that maps $x_{3}$, $x_{4}$ and $x_{5}$ to $x_{6}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$, $x_{7}$, $\mathrm{nil}$, $M_{1}$, $x_{3}$, $x_{4}$, $r$, $\mathrm{rs1}$, $\mathrm{cons}$ and $h$.

RingTheory.Sequence.IsRegular.ndrecIterModByRegularWithRingdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

Let $\mathrm{nil}$ be a function from sets $R_{2}$ and elements $x_{7}$ of $\mathrm{Proof}$ applied to the proposition that $R_{2}$ is a commutative ring and sets $M_{2}$ and elements $x_{8}$ of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is an additive commutative group and elements $x_{9}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R_{2}$ and $M_{2}$ and elements of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is nontrivial to elements of $\mathrm{motive}$ applied to $R_{2}$, $x_{7}$, $M_{2}$, $x_{8}$, $x_{9}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from sets $R_{1}$ and elements $x_{3}$ of $\mathrm{Proof}$ applied to the proposition that $R_{1}$ is a commutative ring and sets $M_{1}$ and elements $x_{4}$ of $\mathrm{Proof}$ applied to the proposition that $M_{1}$ is an additive commutative group and elements $x_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R_{1}$ and $M_{1}$ and elements $r$ of $R_{1}$ and lists $\mathrm{rs1}$ of elements of $R_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that $r$ is a multiplicative regular and elements of $\mathrm{Proof}$ applied to the proposition that $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to $r$ and $\mathrm{rs1}$ is regular and elements of $\mathrm{motive}$ applied to the set of quotients of $R_{1}$ and the span of $\operatorname{singleton}$ applied to $r$, $\operatorname{commRing}$ applied to the span of $\operatorname{singleton}$ applied to $r$, the set of quotient multiplicative tops of $r$ and $M_{1}$, $\operatorname{addCommGroup}$ applied to $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$, $\operatorname{instQuotientIdealSpanSingletonSetSubmoduleHSMulTop}$ applied to $M_{1}$ and $r$ and $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to $r$ and $\mathrm{rs1}$ to elements of $\mathrm{motive}$ applied to $R_{1}$, $x_{3}$, $M_{1}$, $x_{4}$, $x_{5}$ and $\operatorname{cons}$ applied to $r$ and $\mathrm{rs1}$. Assume that $\mathrm{rs}$ is regular. Then $\operatorname{ndrecIterModByRegularWithRing}$ applied to $R_{2}$, $x_{7}$, $M_{2}$, $x_{8}$, $x_{9}$, $\mathrm{nil}$, $R_{1}$, $x_{3}$, $M_{1}$, $x_{4}$, $x_{5}$, $r$, $\mathrm{rs1}$, $\mathrm{cons}$ and $h$ is an element of $\mathrm{motive}$ applied to $R$, $x$, $M$, $x_{1}$, $x_{2}$ and $\mathrm{rs}$ defined as the function that maps $x_{8}$, $x_{9}$, $\mathrm{nil}$, $R_{1}$, $x_{3}$, $M_{1}$, $x_{4}$, $x_{5}$, $r$, $\mathrm{rs1}$, $\mathrm{cons}$ and $h$ to $\operatorname{recIterModByRegularWithRing}$ applied to $R_{2}$, the function that maps $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$ and $x_{7}$ to $x_{7}$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$ and $x_{7}$, $M_{2}$, $x_{8}$, $x_{9}$, $\mathrm{nil}$, $R_{1}$, $x_{3}$, $M_{1}$, $x_{4}$, $x_{5}$, $r$, $\mathrm{rs1}$, $\mathrm{cons}$ and $h$.

RingTheory.Sequence.IsRegular.recIterModByRegulardefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

Let $\mathrm{nil}$ be a function from sets $M_{2}$ and elements $x_{5}$ of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is an additive commutative group and elements $x_{6}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R$ and $M_{2}$ and elements $h_{3}$ of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is nontrivial to elements of $\mathrm{motive}$ applied to $M_{2}$, $x_{5}$, $x_{6}$, $\operatorname{nil}$ and $\operatorname{nil}$ applied to $R$ and $M_{2}$. Let $\mathrm{cons}$ be a function from sets $M_{1}$ and elements $x_{3}$ of $\mathrm{Proof}$ applied to the proposition that $M_{1}$ is an additive commutative group and elements $x_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R$ and $M_{1}$ and elements $r$ of $R$ and lists $\mathrm{rs1}$ of elements of $R$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that $r$ is a multiplicative regular and elements $h_{2}$ of $\mathrm{Proof}$ applied to the proposition that $\mathrm{rs1}$ is regular and elements of $\mathrm{motive}$ applied to the set of quotient multiplicative tops of $r$ and $M_{1}$, $\operatorname{addCommGroup}$ applied to $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$, $\operatorname{module}$ applied to $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$, $\mathrm{rs1}$ and $h_{2}$ to elements of $\mathrm{motive}$ applied to $M_{1}$, $x_{3}$, $x_{4}$, $\operatorname{cons}$ applied to $r$ and $\mathrm{rs1}$ and $\operatorname{cons}$ applied to $h_{1}$ and $h_{2}$. Assume that $\mathrm{rs}$ is regular. Then $\operatorname{recIterModByRegular}$ applied to $M_{2}$, $x_{5}$, $x_{6}$, $h_{3}$, $\mathrm{nil}$, $M_{1}$, $x_{3}$, $x_{4}$, $r$, $\mathrm{rs1}$, $h_{1}$, $h_{2}$, $\mathrm{cons}$ and $h$ is an element of $\mathrm{motive}$ applied to $M$, $x_{1}$, $x_{2}$, $\mathrm{rs}$ and $h$.

RingTheory.Sequence.IsRegular.recIterModByRegularWithRingdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

Let $\mathrm{nil}$ be a function from sets $R_{2}$ and elements $x_{6}$ of $\mathrm{Proof}$ applied to the proposition that $R_{2}$ is a commutative ring and sets $M_{2}$ and elements $x_{7}$ of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is an additive commutative group and elements $x_{8}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R_{2}$ and $M_{2}$ and elements $h_{3}$ of $\mathrm{Proof}$ applied to the proposition that $M_{2}$ is nontrivial to elements of $\mathrm{motive}$ applied to $R_{2}$, $x_{6}$, $M_{2}$, $x_{7}$, $x_{8}$, $\operatorname{nil}$ and $\operatorname{nil}$ applied to $R_{2}$ and $M_{2}$. Let $\mathrm{cons}$ be a function from sets $R_{1}$ and elements $x_{3}$ of $\mathrm{Proof}$ applied to the proposition that $R_{1}$ is a commutative ring and sets $M_{1}$ and elements $x_{4}$ of $\mathrm{Proof}$ applied to the proposition that $M_{1}$ is an additive commutative group and elements $x_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Module}$ applied to $R_{1}$ and $M_{1}$ and elements $r$ of $R_{1}$ and lists $\mathrm{rs1}$ of elements of $R_{1}$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that $r$ is a multiplicative regular and elements $h_{2}$ of $\mathrm{Proof}$ applied to the proposition that $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to $r$ and $\mathrm{rs1}$ is regular and elements of $\mathrm{motive}$ applied to the set of quotients of $R_{1}$ and the span of $\operatorname{singleton}$ applied to $r$, $\operatorname{commRing}$ applied to the span of $\operatorname{singleton}$ applied to $r$, the set of quotient multiplicative tops of $r$ and $M_{1}$, $\operatorname{addCommGroup}$ applied to $\HSMulhSMulMACRoAL {r}{\operatorname{top}}$, $\operatorname{instQuotientIdealSpanSingletonSetSubmoduleHSMulTop}$ applied to $M_{1}$ and $r$, $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to $r$ and $\mathrm{rs1}$ and $h_{2}$ to elements of $\mathrm{motive}$ applied to $R_{1}$, $x_{3}$, $M_{1}$, $x_{4}$, $x_{5}$, $\operatorname{cons}$ applied to $r$ and $\mathrm{rs1}$ and $\operatorname{cons'}$ applied to $h_{1}$ and $h_{2}$. Assume that $\mathrm{rs}$ is regular. Then $\operatorname{recIterModByRegularWithRing}$ applied to $R_{2}$, $x_{6}$, $M_{2}$, $x_{7}$, $x_{8}$, $h_{3}$, $\mathrm{nil}$, $R_{1}$, $x_{3}$, $M_{1}$, $x_{4}$, $x_{5}$, $r$, $\mathrm{rs1}$, $h_{1}$, $h_{2}$, $\mathrm{cons}$ and $h$ is an element of $\mathrm{motive}$ applied to $R$, $x$, $M$, $x_{1}$, $x_{2}$, $\mathrm{rs}$ and $h$.

RingTheory.Sequence.IsWeaklyRegularstructureMathlib.RingTheory.Regular.RegularSequence, predicate

Wording

rs is weakly regular (from the name)

English

generation took over the time limit

RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegulardefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

no reading

RingTheory.Sequence.IsWeaklyRegular.ndrecWithRingdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

no reading

RingTheory.Sequence.IsWeaklyRegular.recIterModByRegulardefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

no reading

RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRingdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

no wording

English

no reading

Submodule.quotOfListConsSMulTopEquivQuotSMulTopInnerdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

the quotient of r and rs (from the name)

English

Let $M$ be a set. Let $r$ be an element of $R$. Let $\mathrm{rs}$ be a list of elements of $R$. Then the quotient of $r$ and $\mathrm{rs}$ is a linear equivalence of the set of quotients of $M$ and $\HSMulhSMulMACRoAL {\operatorname{ofList} (\operatorname{cons} (r , \mathrm{rs}))}{\operatorname{top}}$ and the set of quotients of the set of quotient multiplicative tops of $r$ and $M$ and $\HSMulhSMulMACRoAL {\operatorname{ofList} (\mathrm{rs})}{\operatorname{top}}$.

Submodule.quotOfListConsSMulTopEquivQuotSMulTopOuterdefMathlib.RingTheory.Regular.RegularSequence, function or constant

Wording

the quotient of r and rs (from the name)

English

Let $M$ be a set. Let $r$ be an element of $R$. Let $\mathrm{rs}$ be a list of elements of $R$. Then the quotient of $r$ and $\mathrm{rs}$ is a linear equivalence of the set of quotients of $M$ and $\HSMulhSMulMACRoAL {\operatorname{ofList} (\operatorname{cons} (r , \mathrm{rs}))}{\operatorname{top}}$ and the set of quotient multiplicative tops of $r$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {\operatorname{ofList} (\mathrm{rs})}{\operatorname{top}}$.

Mathlib.RingTheory.RegularLocalRing.Defs

IsRegularLocalRingclassMathlib.RingTheory.RegularLocalRing.Defs, predicate

Wording

R is a regular local ring (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a regular local ring.

IsRegularRingclassMathlib.RingTheory.RegularLocalRing.Defs, predicate

Wording

R is regular (from the docstring)

English

Let $R$ be a set. Then we can say that $R$ is regular.

Mathlib.RingTheory.RingHom.Etale

RingHom.EtaledefMathlib.RingTheory.RingHom.Etale, predicate

Wording

f is a etale (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $f$ is an etale, if $\operatorname{Etale}$ holds for $R$ and $S$.

Mathlib.RingTheory.RingHom.FaithfullyFlat

RingHom.FaithfullyFlatdefMathlib.RingTheory.RingHom.FaithfullyFlat, predicate

Wording

f is faithfully flat (from the name)

English

generation took over the time limit

Mathlib.RingTheory.RingHom.Flat

CommRingCat.flatdefMathlib.RingTheory.RingHom.Flat, function or constant

Wording

no wording

English

There is a morphism property of the set of categories of commutative rings. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. By f. By RingHom__Flat. By RingHom__toMorphismProperty.

RingHom.FlatdefMathlib.RingTheory.RingHom.Flat, predicate

Wording

f is flat (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $f$ is flat, if $S$ is flat with respect to $R$.

Mathlib.RingTheory.RingHom.Locally

RingHom.LocallydefMathlib.RingTheory.RingHom.Locally, predicate

Wording

no wording

English

Let $P$ be a function from sets $R_{1}$ and sets $S_{1}$ and elements $x_{2}$ of $\mathrm{Proof}$ applied to the proposition that $R_{1}$ is a commutative ring and elements $x_{3}$ of $\mathrm{Proof}$ applied to the proposition that $S_{1}$ is a commutative ring and ring homomorphisms of $R_{1}$ and $S_{1}$ to propositions. Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{Locally}$ holds for $R_{1}$, $S_{1}$, $x_{2}$, $x_{3}$, $P$ and $f$, if there exists an element $s$ of $\wp S$, such that there exists an element $h$ of $\mathrm{Eqt}$ applied to the span of $s$ and the top, such that for all elements $t$ of $S$, if $t$ is an element of $s$, then $R_{1}$ holds for $R$, $\operatorname{Away}$ applied to $t$, $x$, $\operatorname{instCommRing}$ and the composition of the algebra map of $S$ and $\operatorname{Away}$ applied to $t$ and $S_{1}$.

Mathlib.RingTheory.RingHom.OpenImmersion

Algebra.IsStandardOpenImmersionclassMathlib.RingTheory.RingHom.OpenImmersion, predicate

Wording

no wording

English

Let $R$ and $S$ be sets. Then we can say that $\operatorname{IsStandardOpenImmersion}$ holds for $R$ and $S$.

RingHom.IsStandardOpenImmersiondefMathlib.RingTheory.RingHom.OpenImmersion, predicate

Wording

f is a standard open immersion (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $f$ is a standard open immersion, if $\operatorname{IsStandardOpenImmersion}$ holds for $R$ and $S$.

Mathlib.RingTheory.RingHom.PurelyInseparable

RingHom.IsPurelyInseparabledefMathlib.RingTheory.RingHom.PurelyInseparable, predicate

Wording

f is purely inseparable (from the name)

English

generation took over the time limit

Mathlib.RingTheory.RingHom.QuasiFinite

RingHom.QuasiFinitedefMathlib.RingTheory.RingHom.QuasiFinite, predicate

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{QuasiFinite}$ holds for $f$, if $\operatorname{QuasiFinite}$ holds for $R$ and $S$.

RingHom.QuasiFiniteAtdefMathlib.RingTheory.RingHom.QuasiFinite, predicate

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $p$ be an ideal of $S$. Then $\operatorname{QuasiFiniteAt}$ holds for $f$ and $p$, if $\operatorname{QuasiFiniteAt}$ holds for $R$ and $p$.

Mathlib.RingTheory.RingHom.Smooth

RingHom.FormallySmoothdefMathlib.RingTheory.RingHom.Smooth, predicate

Wording

f is formally smooth (from the name)

English

generation took over the time limit

RingHom.SmoothdefMathlib.RingTheory.RingHom.Smooth, predicate

Wording

f is smooth (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $f$ is smooth, if $\operatorname{Smooth}$ holds for $R$ and $S$.

Mathlib.RingTheory.RingHom.StandardSmooth

RingHom.IsStandardSmoothdefMathlib.RingTheory.RingHom.StandardSmooth, predicate

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{IsStandardSmooth}$ holds for $f$, if $\operatorname{IsStandardSmooth}$ holds for $R$ and $S$.

RingHom.IsStandardSmoothOfRelativeDimensiondefMathlib.RingTheory.RingHom.StandardSmooth, predicate

Wording

no wording

English

Let $n$ be a natural number. Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{IsStandardSmoothOfRelativeDimension}$ holds for $n$ and $f$, if $n$ is a standard smooth of relative dimension.

Mathlib.RingTheory.RingHom.Unramified

RingHom.FormallyUnramifieddefMathlib.RingTheory.RingHom.Unramified, predicate

Wording

f is formally unramified (from the name)

English

generation took over the time limit

Mathlib.RingTheory.RingHomProperties

RingHom.CodescendsAlongdefMathlib.RingTheory.RingHomProperties, predicate

Wording

no wording

English

Let $P$ be a function from sets $R_{1}$ and sets $S_{1}$ and elements $x_{3}$ of $\mathrm{Proof}$ applied to the proposition that $R_{1}$ is a commutative ring and elements $x_{4}$ of $\mathrm{Proof}$ applied to the proposition that $S_{1}$ is a commutative ring and ring homomorphisms of $R_{1}$ and $S_{1}$ to propositions. Let $Q$ 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 $\operatorname{CodescendsAlong}$ holds for $R_{1}$, $S_{1}$, $x_{3}$, $x_{4}$, $P$, $R$, $S$, $x$, $x_{1}$ and $Q$, if for all sets $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$, 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 $\mathrm{R'}$, for all elements $x_{3}$ of $\mathrm{CommRing}$ applied to $\mathrm{S'}$, for all elements $x_{4}$ of $\mathrm{Algebra}$ applied to $R$ and $S$, for all elements $x_{5}$ of $\mathrm{Algebra}$ applied to $R$ and $\mathrm{R'}$, for all elements $x_{6}$ of $\mathrm{Algebra}$ applied to $R$ and $\mathrm{S'}$, for all elements $x_{7}$ of $\mathrm{Algebra}$ applied to $S$ and $\mathrm{S'}$, for all elements $x_{8}$ of $\mathrm{Algebra}$ applied to $\mathrm{R'}$ and $\mathrm{S'}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{IsScalarTower}$ applied to $R$, $S$ and $\mathrm{S'}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{IsScalarTower}$ applied to $R$, $\mathrm{R'}$ and $\mathrm{S'}$, if $\operatorname{IsPushout}$ holds for $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$, then if $S_{1}$ holds for $R$, $\mathrm{R'}$, $x$, $x_{2}$ and the algebra map of $R$ and $\mathrm{R'}$, then if $R_{1}$ holds for $\mathrm{R'}$, $\mathrm{S'}$, $x_{2}$, $x_{3}$ and the algebra map of $\mathrm{R'}$ and $\mathrm{S'}$, then $R_{1}$ holds for $R$, $S$, $x$, $x_{1}$ and the algebra map of $R$ and $S$.

RingHom.HasEqualizersdefMathlib.RingTheory.RingHomProperties, predicate

Wording

P has 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 equalizers, if for all sets $R$, $S$ and $T$, 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 $T$, for all elements $x_{3}$ of $\mathrm{Algebra}$ applied to $R$ and $S$, for all elements $x_{4}$ of $\mathrm{Algebra}$ applied to $R$ and $T$, for all algebra homomorphisms $f$ and $g$ of $S$ and $T$, if $R$ holds for $R$, $S$, $x$, $x_{1}$ and the algebra map of $R$ and $S$, then if $R$ holds for $R$, $T$, $x$, $x_{2}$ and the algebra map of $R$ and $T$, then $R$ holds for $R$, $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{5}})}$, $x$, $\operatorname{toCommRing}$ applied to the equalizer of $f$ and $g$ and the algebra map of $R$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{6}})}$.

RingHom.HasFiniteProductsdefMathlib.RingTheory.RingHomProperties, predicate

Wording

P has finite products (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 finite products, if for all sets $R$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all sets $x_{1}$, if $x_{1}$ is finite, then for all functions $S$ from elements of $x_{1}$ to sets, for all functions $x_{2}$ from elements $i_{4}$ of $x_{1}$ to elements of $\mathrm{CommRing}$ applied to $S$ applied to $i_{4}$, for all functions $x_{3}$ from elements $i_{3}$ of $x_{1}$ to elements of $\mathrm{Algebra}$ applied to $R$ and $S$ applied to $i_{3}$, if for all elements $i_{2}$ of $x_{1}$, $R$ holds for $R$, $S$ applied to $i_{2}$, $x$, $x_{2}$ applied to $i_{2}$ and the algebra map of $R$ and $S$ applied to $i_{2}$, then $R$ holds for $R$, the set of functions from elements $i$ of $x_{1}$ to elements of $S$ applied to $i$, $x$, $\operatorname{commRing}$ and the algebra map of $R$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $S$ applied to $i_{1}$.

RingHom.IsStableUnderBaseChangedefMathlib.RingTheory.RingHomProperties, predicate

Wording

P is a stable under base change (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$ is a stable under base change, if for all sets $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$, 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 $\mathrm{R'}$, for all elements $x_{3}$ of $\mathrm{CommRing}$ applied to $\mathrm{S'}$, for all elements $x_{4}$ of $\mathrm{Algebra}$ applied to $R$ and $S$, for all elements $x_{5}$ of $\mathrm{Algebra}$ applied to $R$ and $\mathrm{R'}$, for all elements $x_{6}$ of $\mathrm{Algebra}$ applied to $R$ and $\mathrm{S'}$, for all elements $x_{7}$ of $\mathrm{Algebra}$ applied to $S$ and $\mathrm{S'}$, for all elements $x_{8}$ of $\mathrm{Algebra}$ applied to $\mathrm{R'}$ and $\mathrm{S'}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{IsScalarTower}$ applied to $R$, $S$ and $\mathrm{S'}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{IsScalarTower}$ applied to $R$, $\mathrm{R'}$ and $\mathrm{S'}$, if $\operatorname{IsPushout}$ holds for $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$, then if $R$ holds for $R$, $S$, $x$, $x_{1}$ and the algebra map of $R$ and $S$, then $R$ holds for $\mathrm{R'}$, $\mathrm{S'}$, $x_{2}$, $x_{3}$ and the algebra map of $\mathrm{R'}$ and $\mathrm{S'}$.

RingHom.RespectsIsodefMathlib.RingTheory.RingHomProperties, predicate

Wording

no wording

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 $\operatorname{RespectsIso}$ holds for $R$, $S$, $x$, $x_{1}$ and $P$, if for all sets $R$, for all sets $S$, for all sets $T$, 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 $T$, for all ring homomorphisms $f$ of $R$ and $S$, for all ring isomorphisms $e$ of $S$ and $T$, if $R$ holds for $R$, $S$, $x$, $x_{1}$ and $f$, then $R$ holds for $R$, $T$, $x$, $x_{2}$ and the composition of the ring homomorphism of $e$ and $f$ and for all sets $R_{1}$, for all sets $S_{1}$, for all sets $T_{1}$, for all elements $x_{3}$ of $\mathrm{CommRing}$ applied to $R_{1}$, for all elements $x_{4}$ of $\mathrm{CommRing}$ applied to $S_{1}$, for all elements $x_{5}$ of $\mathrm{CommRing}$ applied to $T_{1}$, for all ring homomorphisms $f_{1}$ of $S_{1}$ and $T_{1}$, for all ring isomorphisms $e_{1}$ of $R_{1}$ and $S_{1}$, if $R$ holds for $S_{1}$, $T_{1}$, $x_{4}$, $x_{5}$ and $f_{1}$, then $R$ holds for $R_{1}$, $T_{1}$, $x_{3}$, $x_{5}$ and the composition of $f_{1}$ and the ring homomorphism of $e_{1}$.

RingHom.StableUnderCompositiondefMathlib.RingTheory.RingHomProperties, predicate

Wording

P is stable under composition (from the name)

English

RingHom.toMorphismPropertydefMathlib.RingTheory.RingHomProperties, function or constant

Wording

the morphism property of P (from the name)

English

Mathlib.RingTheory.RingInvo

RingInvostructureMathlib.RingTheory.RingInvo, type

Wording

no wording

English

Let $R$ be a set. Then the elements of $\mathrm{RingInvo}$ applied to $R$ are a basic type.

RingInvo.iddefMathlib.RingTheory.RingInvo, function or constant

Wording

the identity function of R (from the docstring)

English

Let $R$ be a set. Then the identity function of $R$ is an element of $\mathrm{RingInvo}$ applied to $R$.

RingInvo.mk'defMathlib.RingTheory.RingInvo, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and the set of multiplicative opposites of $R$ such that for all elements $r$ of $R$, the opposite of $f$ applied to the opposite of $f$ applied to $r$ is equal to $r$. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{involution}$ is an element of $\mathrm{RingInvo}$ applied to $R$.

RingInvoClassclassMathlib.RingTheory.RingInvo, predicate

Wording

no wording

English

Let $F$ and $R$ be sets. Then we can say that $\mathrm{RingInvoClass}$ holds for $F$ and $R$.

RingInvoClass.toRingInvodefMathlib.RingTheory.RingInvo, function or constant

Wording

no wording

English

Let $f$ be an element of $F$. Then $\operatorname{toRingInvo}$ applied to $f$ is an element of $\mathrm{RingInvo}$ applied to $R$ defined as $\operatorname{mk}$ applied to the ring isomorphism of $f$ and $\operatorname{involution}$ applied to $f$.

Mathlib.RingTheory.RootsOfUnity.Basic

IsCyclic.monoidHomMulEquivRootsOfUnityOfGeneratordefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

the monoid homomorphism multiplicative equivalence root of hg and #2 (from the name)

English

Assume that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Let $\mathrm{G'}$ be a set. Then the monoid homomorphism multiplicative equivalence root of $\mathrm{hg}$ and $\mathrm{G'}$ is a multiplicative equivalence of the set of monoid homomorphisms of $G$ and $\mathrm{G'}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (\operatorname{card} (G), \mathrm{G'})}{x_{2}})}$.

MulEquiv.restrictRootsOfUnitydefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a multiplicative equivalence of $R$ and $S$. Let $n$ be an element of $\Natural$. Then $\operatorname{restrictRootsOfUnity}$ applied to $x_{2}$ and $n$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , R)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , S)}{x_{4}})}$.

restrictRootsOfUnitydefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be an element of $F$. Let $n$ be an element of $\Natural$. Then $\mathrm{restrictRootsOfUnity}$ applied to $x_{3}$ and $n$ is a monoid homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , R)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , S)}{x_{5}})}$.

rootsOfUnitydefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

the root of k and M (from the name)

English

Let $k$ be a natural number. Let $M$ be a set. Then the root of $k$ and $M$ is a subgroup of $\UnitsMACRoAO {M}$.

rootsOfUnity.mkOfPowEqdefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $M$ such that $\EqtMACRoH {x_{1} ^ {n}}{1}$. Then $\operatorname{mkOfPowEq}$ applied to $x_{1}$ and $h_{1}$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , M)}{x_{2}})}$.

rootsOfUnityEquivNthRootsdefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

the root of R and k (from the name)

English

Let $R$ be a set. Let $k$ be an element of $\Natural$. Then the root of $R$ and $k$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (k , R)}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{nthRoots} (k , 1)}{x_{2}})})}$.

rootsOfUnityUnitsMulEquivdefMathlib.RingTheory.RootsOfUnity.Basic, function or constant

Wording

the root of M and n (from the name)

English

Let $M$ be a set. Let $n$ be an element of $\Natural$. Then the root of $M$ and $n$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , \UnitsMACRoAO {M})}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , M)}{x_{2}})}$.

Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

HasEnoughRootsOfUnityclassMathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity, predicate

Wording

n has a enough root of unity (from the name)

English

Let $M$ be a set. Let $n$ be a natural number. Then we can say that $n$ has an enough root of unity.

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

IsPrimitiveRootstructureMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $M$. Let $k$ be a natural number. Then we can say that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $k$.

IsPrimitiveRoot.autToPowdefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the automorphism to power of R and h1 (from the name)

English

Let $R$ be a set. Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $n$. Then the automorphism to power of $R$ and $h_{1}$ is a monoid homomorphism of the set of algebra isomorphisms of $S$ and $S$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$.

IsPrimitiveRoot.primitiveRootsPowEquivdefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the primitive root power equivalence of h1 (from the name)

English

Assume that $\operatorname{ModEq}$ holds for $n$, $a \times b$ and $1$. Then the primitive root power equivalence of $h_{1}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{primitiveRoots} (n , R)}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{primitiveRoots} (n , R)}{x_{2}})})}$.

IsPrimitiveRoot.primitiveRootsPowEquivOfCoprimedefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the primitive root power equivalence of h1 (from the name)

English

Assume that $\NatCoprimeMACRoC {a}{n}$. Then the primitive root power equivalence of $h_{1}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{primitiveRoots} (n , R)}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{primitiveRoots} (n , R)}{x_{2}})})}$.

IsPrimitiveRoot.toRootsOfUnitydefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the root of h1 (from the name)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $n$. Then the root of $h_{1}$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , M)}{x_{2}})}$ defined as $\operatorname{mkOfPowEq}$ applied to $x_{1}$ and $\mathrm{IsPrimitiveRoot\_\_pow\_eq\_one}$ applied to $h_{1}$.

IsPrimitiveRoot.zmodEquivZPowersdefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the integer modulo equivalence power of h (from the name)

English

Assume that $\mathrm{IsPrimitiveRoot}$ holds for $x_{1}$ and $k$. Then the integer modulo equivalence power of $h$ is an additive equivalence of $\mathrm{ZMod}$ applied to $k$ and $\mathrm{Additive}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{zpowers} (x_{1})}{x_{2}})}$.

primitiveRootsdefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the primitive root of k and R (from the name)

English

Let $k$ be an element of $\Natural$. Let $R$ be a set. Then the primitive root of $k$ and $R$ is a finite set of $R$ defined as $\FinsetFilter {x_{1}}{\mathrm{IsPrimitiveRoot} (x_{1} , k)}{\operatorname{toFinset} (\operatorname{nthRoots} (k , 1))}$.

rootsOfUnityEquivOfPrimitiveRootsdefMathlib.RingTheory.RootsOfUnity.PrimitiveRoots, function or constant

Wording

the root of hf and h4 (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Assume that the primitive root of $n$ and $R$ is nonempty. Then the root of $\mathrm{hf}$ and $h_{4}$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , R)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , S)}{x_{4}})}$.

Mathlib.RingTheory.SimpleModule.Basic

IsSemisimpleModuleclassMathlib.RingTheory.SimpleModule.Basic, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then we can say that $\mathrm{IsSemisimpleModule}$ holds for $R$ and $M$.

IsSemisimpleRingdefMathlib.RingTheory.SimpleModule.Basic, predicate

Wording

R is semisimple (from the docstring)

English

Let $R$ be a set. Then $R$ is semisimple, if $\mathrm{IsSemisimpleModule}$ holds for $R$ and $R$.

IsSimpleModuleclassMathlib.RingTheory.SimpleModule.Basic, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then we can say that $\mathrm{IsSimpleModule}$ holds for $R$ and $M$.

JordanHolderLattice.Iso.linearEquivdefMathlib.RingTheory.SimpleModule.Basic, function or constant

Wording

the linear equivalence of h (from the name)

English

Assume that $\operatorname{Iso}$ holds for $X$ and $Y$. Then the linear equivalence of $h$ is a linear equivalence of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\ProdsndMACRoAA {X}}{x_{3}})}$ and the preimage of the subtype of $\ProdsndMACRoAA {X}$ and $\ProdfstMACRoZ {X}$ and the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\ProdsndMACRoAA {Y}}{x_{4}})}$ and the preimage of the subtype of $\ProdsndMACRoAA {Y}$ and $\ProdfstMACRoZ {Y}$.

Mathlib.RingTheory.SimpleModule.Isotypic

GaloisCoinsertion.setIsotypicComponentsdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the set isotypic component of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the set isotypic component of $R$ and $M$ is a Galois coinsertion of the function that maps $s$ to the supremum of the function that maps $c$ to the supremum of the function that maps $h$ to $c$ and the function that maps $m$ to $\operatorname{ofPred}$ applied to the function that maps $c_{1}$ to $\mathrm{Leq} (c_{1} , m)$.

IsIsotypicdefMathlib.RingTheory.SimpleModule.Isotypic, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\mathrm{IsIsotypic}$ holds for $R$ and $M$, if for all submodules $m$ of $R$ and $M$, if $\mathrm{IsSimpleModule}$ holds for $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {m}{x_{4}})}$, then $\mathrm{IsIsotypicOfType}$ holds for $R$, $M$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {m}{x_{3}})}$.

IsIsotypicOfTypedefMathlib.RingTheory.SimpleModule.Isotypic, predicate

Wording

no wording

English

Let $R$, $M$ and $S$ be sets. Then $\mathrm{IsIsotypicOfType}$ holds for $R$, $M$ and $S$, if for all submodules $m$ of $R$ and $M$, if $\mathrm{IsSimpleModule}$ holds for $R$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {m}{x_{6}})}$, then $\mathrm{Nonempty}$ holds for the set of linear equivalences of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {m}{x_{5}})}$ and $S$.

IsSemisimpleModule.endAlgEquivdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the end algebra isomorphism of R and M (from the name)

English

Let $x$, $R$ and $M$ be sets. Then the end algebra isomorphism of $R$ and $M$ is an algebra isomorphism of the set of ends of $R$ and $M$ and the set of functions from elements $c$ of the isotypic component of $R$ and $M$ to ends of $R$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {c}{x_{8}})}$.

IsSemisimpleModule.endRingEquivdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the endomorphism ring of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the endomorphism ring of $R$ and $M$ is a ring isomorphism of the set of ends of $R$ and $M$ and the set of functions from elements $c$ of the isotypic component of $R$ and $M$ to ends of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {c}{x_{4}})}$ defined as the ring isomorphism of the end algebra isomorphism of $R$ and $M$.

OrderIso.setIsotypicComponentsdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the set isotypic component (from the name)

English

The set isotypic component is an order isomorphism of $\wp \operatorname{Elem} (\mathrm{isotypicComponents} (R , M))$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fullyInvariantSubmodule} (R , M)}{x_{3}})}$.

Submodule.IsFullyInvariantdefMathlib.RingTheory.SimpleModule.Isotypic, predicate

Wording

N is fully invariant (from the name)

English

generation took over the time limit

fullyInvariantSubmoduledefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the fully invariant submodule of R and M (from the name)

English

generation took over the time limit

iSupIndep.algEquivdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the algebra isomorphism of iSup_top and invar (from the name)

English

generation took over the time limit

iSupIndep.ringEquivdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the ring isomorphism of iSup_top and invar (from the name)

English

generation took over the time limit

isotypicComponentdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the isotypic component of M and S (from the name)

English

Let $R$, $M$ and $S$ be sets. Then the isotypic component of $M$ and $S$ is a submodule of $R$ and $M$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $m$ to $\mathrm{Nonempty}$ applied to the set of linear equivalences of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {m}{x_{5}})}$ and $S$.

isotypicComponentsdefMathlib.RingTheory.SimpleModule.Isotypic, function or constant

Wording

the isotypic component of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the isotypic component of $R$ and $M$ is an element of the power set of the set of submodules of $R$ and $M$ defined as $\operatorname{ofPred}$ applied to the function that maps $m$ to the proposition that there exists a submodule $S$ of $R$ and $M$, such that $\mathrm{IsSimpleModule}$ holds for $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and $m$ is equal to the isotypic component of $M$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$.

Mathlib.RingTheory.SimpleRing.Defs

IsSimpleRingclassMathlib.RingTheory.SimpleRing.Defs, predicate

Wording

R is a simple ring (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a simple ring.

Mathlib.RingTheory.Smooth.Basic

Algebra.Extension.H1Cotangent.equivOfFormallySmoothdefMathlib.RingTheory.Smooth.Basic, function or constant

Wording

the equivalence of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be extensions of $R$ and $A$. Then the equivalence of $x_{3}$ and $x_{4}$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to $x_{3}$ and $\operatorname{H1Cotangent}$ applied to $x_{4}$ defined as the composition of the composition of the linear equivalence of the map of $\operatorname{toInfinitesimal}$ applied to $x_{3}$ and $\mathrm{Algebra\_\_Extension\_\_H1Cotangent\_\_map\_toInfinitesimal\_bijective}$ applied to $x_{3}$ and the equivalence of $\operatorname{homInfinitesimal}$ applied to $x_{3}$ and $x_{4}$ and $\operatorname{homInfinitesimal}$ applied to $x_{4}$ and $x_{3}$ and the inverse of the linear equivalence of the map of $\operatorname{toInfinitesimal}$ applied to $x_{4}$ and $\mathrm{Algebra\_\_Extension\_\_H1Cotangent\_\_map\_toInfinitesimal\_bijective}$ applied to $x_{4}$.

Algebra.Extension.equivH1CotangentOfFormallySmoothdefMathlib.RingTheory.Smooth.Basic, function or constant

Wording

no wording

English

Let $P$ be an extension of $R$ and $A$. Then $\operatorname{equivH1CotangentOfFormallySmooth}$ applied to $P$ is a linear equivalence of $\operatorname{H1Cotangent}$ applied to $P$ and $\operatorname{H1Cotangent}$ applied to $R$ and $A$ defined as the equivalence of $P$ and the extension of the self of $R$ and $A$.

Algebra.Extension.homInfinitesimaldefMathlib.RingTheory.Smooth.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ and $x_{4}$ be extensions of $R$ and $A$. Then $\operatorname{homInfinitesimal}$ applied to $x_{3}$ and $x_{4}$ is a homomorphism of $\operatorname{infinitesimal}$ applied to $x_{3}$ and $\operatorname{infinitesimal}$ applied to $x_{4}$.

Algebra.FormallySmoothclassMathlib.RingTheory.Smooth.Basic, predicate

Wording

no wording

English

Let $R$ and $A$ be sets. Then we can say that $\operatorname{FormallySmooth}$ holds for $R$ and $A$.

Algebra.FormallySmooth.liftdefMathlib.RingTheory.Smooth.Basic, function or constant

Wording

the lift of I and g (from the name)

English

Let $I$ be a nilpotent ideal of $B$. Let $g$ be an algebra homomorphism of $A$ and the set of quotients of $B$ and $I$. Then the lift of $I$ and $g$ is an algebra homomorphism of $A$ and $B$ defined as $\operatorname{choose}$ applied to $\mathrm{Algebra\_\_FormallySmooth\_\_exists\_lift}$ applied to $I$, $\mathrm{hI}$ and $g$.

Algebra.FormallySmooth.liftOfSurjectivedefMathlib.RingTheory.Smooth.Basic, function or constant

Wording

the lift of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $C$. Let $g$ be an algebra homomorphism of $B$ and $C$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$ and the kernel of the ring homomorphism of $g$ is nilpotent. Then the lift of $f$ and $g$ is an algebra homomorphism of $A$ and $B$ defined as the lift of the kernel of the ring homomorphism of $g$ and the composition of the algebra homomorphism of the inverse of the quotient kernel algebra isomorphism of $\mathrm{hg}$ and $f$.

Algebra.SmoothclassMathlib.RingTheory.Smooth.Basic, predicate

Wording

no wording

English

Let $R$ and $A$ be sets. Then we can say that $\operatorname{Smooth}$ holds for $R$ and $A$.

Mathlib.RingTheory.Smooth.IntegralClosure

TensorProduct.toIntegralClosuredefMathlib.RingTheory.Smooth.IntegralClosure, function or constant

Wording

the integral closure of S and B (from the name)

English

Let $R$, $S$ and $B$ be sets. Then the integral closure of $S$ and $B$ is an algebra homomorphism of the set of tensor products of $S$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (R , B)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (S , \mathrm{TensorProduct} (S , B))}{x_{6}})}$.

Mathlib.RingTheory.Smooth.Kaehler

derivationOfSectionOfKerSqZerodefMathlib.RingTheory.Smooth.Kaehler, function or constant

Wording

the derivation of f and hg (from the name)

English

Let $f$ be an algebra homomorphism of $P$ and $S$ such that $\EqtMACRoH {\operatorname{ker} (f)^ {2}}{\operatorname{bot}}$. Let $g$ be an algebra homomorphism of $S$ and $P$ such that $\EqtMACRoH {\operatorname{comp} (f , g)}{\operatorname{id} (R , S)}$. Then the derivation of $f$ and $g$ is a derivation of $P$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{5}})}$.

derivationQuotKerSqdefMathlib.RingTheory.Smooth.Kaehler, function or constant

Wording

the derivation quotient kernel square of P and S (from the name)

English

Let $R$, $P$ and $S$ be sets. Then the derivation quotient kernel square of $P$ and $S$ is a derivation of the set of quotients of $P$ and the exponentiation of the kernel of the algebra map of $P$ and $S$ to $2$ and the set of tensor products of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $P$.

retractionKerCotangentToTensorEquivSectiondefMathlib.RingTheory.Smooth.Kaehler, function or constant

Wording

the retraction kernel cotangent to tensor equivalence section of hf (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $P$ and $S$. Then the retraction kernel cotangent to tensor equivalence section of $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \operatorname{kerCotangentToTensor} (P , S))}{\operatorname{id}})})}{(\SubtypeSet {g}{(\EqtMACRoH {\operatorname{comp} (\operatorname{kerSquareLift} (\operatorname{toAlgHom} (P , S)), g)}{\operatorname{id} (R , S)})})}$.

retractionKerToTensorEquivSectiondefMathlib.RingTheory.Smooth.Kaehler, function or constant

Wording

the retraction kernel to tensor equivalence section of hf and #2 (from the name)

English

Assume that $\EqtMACRoH {\operatorname{ker} (\operatorname{algebraMap} (P , S))^ {2}}{\operatorname{bot}}$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $P$ and $S$. Then the retraction kernel to tensor equivalence section of $\mathrm{hf'}$ and $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \operatorname{kerToTensor} (P , S))}{\operatorname{id}})})}{(\SubtypeSet {g}{(\EqtMACRoH {\operatorname{comp} (\operatorname{toAlgHom} (P , S), g)}{\operatorname{id} (R , S)})})}$.

retractionOfSectionOfKerSqZerodefMathlib.RingTheory.Smooth.Kaehler, function or constant

Wording

the retraction of g (from the name)

English

Let $g$ be an algebra homomorphism of $S$ and $P$. Assume that $\EqtMACRoH {\operatorname{ker} (\operatorname{algebraMap} (P , S))^ {2}}{\operatorname{bot}}$. Assume that $\EqtMACRoH {\operatorname{comp} (\operatorname{toAlgHom} (P , S), g)}{\operatorname{id} (R , S)}$. Then the retraction of $g$ is a linear map of the set of tensor products of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $P$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{algebraMap} (P , S))}{x_{6}})}$ defined as $\operatorname{restrictScalars}$ applied to $P$ and the lift base change of $S$ and $\operatorname{liftKaehlerDifferential}$ applied to the derivation of the algebra homomorphism of $P$ and $S$ and $g$.

sectionOfRetractionKerToTensordefMathlib.RingTheory.Smooth.Kaehler, function or constant

Wording

the section of l (from the name)

English

Let $l$ be a linear map of the set of tensor products of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $P$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{algebraMap} (P , S))}{x_{8}})}$ such that $\EqtMACRoH {\operatorname{comp} (l , \operatorname{kerToTensor} (P , S))}{\operatorname{id}}$. Assume that $\EqtMACRoH {\operatorname{ker} (\operatorname{algebraMap} (P , S))^ {2}}{\operatorname{bot}}$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $P$ and $S$. Then the section of $l$ is an algebra homomorphism of $S$ and $P$.

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Mathlib.RingTheory.Norm.Defs

Mathlib.RingTheory.Norm.Transitivity

Mathlib.RingTheory.NormalClosure

Mathlib.RingTheory.Nullstellensatz

Mathlib.RingTheory.OrderOfVanishing.Basic

Mathlib.RingTheory.OrderOfVanishing.Noetherian

Mathlib.RingTheory.OreLocalization.Basic

Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Mathlib.RingTheory.OreLocalization.Ring

Mathlib.RingTheory.OrzechProperty

Mathlib.RingTheory.Perfection

Mathlib.RingTheory.Perfectoid.BDeRham

Mathlib.RingTheory.Perfectoid.FontaineTheta

Mathlib.RingTheory.Perfectoid.Untilt

Mathlib.RingTheory.PiTensorProduct

Mathlib.RingTheory.PicardGroup

Mathlib.RingTheory.Polynomial.Basic

Mathlib.RingTheory.Polynomial.Bernstein

Mathlib.RingTheory.Polynomial.Chebyshev

Mathlib.RingTheory.Polynomial.Content

Mathlib.RingTheory.Polynomial.ContentIdeal

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Mathlib.RingTheory.Polynomial.DegreeLT

Mathlib.RingTheory.Polynomial.Dickson

Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Mathlib.RingTheory.Polynomial.GaussNorm

Mathlib.RingTheory.Polynomial.Hermite.Basic

Mathlib.RingTheory.Polynomial.HilbertPoly

Mathlib.RingTheory.Polynomial.IntegralNormalization

Mathlib.RingTheory.Polynomial.Opposites

Mathlib.RingTheory.Polynomial.Pochhammer

Mathlib.RingTheory.Polynomial.Quotient

Mathlib.RingTheory.Polynomial.Resultant.Basic

Mathlib.RingTheory.Polynomial.ScaleRoots

Mathlib.RingTheory.Polynomial.SeparableDegree

Mathlib.RingTheory.Polynomial.ShiftedLegendre

Mathlib.RingTheory.Polynomial.Subring

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Mathlib.RingTheory.Polynomial.Wronskian

Mathlib.RingTheory.PolynomialAlgebra

Mathlib.RingTheory.PolynomialLaw.Basic

Mathlib.RingTheory.PowerBasis

Mathlib.RingTheory.PowerSeries.Basic

Mathlib.RingTheory.PowerSeries.Binomial

Mathlib.RingTheory.PowerSeries.Catalan

Mathlib.RingTheory.PowerSeries.Derivative

Mathlib.RingTheory.PowerSeries.Evaluation

Mathlib.RingTheory.PowerSeries.Exp

Mathlib.RingTheory.PowerSeries.Expand

Mathlib.RingTheory.PowerSeries.GaussNorm

Mathlib.RingTheory.PowerSeries.Inverse

Mathlib.RingTheory.PowerSeries.Log

Mathlib.RingTheory.PowerSeries.Order

Mathlib.RingTheory.PowerSeries.Restricted

Mathlib.RingTheory.PowerSeries.Schroder

Mathlib.RingTheory.PowerSeries.Substitution

Mathlib.RingTheory.PowerSeries.Trunc

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Mathlib.RingTheory.PowerSeries.WellKnown

Mathlib.RingTheory.PrincipalIdealDomain

Mathlib.RingTheory.QuasiFinite.Basic

Mathlib.RingTheory.QuasiFinite.Weakly

Mathlib.RingTheory.QuotSMulTop

Mathlib.RingTheory.Radical.Basic

Mathlib.RingTheory.RamificationInertia.Inertia

Mathlib.RingTheory.RamificationInertia.Ramification

Mathlib.RingTheory.ReesAlgebra

Mathlib.RingTheory.Regular.Category

Mathlib.RingTheory.Regular.RegularSequence

Mathlib.RingTheory.RegularLocalRing.Defs

Mathlib.RingTheory.RingHom.Etale

Mathlib.RingTheory.RingHom.FaithfullyFlat

Mathlib.RingTheory.RingHom.Flat

Mathlib.RingTheory.RingHom.Locally

Mathlib.RingTheory.RingHom.OpenImmersion

Mathlib.RingTheory.RingHom.PurelyInseparable

Mathlib.RingTheory.RingHom.QuasiFinite

Mathlib.RingTheory.RingHom.Smooth