Definitions: Mathlib.RingTheory, part 1 of 6

AdicCompletion.AdicCauchySequence.subalgebradefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the subalgebra of I (from the name)

English

Let $I$ be an ideal of $R$. Then the subalgebra of $I$ is a subalgebra of $R$ and the set of functions from natural numbers to elements of $R$.

AdicCompletion.AdicCauchySequence.subringdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the subring of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the subring of $I$ is a subring of the set of functions from natural numbers to elements of $R$ defined as the subring of the subalgebra of $I$.

AdicCompletion.evalOneₐdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the evaluation one of I (from the name)

English

Let $I$ be an ideal of $R$. Then the evaluation one of $I$ is an algebra homomorphism of the set of adic completions of $I$ and $R$ and the set of quotients of $R$ and $I$.

AdicCompletion.evalₐdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the evaluation of I and n (from the name)

English

Let $I$ be an ideal of $R$. Let $n$ be a natural number. Then the evaluation of $I$ and $n$ is an algebra homomorphism of the set of adic completions of $I$ and $R$ and the set of quotients of $R$ and $I ^ {n}$.

AdicCompletion.kerProjdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the kernel projection of hf (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the kernel projection of $\mathrm{hf}$ is an algebra homomorphism of the set of adic completions of the kernel of $f$ and $S$ and $A$ defined as the composition of the algebra homomorphism of the quotient kernel algebra isomorphism of $\mathrm{hf}$ and $\operatorname{restrictScalars}$ applied to $R$ and the evaluation one of the kernel of $f$.

AdicCompletion.liftAlgHomdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the lift algebra homomorphism of I and f (from the name)

English

Let $I$ be an ideal of $S$. Let $f$ be a function from natural numbers $n_{1}$ to algebra homomorphisms of $A$ and the set of quotients of $S$ and $I ^ {n_{1}}$ such that for all natural numbers $m$ and $n$, for all elements $\mathrm{hle}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , n)$, the composition of the factor of $R$ and $\mathrm{Ideal\_\_pow\_le\_pow\_right}$ applied to $\mathrm{hle}$ and $f$ applied to $n$ is equal to $f$ applied to $m$. Then the lift algebra homomorphism of $I$ and $n_{1}$ is an algebra homomorphism of $A$ and the set of adic completions of $I$ and $S$.

AdicCompletion.liftRingHomdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the lift ring homomorphism of I and f (from the name)

English

Let $I$ be an ideal of $S$. Let $f$ be a function from natural numbers $n_{1}$ to ring homomorphisms of $R$ and the set of quotients of $S$ and $I ^ {n_{1}}$ such that for all natural numbers $m$ and $n$, for all elements $\mathrm{hle}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , n)$, the composition of the factor power of $I$ and $\mathrm{hle}$ and $f$ applied to $n$ is equal to $f$ applied to $m$. Then the lift ring homomorphism of $I$ and $n_{1}$ is a ring homomorphism of $R$ and the set of adic completions of $I$ and $S$.

AdicCompletion.mkₐdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Then $\mathrm{AdicCompletion\_\_mk\_u2090\_}$ applied to $I$ is an algebra homomorphism of the set of adic Cauchy sequences of $I$ and $R$ and the set of adic completions of $I$ and $R$.

AdicCompletion.ofAlgEquivdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the adic completion of I (from the name)

English

Let $I$ be an ideal of $S$. Then the adic completion of $I$ is an algebra isomorphism of $S$ and the set of adic completions of $I$ and $S$.

AdicCompletion.subalgebradefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the subalgebra of I (from the name)

English

Let $I$ be an ideal of $R$. Then the subalgebra of $I$ is a subalgebra of $R$ and the set of functions from elements $n$ of $\Natural$ to quotients of $R$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

AdicCompletion.subringdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the subring of I (from the name)

English

Let $I$ be an ideal of $R$. Then the subring of $I$ is a subring of the set of functions from elements $n$ of $\Natural$ to quotients of $R$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$ defined as the subring of the subalgebra of $I$.

AdicCompletion.transitionMapₐdefMathlib.RingTheory.AdicCompletion.Algebra, function or constant

Wording

the transition map of I and hmn (from the name)

English

Let $I$ be an ideal of $R$. Assume that $m \leq n$. Then the transition map of $I$ and $\mathrm{hmn}$ is an algebra homomorphism of the set of quotients of $R$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$ and the set of quotients of $R$ and $\HSMulhSMulMACRoAL {(I ^ {m})}{\operatorname{top}}$.

Mathlib.RingTheory.AdicCompletion.AsTensorProduct

AdicCompletion.ofTensorProductdefMathlib.RingTheory.AdicCompletion.AsTensorProduct, function or constant

Wording

the adic completion of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then the adic completion of $I$ and $M$ is a linear map of the set of tensor products of the set of adic completions of $I$ and $R$ and $M$ and the set of adic completions of $I$ and $M$.

AdicCompletion.ofTensorProductEquivOfFiniteNoetheriandefMathlib.RingTheory.AdicCompletion.AsTensorProduct, function or constant

Wording

the adic completion of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then the adic completion of $I$ and $M$ is a linear equivalence of the set of tensor products of the set of adic completions of $I$ and $R$ and $M$ and the set of adic completions of $I$ and $M$ defined as the linear equivalence of the adic completion of $I$ and $M$ and $\mathrm{AdicCompletion\_\_ofTensorProduct\_bijective\_of\_finite\_of\_isNoetherian}$ applied to $I$ and $M$.

AdicCompletion.ofTensorProductEquivOfPiFintypedefMathlib.RingTheory.AdicCompletion.AsTensorProduct, function or constant

Wording

the adic completion of I and x1 (from the name)

English

Let $I$ be an ideal of $R$. Let $x_{1}$ be a set. Then the adic completion of $I$ and $x_{1}$ is a linear equivalence of the set of tensor products of the set of adic completions of $I$ and $R$ and the set of functions from elements of $x_{1}$ to elements of $R$ and the set of adic completions of $I$ and the set of functions from elements of $x_{1}$ to elements of $R$ defined as the linear equivalence of the adic completion of $I$ and the set of functions from elements of $x_{1}$ to elements of $R$ and $\operatorname{toLinearMap}$ applied to the adic completion of $I$ and $x_{1}$.

AdicCompletion.ofTensorProductInvOfPiFintypedefMathlib.RingTheory.AdicCompletion.AsTensorProduct, function or constant

Wording

the adic completion of I and x1 (from the name)

English

Let $I$ be an ideal of $R$. Let $x_{1}$ be a set. Then the adic completion of $I$ and $x_{1}$ is a linear equivalence of the set of adic completions of $I$ and the set of functions from elements of $x_{1}$ to elements of $R$ and the set of tensor products of the set of adic completions of $I$ and $R$ and the set of functions from elements of $x_{1}$ to elements of $R$ defined as the composition of the product equivalence of $I$ and the function that maps $x_{4}$ to $R$ and the inverse of the right product scalar of the set of adic completions of $I$ and $R$ and $x_{1}$.

Mathlib.RingTheory.AdicCompletion.Basic

AdicCompletiondefMathlib.RingTheory.AdicCompletion.Basic, type

Wording

adic completion of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then an adic completion of $I$ and $M$ is an element of the function that maps $I$ and $M$ to $\SubtypeSet {f}{\mathrm{forall} (\Natural , \lambda m . \mathrm{forall} (\Natural , \lambda n . \mathrm{forall} (\mathrm{Proof} (\mathrm{Leq} (m , n)), \lambda \mathrm{hmn} . \EqtMACRoH {\operatorname{transitionMap} (I , M , \mathrm{hmn} , f (n))}{f (m)})))}$.

AdicCompletion.AdicCauchySequencedefMathlib.RingTheory.AdicCompletion.Basic, type

Wording

adic Cauchy sequence of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then an adic Cauchy sequence of $I$ and $M$ is an element of the function that maps $I$ and $M$ to $\SubtypeSet {f}{\operatorname{IsAdicCauchy} (I , M , f)}$.

AdicCompletion.AdicCauchySequence.mkdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Let $f$ be a function from elements of $\Natural$ to elements of $M$ such that for all elements $n$ of $\Natural$, $\mathrm{SModEq}$ holds for $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$, $f$ applied to $n$ and $f$ applied to $n + 1$. Then $\operatorname{mk}$ applied to $I$, $M$, $f$ and $h$ is an adic Cauchy sequence of $I$ and $M$ defined as $f$.

AdicCompletion.AdicCauchySequence.submoduledefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the submodule of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then the submodule of $I$ and $M$ is a submodule of $R$ and the set of functions from natural numbers to elements of $M$.

AdicCompletion.IsAdicCauchydefMathlib.RingTheory.AdicCompletion.Basic, predicate

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Let $f$ be a function from elements of $\Natural$ to elements of $M$. Then $\operatorname{IsAdicCauchy}$ holds for $I$, $M$ and $f$, if for all elements $m$ and $n$ of $\Natural$, if $m \leq n$, then $\mathrm{SModEq}$ holds for $\HSMulhSMulMACRoAL {(I ^ {m})}{\operatorname{top}}$, $f$ applied to $m$ and $f$ applied to $n$.

AdicCompletion.evaldefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the evaluation of I and n (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Let $n$ be an element of $\Natural$. Then the evaluation of $I$ and $n$ is a linear map of the set of adic completions of $I$ and $M$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

AdicCompletion.incldefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the canonical inclusion from the completion to the product of I and M (from the docstring)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then the canonical inclusion from the completion to the product of $I$ and $M$ is a linear map of the set of adic completions of $I$ and $M$ and the set of functions from elements $n$ of $\Natural$ to quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

AdicCompletion.liftdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the lift of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a function from elements $n_{1}$ of $\Natural$ to linear maps of $M$ and the set of quotients of $N$ and $\HSMulhSMulMACRoAL {(I ^ {n_{1}})}{\operatorname{top}}$ such that for all elements $m$ and $n$ of $\Natural$, for all elements $\mathrm{hle}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , n)$, $\EqtMACRoH {\operatorname{comp} (\operatorname{transitionMap} (I), f (n))}{f (m)}$. Then the lift of $I$ and $n_{1}$ is a linear map of $M$ and the set of adic completions of $I$ and $N$.

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

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then $\operatorname{mk}$ applied to $I$ and $M$ is a linear map of the set of adic Cauchy sequences of $I$ and $M$ and the set of adic completions of $I$ and $M$.

AdicCompletion.ofdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then $\operatorname{of}$ applied to $I$ and $M$ is a linear map of $M$ and the set of adic completions of $I$ and $M$.

AdicCompletion.ofLinearEquivdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the adic completion of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then the adic completion of $I$ and $M$ is a linear equivalence of $M$ and the set of adic completions of $I$ and $M$ defined as the linear equivalence of $\operatorname{of}$ applied to $I$ and $M$ and $\mathrm{AdicCompletion\_\_of\_bijective}$ applied to $I$ and $M$.

AdicCompletion.submoduledefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the submodule of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then the submodule of $I$ and $M$ is a submodule of $R$ and the set of functions from elements $n$ of $\Natural$ to quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

AdicCompletion.transitionMapdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the transition map of I (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Assume that $m \leq n$. Then the transition map of $I$ is a linear map of the set of quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {m})}{\operatorname{top}}$ defined as the factor power of $I$.

HausdorffificationdefMathlib.RingTheory.AdicCompletion.Basic, type

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then an element of $\mathrm{Hausdorffification}$ applied to $I$ and $M$ is an element of the function that maps $I$ and $M$ to the set of quotients of $M$ and the infimum of the function that maps $n$ to $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

Hausdorffification.liftdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the lift of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a linear map of $M$ and $N$. Then the lift of $I$ and $f$ is a linear map of $\mathrm{Hausdorffification}$ applied to $I$ and $M$ and $N$.

Hausdorffification.ofdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then $\operatorname{of}$ applied to $I$ and $M$ is a linear map of $M$ and $\mathrm{Hausdorffification}$ applied to $I$ and $M$ defined as $\operatorname{mkQ}$ applied to the infimum of the function that maps $n$ to $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

IsAdicCompleteclassMathlib.RingTheory.AdicCompletion.Basic, predicate

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then we can say that $\mathrm{IsAdicComplete}$ holds for $I$ and $M$.

IsAdicComplete.StrictMono.extenddefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{StrictMono}$ holds for $a$. Let $f$ be a function from elements $n_{1}$ of $\Natural$ to linear maps of $M$ and the set of quotients of $N$ and $\HSMulhSMulMACRoAL {(I ^ {a (n_{1})})}{\operatorname{top}}$. Let $n$ be an element of $\Natural$. Then $\operatorname{extend}$ applied to $\mathrm{ha}$, $n_{1}$, $f$ and $n$ is a linear map of $M$ and the set of quotients of $N$ and $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$ defined as the function that maps $n$ to the composition of the factor power of $I$ and $n_{1}$ applied to $f$.

IsAdicComplete.StrictMono.liftdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the lift of I and f (from the name)

English

Let $I$ be an ideal of $R$. Assume that $\mathrm{StrictMono}$ holds for $a$. Let $f$ be a function from elements $n$ of $\Natural$ to linear maps of $M$ and the set of quotients of $N$ and $\HSMulhSMulMACRoAL {(I ^ {a (n)})}{\operatorname{top}}$ such that for all elements $m$ of $\Natural$, $\EqtMACRoH {\operatorname{comp} (\operatorname{factorPow} (I), f (m + 1))}{f (m)}$. Then the lift of $I$ and $n$ is a linear map of $M$ and $N$.

IsAdicComplete.liftdefMathlib.RingTheory.AdicCompletion.Basic, function or constant

Wording

the lift of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a function from elements $n_{1}$ of $\Natural$ to linear maps of $M$ and the set of quotients of $N$ and $\HSMulhSMulMACRoAL {(I ^ {n_{1}})}{\operatorname{top}}$ such that for all elements $m$ and $n$ of $\Natural$, for all elements $\mathrm{hle}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , n)$, $\EqtMACRoH {\operatorname{comp} (\operatorname{factorPow} (I), f (n))}{f (m)}$. Then the lift of $I$ and $n_{1}$ is a linear map of $M$ and $N$ defined as the function that maps $h_{1}$ to the composition of $\operatorname{toLinearMap}$ applied to the inverse of the adic completion of $I$ and $N$ and the lift of $I$ and $n_{1}$.

IsHausdorffclassMathlib.RingTheory.AdicCompletion.Basic, predicate

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then we can say that $\mathrm{IsHausdorff}$ holds for $I$ and $M$.

IsPrecompleteclassMathlib.RingTheory.AdicCompletion.Basic, predicate

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then we can say that $\mathrm{IsPrecomplete}$ holds for $I$ and $M$.

Mathlib.RingTheory.AdicCompletion.Completeness

AdicCompletion.ofPowSMuldefMathlib.RingTheory.AdicCompletion.Completeness, function or constant

Wording

the canonical inclusion from the adic completion of I (from the docstring)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Let $n$ be an element of $\Natural$. Then the canonical inclusion from the adic completion of $I$ is a linear map of the set of adic completions of $I$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {(\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}})}{x_{3}})}$ and the set of adic completions of $I$ and $M$ defined as $\operatorname{map}$ applied to $I$ and the subtype of $\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}}$.

AdicCompletion.ofValEqZerodefMathlib.RingTheory.AdicCompletion.Completeness, function or constant

Wording

the adic completion of I and hxn (from the name)

English

Let $I$ be an ideal of $R$. Assume that $\EqtMACRoH {n}{0}$. Then the adic completion of $I$ and $\mathrm{hxn}$ is an adic completion of $I$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {(\HSMulhSMulMACRoAL {(I ^ {n})}{\operatorname{top}})}{x_{4}})}$.

Mathlib.RingTheory.AdicCompletion.Functoriality

AdicCompletion.AdicCauchySequence.mapdefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the map of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a linear map of $M$ and $N$. Then the map of $I$ and $f$ is a linear map of the set of adic Cauchy sequences of $I$ and $M$ and the set of adic Cauchy sequences of $I$ and $N$.

AdicCompletion.congrdefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the congruence of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a linear equivalence of $M$ and $N$. Then the congruence of $I$ and $f$ is a linear equivalence of the set of adic completions of $I$ and $M$ and the set of adic completions of $I$ and $N$.

AdicCompletion.mapdefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the map of I (from the name)

English

Let $I$ be an ideal of $R$. Then the map of $I$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of the set of adic completions of $I$ and $M$ and the set of adic completions of $I$ and $N$.

AdicCompletion.pidefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the product of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a function from elements of $x_{1}$ to sets. Then the product of $I$ and $M$ is a linear map of the set of adic completions of $I$ and the set of functions from elements $j$ of $x_{1}$ to elements of $M$ applied to $j$ and the set of functions from elements $j_{1}$ of $x_{1}$ to adic completions of $I$ and $M$ applied to $j_{1}$ defined as the product of the function that maps $j$ to $\operatorname{map}$ applied to $I$ and the projection of $j$.

AdicCompletion.piEquivFindefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $n$ be a natural number. Then $\operatorname{piEquivFin}$ applied to $I$ and $n$ is a linear equivalence of the set of adic completions of $I$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to adic completions of $I$ and $R$ defined as the product equivalence of $I$ and the function that maps $x_{1}$ to $R$.

AdicCompletion.piEquivOfFintypedefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the product equivalence of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a function from elements of $x_{1}$ to sets. Then the product equivalence of $I$ and $M$ is a linear equivalence of the set of adic completions of $I$ and the set of functions from elements $j$ of $x_{1}$ to elements of $M$ applied to $j$ and the set of functions from elements $j_{1}$ of $x_{1}$ to adic completions of $I$ and $M$ applied to $j_{1}$ defined as the composition of the inverse of the congruence of $I$ and the linear equivalence function on finite type of $M$ and the composition of the inverse of the sum equivalence of $I$ and $M$ and the linear equivalence function on finite type of the function that maps $j$ to the set of adic completions of $I$ and $M$ applied to $j$.

AdicCompletion.sumdefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the sum of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a function from elements of $x_{1}$ to sets. Then the sum of $I$ and $M$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $j$ to the set of adic completions of $I$ and $M$ applied to $j$ and the set of adic completions of $I$ and the set of direct sums of $x_{1}$ and the function that maps $j_{1}$ to $M$ applied to $j_{1}$ defined as the module of the function that maps $j_{1}$ to $\operatorname{map}$ applied to $I$ and $\operatorname{lof}$ applied to $R$, $x_{1}$, $M$ and $j_{1}$.

AdicCompletion.sumEquivOfFintypedefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the sum equivalence of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a function from elements of $x_{1}$ to sets. Then the sum equivalence of $I$ and $M$ is a linear equivalence of the set of direct sums of $x_{1}$ and the function that maps $j$ to the set of adic completions of $I$ and $M$ applied to $j$ and the set of adic completions of $I$ and the set of direct sums of $x_{1}$ and the function that maps $j_{1}$ to $M$ applied to $j_{1}$ defined as the linear equivalence of the sum of $I$ and $M$ and the sum inverse of $I$ and $M$.

AdicCompletion.sumInvdefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

the sum inverse of I and M (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a function from elements of $x_{1}$ to sets. Then the sum inverse of $I$ and $M$ is a linear map of the set of adic completions of $I$ and the set of direct sums of $x_{1}$ and the function that maps $j$ to $M$ applied to $j$ and the set of direct sums of $x_{1}$ and the function that maps $j_{1}$ to the set of adic completions of $I$ and $M$ applied to $j_{1}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence function on finite type of the function that maps $j$ to the set of adic completions of $I$ and $M$ applied to $j$ and the composition of the product of $I$ and $M$ and $\operatorname{map}$ applied to $I$ and $\operatorname{toLinearMap}$ applied to the linear equivalence function on finite type of $M$.

LinearMap.reduceModIdealdefMathlib.RingTheory.AdicCompletion.Functoriality, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Then $\operatorname{reduceModIdeal}$ applied to $I$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of the set of quotients of $M$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$ and the set of quotients of $N$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$.

Mathlib.RingTheory.AdicCompletion.RingHom

IsAdicComplete.StrictMono.liftRingHomdefMathlib.RingTheory.AdicCompletion.RingHom, function or constant

Wording

the lift ring homomorphism of I and f (from the name)

English

Let $I$ be an ideal of $S$. Assume that $\mathrm{StrictMono}$ holds for $a$. Let $f$ be a function from natural numbers $n$ to ring homomorphisms of $R$ and the set of quotients of $S$ and $I ^ {a (n)}$ such that for all natural numbers $m$, the composition of the factor power of $I$ and $\operatorname{monotone}$ applied to $\mathrm{ha}$, $m$, $m + 1$ and $\mathrm{Nat\_\_le\_succ}$ applied to $m$ and $f$ applied to $m + 1$ is equal to $f$ applied to $m$. Then the lift ring homomorphism of $I$ and $n$ is a ring homomorphism of $R$ and $S$.

IsAdicComplete.liftAlgHomdefMathlib.RingTheory.AdicCompletion.RingHom, function or constant

Wording

the lift algebra homomorphism of I and f (from the name)

English

IsAdicComplete.liftRingHomdefMathlib.RingTheory.AdicCompletion.RingHom, function or constant

Wording

the lift ring homomorphism of I and f (from the name)

English

Mathlib.RingTheory.Adjoin.FG

Subalgebra.FGdefMathlib.RingTheory.Adjoin.FG, predicate

Wording

no wording

English

Let $S$ be a subalgebra of $R$ and $A$. Then $\operatorname{FG}$ holds for $S$, if there exists a finite set $t$ of $A$, such that $\EqtMACRoH {\operatorname{adjoin} (R , t)}{S}$.

Mathlib.RingTheory.Adjoin.Field

AlgEquiv.adjoinSingletonEquivAdjoinRootMinpolydefMathlib.RingTheory.Adjoin.Field, function or constant

Wording

no wording

English

Let $F$ be a set. Let $x_{3}$ be an element of $R$. Then $\operatorname{adjoinSingletonEquivAdjoinRootMinpoly}$ applied to $F$ and $x_{3}$ is an algebra isomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{singleton} (x_{3}))}{x_{4}})}$ and $\mathrm{AdjoinRoot}$ applied to the minimal polynomial of $F$ and $x_{3}$.

Algebra.adjoin.liftSingletondefMathlib.RingTheory.Adjoin.Field, function or constant

Wording

the lift singleton of x5 and y (from the name)

English

Let $F$ be a set. Let $x_{5}$ be an element of $S$. Let $y$ be an element of $T$ such that $\operatorname{aeval}$ applied to $y$ and the minimal polynomial of $F$ and $x_{5}$ is equal to $0$. Then the lift singleton of $x_{5}$ and $y$ is an algebra homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{singleton} (x_{5}))}{x_{6}})}$ and $T$ defined as the composition of the lift algebra homomorphism of the algebra of $F$ and $T$ and $y$ and the algebra homomorphism of $\operatorname{adjoinSingletonEquivAdjoinRootMinpoly}$ applied to $F$ and $x_{5}$.

Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Polynomial.Bivariate.Transcendental.algEquivAdjoindefMathlib.RingTheory.Adjoin.Polynomial.Bivariate, function or constant

Wording

no wording

English

Assume that $x_{3}$ is transcendental. Then $\operatorname{algEquivAdjoin}$ applied to $\mathrm{hx}$ is an algebra isomorphism of the set of polynomials of the set of polynomials of $R$ and the set of polynomials of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$ defined as the map algebra isomorphism of the algebra isomorphism of $x_{3}$.

Mathlib.RingTheory.Adjoin.Polynomial.Transcendental

Algebra.adjoin.evalOfTranscendentaldefMathlib.RingTheory.Adjoin.Polynomial.Transcendental, function or constant

Wording

the evaluation of s and c (from the name)

English

Let $s$ be a transcendental element of $S$. Let $c$ be an element of $T$. Then the evaluation of $s$ and $c$ is an algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (s))}{x_{5}})}$ and $T$ defined as the composition of the algebra evaluation of $c$ and the algebra homomorphism of the inverse of the algebra isomorphism of $s$.

Polynomial.algEquivOfTranscendentaldefMathlib.RingTheory.Adjoin.Polynomial.Transcendental, function or constant

Wording

the algebra isomorphism of s (from the name)

English

Let $R$ be a set. Let $s$ be a transcendental element of $S$. Then the algebra isomorphism of $s$ is an algebra isomorphism of the set of polynomials of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (s))}{x_{3}})}$.

Mathlib.RingTheory.Adjoin.PowerBasis

Algebra.adjoin.powerBasisdefMathlib.RingTheory.Adjoin.PowerBasis, function or constant

Wording

the power basis of hx (from the docstring)

English

Assume that $x_{3}$ is integral. Then the power basis of $\mathrm{hx}$ is a power basis of $K$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (K , \operatorname{singleton} (x_{3}))}{x_{4}})}$.

PowerBasis.ofAdjoinEqTopdefMathlib.RingTheory.Adjoin.PowerBasis, function or constant

Wording

the power basis of hx and #2 (from the name)

English

Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $K$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then the power basis of $\mathrm{hx}$ and $\mathrm{hx'}$ is a power basis of $K$ and $S$ defined as the map of the power basis of $\mathrm{hx}$ and the composition of the equivalence of $\operatorname{adjoin}$ applied to $K$ and $\operatorname{singleton}$ applied to $x_{3}$ and the top and the top subalgebra.

Mathlib.RingTheory.Adjoin.Singleton

Algebra.RingHom.adjoinAlgebraMapdefMathlib.RingTheory.Adjoin.Singleton, function or constant

Wording

no wording

English

Let $b$ be an element of $B$. Then $\operatorname{adjoinAlgebraMap}$ applied to $b$ is a ring homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (A , \operatorname{singleton} (b))}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{adjoin} (A , \operatorname{singleton} (\operatorname{algebraMap} (B , C , b)))}{x_{7}})}$.

Algebra.RingHom.adjoinAlgebraMapEquivdefMathlib.RingTheory.Adjoin.Singleton, function or constant

Wording

no wording

English

Let $b$ be an element of $B$. Then $\operatorname{adjoinAlgebraMapEquiv}$ applied to $b$ is a ring isomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (A , \operatorname{singleton} (b))}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{adjoin} (A , \operatorname{singleton} (\operatorname{algebraMap} (B , C , b)))}{x_{7}})}$.

Mathlib.RingTheory.AdjoinRoot

AdjoinRootdefMathlib.RingTheory.AdjoinRoot, type

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then an element of $\mathrm{AdjoinRoot}$ applied to $f$ is an element of the function that maps $f$ to the set of quotients of the set of polynomials of $R$ and the span of $\operatorname{singleton}$ applied to $f$.

AdjoinRoot.Minpoly.toAdjoindefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{3}$ be an element of $S$. Then $\operatorname{toAdjoin}$ applied to $R$ and $x_{3}$ is an algebra homomorphism of $\mathrm{AdjoinRoot}$ applied to the minimal polynomial of $R$ and $x_{3}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$.

AdjoinRoot.Polynomial.quotQuotEquivCommdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $f$ be a polynomial of $R$. Then $\operatorname{quotQuotEquivComm}$ applied to $I$ and $f$ is a ring isomorphism of the set of quotients of the set of polynomials of the set of quotients of $R$ and $I$ and the span of $\operatorname{singleton}$ applied to the map of $\operatorname{mk}$ applied to $I$ and $f$ and the set of quotients of the set of quotients of the set of polynomials of $R$ and the map of $\operatorname{C}$ and $I$ and the span of $\operatorname{singleton}$ applied to $\operatorname{mk}$ applied to the map of $\operatorname{C}$ and $I$ and $f$.

AdjoinRoot.algEquivOfAssociateddefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the algebra isomorphism of f and g (from the name)

English

Let $R$ be a set. Let $f$ and $g$ be polynomials of $S$ such that $\mathrm{Associated}$ holds for $f$ and $g$. Then the algebra isomorphism of $f$ and $g$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $f$ and $\mathrm{AdjoinRoot}$ applied to $g$.

AdjoinRoot.algEquivOfEqdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the algebra isomorphism of f and g (from the name)

English

Let $R$ be a set. Let $f$ and $g$ be polynomials of $S$ such that $\EqtMACRoH {f}{g}$. Then the algebra isomorphism of $f$ and $g$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $f$ and $\mathrm{AdjoinRoot}$ applied to $g$.

AdjoinRoot.algHomOfDvddefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the algebra homomorphism of f and g (from the name)

English

Let $R$ be a set. Let $f$ and $g$ be polynomials of $S$ such that $g$ divides $f$. Then the algebra homomorphism of $f$ and $g$ is an algebra homomorphism of $\mathrm{AdjoinRoot}$ applied to $f$ and $\mathrm{AdjoinRoot}$ applied to $g$.

AdjoinRoot.compAlgEquivdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the composition algebra isomorphism of f and g (from the name)

English

Let $f$ and $g$ be polynomials of $R$. Then the composition algebra isomorphism of $f$ and $g$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to the composition of $f$ and $g$ and $\mathrm{AdjoinRoot}$ applied to the difference between the map of $\operatorname{of}$ applied to $f$ and $g$ and $\operatorname{C}$ applied to the adjoined root of $f$.

AdjoinRoot.equivdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the equivalence of f (from the name)

English

Let $L$ and $F$ be sets. Let $f$ be a polynomial of $F$ such that $f \neq 0$. Then the equivalence of $f$ is an equivalence from the set of algebra homomorphisms of $\mathrm{AdjoinRoot}$ applied to $f$ and $L$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{aroots} (f , L)}{x_{3}})}$.

AdjoinRoot.equiv'defMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the equivalence of g and pb (from the name)

English

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

AdjoinRoot.liftdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the lift of i and x2 (from the name)

English

Let $i$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be an element of $S$ such that the evaluation of $x_{2}$ and $f$ is equal to $0$. Then the lift of $i$ and $x_{2}$ is a ring homomorphism of $\mathrm{AdjoinRoot}$ applied to $f$ and $S$.

AdjoinRoot.liftAlgHomdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the lift algebra homomorphism of i and x5 (from the name)

English

Let $p$ be a polynomial of $R$. Let $i$ be an algebra homomorphism of $R$ and $T$. Let $x_{5}$ be an element of $T$ such that the evaluation of $x_{5}$ and $p$ is equal to $0$. Then the lift algebra homomorphism of $i$ and $x_{5}$ is an algebra homomorphism of $\mathrm{AdjoinRoot}$ applied to $p$ and $T$.

AdjoinRoot.mapdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the map of p and q (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $p$ be a polynomial of $R$. Let $q$ be a polynomial of $S$ such that $q$ divides the map of $f$ and $p$. Then the map of $p$ and $q$ is a ring homomorphism of $\mathrm{AdjoinRoot}$ applied to $p$ and $\mathrm{AdjoinRoot}$ applied to $q$.

AdjoinRoot.mapAlgEquivdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the map algebra isomorphism of p and q (from the name)

English

Let $f$ be an algebra isomorphism of $S$ and $T$. Let $p$ be a polynomial of $S$. Let $q$ be a polynomial of $T$ such that $\mathrm{Associated}$ holds for the map of the ring homomorphism of $f$ and $p$ and $q$. Then the map algebra isomorphism of $p$ and $q$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $p$ and $\mathrm{AdjoinRoot}$ applied to $q$.

AdjoinRoot.mapAlgHomdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the map algebra homomorphism of p and q (from the name)

English

Let $f$ be an algebra homomorphism of $S$ and $T$. Let $p$ be a polynomial of $S$. Let $q$ be a polynomial of $T$ such that $q$ divides the map of the ring homomorphism of $f$ and $p$. Then the map algebra homomorphism of $p$ and $q$ is an algebra homomorphism of $\mathrm{AdjoinRoot}$ applied to $p$ and $\mathrm{AdjoinRoot}$ applied to $q$.

AdjoinRoot.mapRingEquivdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the map ring isomorphism of p and q (from the name)

English

Let $f$ be a ring isomorphism of $R$ and $S$. Let $p$ be a polynomial of $R$. Let $q$ be a polynomial of $S$ such that $\mathrm{Associated}$ holds for the map of the ring homomorphism of $f$ and $p$ and $q$. Then the map ring isomorphism of $p$ and $q$ is a ring isomorphism of $\mathrm{AdjoinRoot}$ applied to $p$ and $\mathrm{AdjoinRoot}$ applied to $q$.

AdjoinRoot.mkdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then $\operatorname{mk}$ applied to $f$ is a ring homomorphism of the set of polynomials of $R$ and $\mathrm{AdjoinRoot}$ applied to $f$ defined as $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to $f$.

AdjoinRoot.mkₐdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then $\mathrm{AdjoinRoot\_\_mk\_u2090\_}$ applied to $f$ is an algebra homomorphism of the set of polynomials of $R$ and $\mathrm{AdjoinRoot}$ applied to $f$ defined as $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and the span of $\operatorname{singleton}$ applied to $f$.

AdjoinRoot.modByMonicHomdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Assume that $g$ is monic. Then $\operatorname{modByMonicHom}$ applied to $\mathrm{hg}$ is a linear map of $\mathrm{AdjoinRoot}$ applied to $g$ and the set of polynomials of $R$.

AdjoinRoot.ofdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then $\operatorname{of}$ applied to $f$ is a ring homomorphism of $R$ and $\mathrm{AdjoinRoot}$ applied to $f$ defined as the composition of $\operatorname{mk}$ applied to $f$ and $\operatorname{C}$.

AdjoinRoot.ofAlgHomdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $S$ be a set. Let $p$ be a polynomial of $R$. Then $\operatorname{ofAlgHom}$ applied to $S$ and $p$ is an algebra homomorphism of $R$ and $\mathrm{AdjoinRoot}$ applied to $p$ defined as the algebra homomorphism of $R$ and $\mathrm{AdjoinRoot}$ applied to $p$.

AdjoinRoot.powerBasisdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the power basis of hf (from the docstring)

English

Assume that $f \neq 0$. Then the power basis of $\mathrm{hf}$ is a power basis of $K$ and $\mathrm{AdjoinRoot}$ applied to $f$.

AdjoinRoot.powerBasis'defMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the power basis of hg (from the docstring)

English

Assume that $g$ is monic. Then the power basis of $\mathrm{hg}$ is a power basis of $R$ and $\mathrm{AdjoinRoot}$ applied to $g$.

AdjoinRoot.powerBasisAux'defMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the power basis of hg (from the name)

English

Assume that $g$ is monic. Then the power basis of $\mathrm{hg}$ is a basis of $R$ and $\mathrm{AdjoinRoot}$ applied to $g$.

AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuotdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $f$ be a polynomial of $R$. Then $\operatorname{quotAdjoinRootEquivQuotPolynomialQuot}$ applied to $I$ and $f$ is a ring isomorphism of the set of quotients of $\mathrm{AdjoinRoot}$ applied to $f$ and the map of $\operatorname{of}$ applied to $f$ and $I$ and the set of quotients of the set of polynomials of the set of quotients of $R$ and $I$ and the span of $\operatorname{singleton}$ applied to the map of $\operatorname{mk}$ applied to $I$ and $f$.

AdjoinRoot.quotEquivQuotMapdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the quotient equivalence quotient map of f and I (from the name)

English

Let $f$ be a polynomial of $R$. Let $I$ be an ideal of $R$. Then the quotient equivalence quotient map of $f$ and $I$ is an algebra isomorphism of the set of quotients of $\mathrm{AdjoinRoot}$ applied to $f$ and the map of $\operatorname{of}$ applied to $f$ and $I$ and the set of quotients of the set of polynomials of the set of quotients of $R$ and $I$ and the span of $\operatorname{singleton}$ applied to the map of $\operatorname{mk}$ applied to $I$ and $f$.

AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMkdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the quotient map map span equivalence quotient map quotient map of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a polynomial of $R$. Then the quotient map map span equivalence quotient map quotient map of $I$ and $f$ is a ring isomorphism of the set of quotients of $\mathrm{AdjoinRoot}$ applied to $f$ and the map of $\operatorname{mk}$ applied to $f$ and the map of $\operatorname{C}$ and $I$ and the set of quotients of the set of quotients of the set of polynomials of $R$ and the map of $\operatorname{C}$ and $I$ and the map of $\operatorname{mk}$ applied to the map of $\operatorname{C}$ and $I$ and the span of $\operatorname{singleton}$ applied to $f$ defined as $\operatorname{quotQuotEquivComm}$ applied to the span of $\operatorname{singleton}$ applied to $f$ and the map of $\operatorname{C}$ and $I$.

AdjoinRoot.quotMapOfEquivQuotMapCMapMkdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the quotient map of I and f (from the name)

English

Let $I$ be an ideal of $R$. Let $f$ be a polynomial of $R$. Then the quotient map of $I$ and $f$ is a ring isomorphism of the set of quotients of $\mathrm{AdjoinRoot}$ applied to $f$ and the map of $\operatorname{of}$ applied to $f$ and $I$ and the set of quotients of $\mathrm{AdjoinRoot}$ applied to $f$ and the map of $\operatorname{mk}$ applied to $f$ and the map of $\operatorname{C}$ and $I$.

AdjoinRoot.rootdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the adjoined root of f (from the docstring)

English

Let $f$ be a polynomial of $R$. Then the adjoined root of $f$ is an element of $\mathrm{AdjoinRoot}$ applied to $f$ defined as $\operatorname{mk}$ applied to $f$ and $\operatorname{X}$.

AdjoinRoot.tensorAlgEquivdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the tensor algebra isomorphism of p and q (from the name)

English

Let $p$ be a polynomial of $S$. Let $q$ be a polynomial of the set of tensor products of $T$ and $S$ such that the map of $\operatorname{toRingHom}$ applied to $\operatorname{includeRight}$ and $p$ is equal to $q$. Then the tensor algebra isomorphism of $p$ and $q$ is an algebra isomorphism of the set of tensor products of $T$ and $\mathrm{AdjoinRoot}$ applied to $p$ and $\mathrm{AdjoinRoot}$ applied to $q$.

PowerBasis.quotientEquivQuotientMinpolyMapdefMathlib.RingTheory.AdjoinRoot, function or constant

Wording

the quotient equivalence quotient minimal polynomial map of pb and I (from the name)

English

Let $\mathrm{pb}$ be a power basis of $R$ and $S$. Let $I$ be an ideal of $R$. Then the quotient equivalence quotient minimal polynomial map of $\mathrm{pb}$ and $I$ is an algebra isomorphism of the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $I$ and the set of quotients of the set of polynomials of the set of quotients of $R$ and $I$ and the span of $\operatorname{singleton}$ applied to the map of $\operatorname{mk}$ applied to $I$ and the minimal polynomial of $R$ and the generator of $\mathrm{pb}$.

Mathlib.RingTheory.AlgebraTower

AlgHom.domRestrictdefMathlib.RingTheory.AlgebraTower, function or constant

Wording

no wording

English

Let $B$ be a set. Let $f$ be an algebra homomorphism of $C$ and $D$. Then $\operatorname{domRestrict}$ applied to $B$ and $f$ is an algebra homomorphism of $B$ and $D$ defined as the composition of $f$ and the algebra homomorphism of $B$ and $C$.

AlgHom.extendScalarsdefMathlib.RingTheory.AlgebraTower, function or constant

Wording

no wording

English

Let $B$ be a set. Let $f$ be an algebra homomorphism of $C$ and $D$. Then $\operatorname{extendScalars}$ applied to $B$ and $f$ is an algebra homomorphism of $C$ and $D$.

Module.Basis.algebraMapCoeffsdefMathlib.RingTheory.AlgebraTower, function or constant

Wording

no wording

English

Let $A$ be a set. Let $b$ be a basis of $R$ and $M$. Assume that $\operatorname{coe}$ applied to the algebra map of $R$ and $A$ is bijective. Then $\operatorname{algebraMapCoeffs}$ applied to $A$, $b$ and $h_{1}$ is a basis of $A$ and $M$.

Module.Basis.smulTowerdefMathlib.RingTheory.AlgebraTower, function or constant

Wording

the scalar multiple tower of b and c (from the name)

English

Let $b$ be a basis of $R$ and $S$. Let $c$ be a basis of $S$ and $A$. Then the scalar multiple tower of $b$ and $c$ is a basis of $R$ and $A$ defined as $\operatorname{ofRepr}$ applied to the composition of $\operatorname{restrictScalars}$ applied to $R$ and the representation of $c$ and the composition of $\operatorname{lcongr}$ applied to the identity of $x_{7}$ and the representation of $b$ and the composition of the inverse of the curry linear equivalence of $R$ and $\operatorname{lcongr}$ applied to $\operatorname{prodComm}$ applied to $x_{7}$ and $x_{6}$ and the identity map of $R$ and $R$.

Module.Basis.smulTower'defMathlib.RingTheory.AlgebraTower, function or constant

Wording

the scalar multiple tower of b and c (from the name)

English

Let $b$ be a basis of $R$ and $S$. Let $c$ be a basis of $S$ and $A$. Then the scalar multiple tower of $b$ and $c$ is a basis of $R$ and $A$ defined as the reindexing of the scalar multiple tower of $b$ and $c$ and $\operatorname{prodComm}$ applied to $x_{6}$ and $x_{7}$.

algHomEquivSigmadefMathlib.RingTheory.AlgebraTower, function or constant

Wording

the algebra homomorphism equivalence sigma (from the name)

English

The algebra homomorphism equivalence sigma is an equivalence from the set of algebra homomorphisms of $C$ and $D$ to $\Sigma$ applied to the function that maps $f$ to the set of algebra homomorphisms of $C$ and $D$.

Mathlib.RingTheory.Algebraic.Basic

Algebra.IsAlgebraic.algEquivEquivAlgHomdefMathlib.RingTheory.Algebraic.Basic, function or constant

Wording

the algebra isomorphism equivalence algebra homomorphism of K and L (from the name)

English

Let $K$ and $L$ be sets. Then the algebra isomorphism equivalence algebra homomorphism of $K$ and $L$ is a multiplicative equivalence of the set of algebra isomorphisms of $L$ and $L$ and the set of algebra homomorphisms of $L$ and $L$.

Mathlib.RingTheory.Algebraic.Defs

Algebra.IsAlgebraicclassMathlib.RingTheory.Algebraic.Defs, predicate

Wording

R is algebraic (from the docstring)

English

Let $R$ and $A$ be sets. Then we can say that $R$ is algebraic.

Algebra.TranscendentalclassMathlib.RingTheory.Algebraic.Defs, predicate

Wording

R is transcendental (from the docstring)

English

Let $R$ and $A$ be sets. Then we can say that $R$ is transcendental.

IsAlgebraicdefMathlib.RingTheory.Algebraic.Defs, predicate

Wording

x3 is algebraic (from the name)

English

Let $R$ be a set. Let $x_{3}$ be an element of $A$. Then $x_{3}$ is algebraic, if there exists a polynomial $p$ of $R$, such that $p \neq 0$ and $\EqtMACRoH {\operatorname{aeval} (x_{3} , p)}{0}$.

Subalgebra.IsAlgebraicdefMathlib.RingTheory.Algebraic.Defs, predicate

Wording

S is algebraic (from the docstring)

English

Let $S$ be a subalgebra of $R$ and $A$. Then $S$ is algebraic, if for all elements $x_{3}$ of $A$, if $x_{3}$ is an element of $S$, then $x_{3}$ is algebraic.

TranscendentaldefMathlib.RingTheory.Algebraic.Defs, predicate

Wording

x3 is transcendental (from the name)

English

Let $R$ be a set. Let $x_{3}$ be an element of $A$. Then $x_{3}$ is transcendental, if $x_{3}$ is not algebraic.

Mathlib.RingTheory.Algebraic.Denominator

Algebra.denominatordefMathlib.RingTheory.Algebraic.Denominator, function or constant

Wording

the denominator of R and x3 (from the docstring)

English

Let $R$ be a set. Let $x_{3}$ be an element of $S$. Then the denominator of $R$ and $x_{3}$ is an element of $R$ defined as the generator of the colon of $\operatorname{toSubmodule}$ applied to the integral closure of $R$ and $S$ and $\operatorname{singleton}$ applied to $x_{3}$.

Algebra.natDenominatordefMathlib.RingTheory.Algebraic.Denominator, function or constant

Wording

the natural denominator of x1 (from the name)

English

Let $x_{1}$ be an element of $S$. Then the natural denominator of $x_{1}$ is a natural number defined as the absolute value of the denominator of $\Integer$ and $x_{1}$.

Mathlib.RingTheory.Algebraic.Integral

Subalgebra.algebraicClosuredefMathlib.RingTheory.Algebraic.Integral, function or constant

Wording

the algebraic closure of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the algebraic closure of $R$ and $S$ is a subalgebra of $R$ and $S$.

algEquivEquivAlgHomdefMathlib.RingTheory.Algebraic.Integral, function or constant

Wording

the algebra isomorphism equivalence algebra homomorphism of K and L (from the name)

English

Mathlib.RingTheory.Algebraic.StronglyTranscendental

IsStronglyTranscendentaldefMathlib.RingTheory.Algebraic.StronglyTranscendental, predicate

Wording

no wording

English

Let $R$ be a set. Let $x_{3}$ be an element of $S$. Then $\mathrm{IsStronglyTranscendental}$ holds for $R$ and $x_{3}$, if for all elements $u$ of $S$, for all polynomials $p$ of $R$, if $\EqtMACRoH {\operatorname{aeval} (x_{3} , p)\times u}{0}$, then the product of the map of the algebra map of $R$ and $S$ and $p$ and $\operatorname{C}$ applied to $u$ is equal to $0$.

Mathlib.RingTheory.AlgebraicIndependent.Adjoin

AlgebraicIndependent.aevalEquivFielddefMathlib.RingTheory.AlgebraicIndependent.Adjoin, function or constant

Wording

the algebra evaluation equivalence field of hx (from the name)

English

Assume that $\mathrm{AlgebraicIndependent}$ holds for $F$ and $x_{1}$. Then the algebra evaluation equivalence field of $\mathrm{hx}$ is an algebra isomorphism of the set of fraction rings of the set of multivariate polynomials of $x$ and $F$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{range} (x_{1}))}{x_{5}})}$.

AlgebraicIndependent.reprFielddefMathlib.RingTheory.AlgebraicIndependent.Adjoin, function or constant

Wording

the representation field of hx (from the name)

English

Assume that $\mathrm{AlgebraicIndependent}$ holds for $F$ and $x_{1}$. Then the representation field of $\mathrm{hx}$ is an algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (F , \operatorname{range} (x_{1}))}{x_{5}})}$ and the set of fraction rings of the set of multivariate polynomials of $x$ and $F$ defined as the algebra homomorphism of the inverse of the algebra evaluation equivalence field of $\mathrm{hx}$.

Mathlib.RingTheory.AlgebraicIndependent.Basic

Algebra.trdegdefMathlib.RingTheory.AlgebraicIndependent.Basic, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{trdeg}$ applied to $R$ and $A$ is a cardinal defined as the supremum of the function that maps $x_{3}$ to $\operatorname{mk}$ applied to the set of elements of $x_{3}$.

AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoindefMathlib.RingTheory.AlgebraicIndependent.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{AlgebraicIndependent}$ holds for $R$ and $x_{1}$. Then $\operatorname{mvPolynomialOptionEquivPolynomialAdjoin}$ applied to $\mathrm{hx}$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Option}$ applied to $x$ and $R$ and the set of polynomials of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{range} (x_{1}))}{x_{5}})}$ defined as the composition of the left option equivalence of $R$ and $x$ and the map algebra isomorphism of the algebra evaluation equivalence of $\mathrm{hx}$.

Mathlib.RingTheory.AlgebraicIndependent.Defs

AlgebraicIndepOndefMathlib.RingTheory.AlgebraicIndependent.Defs, predicate

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to elements of $A$. Let $s$ be an element of $\wp x$. Then $\mathrm{AlgebraicIndepOn}$ holds for $R$, $x_{1}$ and $s$, if $\mathrm{AlgebraicIndependent}$ holds for $R$ and the function that maps $i$ to $x_{1}$ applied to $i$.

AlgebraicIndepOn.aevalEquivdefMathlib.RingTheory.AlgebraicIndependent.Defs, function or constant

Wording

the algebra evaluation equivalence of hx (from the name)

English

Assume that $\mathrm{AlgebraicIndepOn}$ holds for $R$, $x_{1}$ and $s$. Then the algebra evaluation equivalence of $\mathrm{hx}$ is an algebra isomorphism of the set of multivariate polynomials of the set of elements of $s$ and $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{image} (x_{1} , s))}{x_{5}})}$.

AlgebraicIndependentdefMathlib.RingTheory.AlgebraicIndependent.Defs, predicate

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to elements of $A$. Then $\mathrm{AlgebraicIndependent}$ holds for $R$ and $x_{1}$, if $\operatorname{coe}$ applied to the algebra evaluation of $x_{1}$ is injective.

AlgebraicIndependent.aevalEquivdefMathlib.RingTheory.AlgebraicIndependent.Defs, function or constant

Wording

the algebra evaluation equivalence of hx (from the name)

English

Assume that $\mathrm{AlgebraicIndependent}$ holds for $R$ and $x_{1}$. Then the algebra evaluation equivalence of $\mathrm{hx}$ is an algebra isomorphism of the set of multivariate polynomials of $x$ and $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{range} (x_{1}))}{x_{5}})}$.

AlgebraicIndependent.reprdefMathlib.RingTheory.AlgebraicIndependent.Defs, function or constant

Wording

the representation of hx (from the name)

English

Assume that $\mathrm{AlgebraicIndependent}$ holds for $R$ and $x_{1}$. Then the representation of $\mathrm{hx}$ is an algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{range} (x_{1}))}{x_{5}})}$ and the set of multivariate polynomials of $x$ and $R$ defined as the algebra homomorphism of the inverse of the algebra evaluation equivalence of $\mathrm{hx}$.

IsTranscendenceBasisdefMathlib.RingTheory.AlgebraicIndependent.Defs, predicate

Wording

R is a transcendence basis (from the docstring)

English

Let $R$ be a set. Let $x_{4}$ be a function from elements of $x$ to elements of $A$. Then $R$ is a transcendence basis, if $\mathrm{AlgebraicIndependent}$ holds for $R$ and $x_{4}$ and for all elements $s$ of $\wp A$, if $\mathrm{AlgebraicIndepOn}$ holds for $R$, $\mathrm{id}$ and $s$, then if the range of $x_{4}$ is less than or equal to $s$, then the range of $x_{4}$ is equal to $s$.

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

AlgebraicIndependent.matroiddefMathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis, function or constant

Wording

the matroid of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the matroid of $R$ and $A$ is a matroid of $A$.

Mathlib.RingTheory.Artinian.Defs

IsArtiniandefMathlib.RingTheory.Artinian.Defs, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\mathrm{IsArtinian}$ holds for $R$ and $M$, if $\mathrm{WellFoundedLT}$ holds for the set of submodules of $R$ and $M$.

IsArtinianRingdefMathlib.RingTheory.Artinian.Defs, predicate

Wording

R is a Artinian ring (from the name)

English

Let $R$ be a set. Then $R$ is an Artinian ring, if $\mathrm{IsArtinian}$ holds for $R$ and $R$.

Mathlib.RingTheory.Artinian.Module

IsArtinianRing.equivPidefMathlib.RingTheory.Artinian.Module, function or constant

Wording

the equivalence product of R (from the name)

English

Let $R$ be a set. Then the equivalence product of $R$ is an algebra isomorphism of $R$ and the set of functions from maximal spectra $I$ of $R$ to quotients of $R$ and $\operatorname{asIdeal}$ applied to $I$.

IsArtinianRing.primeSpectrumEquivMaximalSpectrumdefMathlib.RingTheory.Artinian.Module, function or constant

Wording

the prime spectrum (from the docstring)

English

The prime spectrum is an equivalence from the set of prime spectra of $R$ to the set of maximal spectra of $R$.

IsArtinianRing.quotNilradicalEquivPidefMathlib.RingTheory.Artinian.Module, function or constant

Wording

the quotient of R (from the docstring)

English

Let $R$ be a set. Then the quotient of $R$ is an algebra isomorphism of the set of quotients of $R$ and the nilradical of $R$ and the set of functions from maximal spectra $I$ of $R$ to quotients of $R$ and $\operatorname{asIdeal}$ applied to $I$.

IsArtinianRing.quotNilradicalPowEquivPidefMathlib.RingTheory.Artinian.Module, function or constant

Wording

the quotient of R and n (from the docstring)

English

Let $R$ be a set. Let $n$ be a natural number. Then the quotient of $R$ and $n$ is an algebra isomorphism of the set of quotients of $R$ and the exponentiation of the nilradical of $R$ to $n$ and the set of functions from maximal spectra $I$ of $R$ to quotients of $R$ and $\operatorname{asIdeal} (I)^ {n}$.

Mathlib.RingTheory.Bialgebra.Basic

BialgebraclassMathlib.RingTheory.Bialgebra.Basic, predicate

Wording

A is a bialgebra with respect to R (from the name)

English

Let $R$ and $A$ be sets. Then we can say that $A$ is a bialgebra with respect to $R$.

Bialgebra.comulAlgHomdefMathlib.RingTheory.Bialgebra.Basic, function or constant

Wording

no wording

English

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

Bialgebra.counitAlgHomdefMathlib.RingTheory.Bialgebra.Basic, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the counit algebra homomorphism of $R$ and $A$ is an algebra homomorphism of $A$ and $R$ defined as the algebra homomorphism of the counit of the coalgebra.

Mathlib.RingTheory.Bialgebra.Equiv

BialgEquivstructureMathlib.RingTheory.Bialgebra.Equiv, type

Wording

bialgebra equivalence of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the bialgebra equivalences of $A$ and $B$ are a basic type.

BialgEquiv.ofAlgEquivdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the bialgebra equivalence of f (from the name)

English

Let $f$ be an algebra isomorphism of $A$ and $B$ such that the composition of the counit algebra homomorphism of $R$ and $B$ and the algebra homomorphism of $f$ is equal to the counit algebra homomorphism of $R$ and $A$ and the composition of the map of the algebra homomorphism of $f$ and the algebra homomorphism of $f$ and $\operatorname{comulAlgHom}$ applied to $R$ and $A$ is equal to the composition of $\operatorname{comulAlgHom}$ applied to $R$ and $B$ and the algebra homomorphism of $f$. Then the bialgebra equivalence of $f$ is a bialgebra equivalence of $A$ and $B$.

BialgEquiv.ofBialgHomdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the bialgebra equivalence of f and g (from the name)

English

Let $f$ be a bialgebra homomorphism of $A$ and $B$. Let $g$ be a bialgebra homomorphism of $B$ and $A$ such that the composition of $f$ and $g$ is equal to the identity of $R$ and $B$ and the composition of $g$ and $f$ is equal to the identity of $R$ and $A$. Then the bialgebra equivalence of $f$ and $g$ is a bialgebra equivalence of $A$ and $B$.

BialgEquiv.ofBijectivedefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the bialgebra equivalence of f and hf (from the name)

English

Let $f$ be a bialgebra homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the bialgebra equivalence of $f$ and $\mathrm{hf}$ is a bialgebra equivalence of $A$ and $B$.

BialgEquiv.refldefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the identity map of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the identity map of $R$ and $A$ is a bialgebra equivalence of $A$ and $A$ defined as $\operatorname{mk}$ applied to the identity map of $R$ and $A$ and $\mathrm{BialgHom\_\_map\_mul'}$ applied to the identity of $R$ and $A$.

BialgEquiv.symmdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be a bialgebra equivalence of $A$ and $B$. Then the inverse of $e$ is a bialgebra equivalence of $B$ and $A$.

BialgEquiv.toAlgEquivdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the algebra isomorphism of f (from the name)

English

Let $f$ be a bialgebra equivalence of $A$ and $B$. Then the algebra isomorphism of $f$ is an algebra isomorphism of $A$ and $B$.

BialgEquiv.toBialgHomdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the bialgebra homomorphism of f (from the name)

English

Let $f$ be a bialgebra equivalence of $A$ and $B$. Then the bialgebra homomorphism of $f$ is a bialgebra homomorphism of $A$ and $B$.

BialgEquiv.toEquivdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the equivalence of x7 (from the name)

English

Let $x_{7}$ be a bialgebra equivalence of $A$ and $B$. Then the equivalence of $x_{7}$ is an equivalence from $A$ to $B$ defined as the equivalence of $\operatorname{toCoalgEquiv}$ applied to $x_{7}$.

BialgEquiv.toMulEquivdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the multiplicative equivalence of self (from the name)

English

Let $\mathrm{self}$ be a bialgebra equivalence of $A$ and $B$. Then the multiplicative equivalence of $\mathrm{self}$ is a multiplicative equivalence of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddHom}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toCoalgHom}$ applied to $\operatorname{toCoalgEquiv}$ applied to $\mathrm{self}$, $\operatorname{invFun}$ applied to $\operatorname{toCoalgEquiv}$ applied to $\mathrm{self}$, $\mathrm{CoalgEquiv\_\_left\_inv}$ applied to $\operatorname{toCoalgEquiv}$ applied to $\mathrm{self}$ and $\mathrm{CoalgEquiv\_\_right\_inv}$ applied to $\operatorname{toCoalgEquiv}$ applied to $\mathrm{self}$ and $\mathrm{BialgEquiv\_\_map\_mul'}$ applied to $\mathrm{self}$.

BialgEquiv.transdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a bialgebra equivalence of $A$ and $B$. Let $x_{11}$ be a bialgebra equivalence of $B$ and $C$. Then the composition of $x_{10}$ and $x_{11}$ is a bialgebra equivalence of $A$ and $C$.

BialgEquivClassclassMathlib.RingTheory.Bialgebra.Equiv, predicate

Wording

no wording

English

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

BialgEquivClass.toBialgEquivdefMathlib.RingTheory.Bialgebra.Equiv, function or constant

Wording

the bialgebra equivalence of f (from the name)

English

Let $f$ be an element of $F$. Then the bialgebra equivalence of $f$ is a bialgebra equivalence of $A$ and $B$ defined as $\operatorname{mk}$ applied to the coalgebra equivalence of $f$ and $\mathrm{BialgHom\_\_map\_mul'}$ applied to the bialgebra homomorphism of $f$.

Mathlib.RingTheory.Bialgebra.GroupLike

GroupLike.valMonoidHomdefMathlib.RingTheory.Bialgebra.GroupLike, function or constant

Wording

the value monoid homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the value monoid homomorphism of $R$ and $A$ is a monoid homomorphism of $\mathrm{GroupLike}$ applied to $R$ and $A$ and $A$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{val}$ and $\mathrm{GroupLike\_\_val\_one}$ and $\mathrm{GroupLike\_\_val\_mul}$.

groupLikeSubmonoiddefMathlib.RingTheory.Bialgebra.GroupLike, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\mathrm{groupLikeSubmonoid}$ applied to $R$ and $A$ is a submonoid of $A$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $a$ to $\mathrm{IsGroupLikeElem}$ applied to $R$ and $a$ and the function that maps $x_{3}$ and $x_{4}$ to $\operatorname{mul}$ and $\operatorname{one}$.

Mathlib.RingTheory.Bialgebra.Hom

BialgHomstructureMathlib.RingTheory.Bialgebra.Hom, type

Wording

bialgebra homomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the bialgebra homomorphisms of $A$ and $B$ are a basic type.

BialgHom.compdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a bialgebra homomorphism of $B$ and $C$. Let $x_{11}$ be a bialgebra homomorphism of $A$ and $B$. Then the composition of $x_{10}$ and $x_{11}$ is a bialgebra homomorphism of $A$ and $C$.

BialgHom.copydefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a bialgebra homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a bialgebra homomorphism of $A$ and $B$.

BialgHom.iddefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the identity of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the identity of $R$ and $A$ is a bialgebra homomorphism of $A$ and $A$.

BialgHom.ofAlgHomdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the bialgebra homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$ such that the composition of the counit algebra homomorphism of $R$ and $B$ and $f$ is equal to the counit algebra homomorphism of $R$ and $A$ and the composition of the map of $f$ and $f$ and $\operatorname{comulAlgHom}$ applied to $R$ and $A$ is equal to the composition of $\operatorname{comulAlgHom}$ applied to $R$ and $B$ and $f$. Then the bialgebra homomorphism of $f$ is a bialgebra homomorphism of $A$ and $B$.

BialgHom.toAlgHomdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the algebra homomorphism of f (from the name)

English

Let $f$ be a bialgebra homomorphism of $A$ and $B$. Then the algebra homomorphism of $f$ is an algebra homomorphism of $A$ and $B$.

BialgHom.toMonoidHomdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the monoid homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a bialgebra homomorphism of $A$ and $B$. Then the monoid homomorphism of $\mathrm{self}$ is a monoid homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddHom}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toCoalgHom}$ applied to $\mathrm{self}$ and $\mathrm{BialgHom\_\_map\_one'}$ applied to $\mathrm{self}$ and $\mathrm{BialgHom\_\_map\_mul'}$ applied to $\mathrm{self}$.

BialgHomClassclassMathlib.RingTheory.Bialgebra.Hom, predicate

Wording

no wording

English

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

BialgHomClass.toBialgHomdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the bialgebra homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the bialgebra homomorphism of $f$ is a bialgebra homomorphism of $A$ and $B$.

Bialgebra.counitBialgHomdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the counit of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the counit of $R$ and $A$ is a bialgebra homomorphism of $A$ and $R$.

Bialgebra.unitBialgHomdefMathlib.RingTheory.Bialgebra.Hom, function or constant

Wording

the unit of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the unit of $R$ and $A$ is a bialgebra homomorphism of $R$ and $A$.

Mathlib.RingTheory.Bialgebra.MonoidAlgebra

AddMonoidAlgebra.bialgEquivOfSubsingletondefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the bialgebra equivalence of M (from the name)

English

Let $M$ be a set. Then the bialgebra equivalence of $M$ is a bialgebra equivalence of the set of additive monoid algebras of $R$ and $M$ and $R$.

AddMonoidAlgebra.domCongrBialgEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the domain congruence bialgebra equivalence of e (from the name)

English

Let $R$ and $A$ be sets. Let $e$ be an additive equivalence of $M$ and $N$. Then the domain congruence bialgebra equivalence of $e$ is a bialgebra equivalence of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $N$.

AddMonoidAlgebra.liftMulEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the lift multiplicative equivalence of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the lift multiplicative equivalence of $A$ and $M$ is a multiplicative equivalence of the set of monoid homomorphisms of the set of multiplicatives of $M$ and $A$ and $\mathrm{WithConv}$ applied to the set of algebra homomorphisms of the set of additive monoid algebras of $R$ and $M$ and $A$.

AddMonoidAlgebra.mapDomainBialgHomdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain bialgebra homomorphism of R and f (from the name)

English

Let $R$ be a set. Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then the map domain bialgebra homomorphism of $R$ and $f$ is a bialgebra homomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $N$.

AddMonoidAlgebra.mapDomainBialgHomAddEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain bialgebra homomorphism additive equivalence (from the name)

English

The map domain bialgebra homomorphism additive equivalence is an additive equivalence of the set of additive monoid homomorphisms of $G$ and $H$ and $\mathrm{Additive}$ applied to $\mathrm{WithConv}$ applied to the set of bialgebra homomorphisms of the set of additive monoid algebras of $R$ and $G$ and the set of additive monoid algebras of $R$ and $H$.

AddMonoidAlgebra.mapDomainBialgHomEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain bialgebra homomorphism equivalence (from the name)

English

The map domain bialgebra homomorphism equivalence is an equivalence from the set of additive monoid homomorphisms of $G$ and $H$ to the set of bialgebra homomorphisms of the set of additive monoid algebras of $R$ and $G$ and the set of additive monoid algebras of $R$ and $H$ defined as $\operatorname{mk}$ applied to $\operatorname{mapDomainBialgHom}$ applied to $R$, $\operatorname{mapDomainOfBialgHom}$, $\mathrm{AddMonoidAlgebra\_\_mapDomainOfBialgHom\_mapDomainBialgHom}$ and $\mathrm{AddMonoidAlgebra\_\_mapDomainBialgHom\_mapDomainOfBialgHom}$.

AddMonoidAlgebra.mapDomainOfBialgHomdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain of f (from the name)

English

Let $f$ be a bialgebra homomorphism of the set of additive monoid algebras of $R$ and $G$ and the set of additive monoid algebras of $R$ and $H$. Then the map domain of $f$ is an additive monoid homomorphism of $G$ and $H$.

AddMonoidAlgebra.toMultiplicativeBialgEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the multiplicative bialgebra equivalence of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the multiplicative bialgebra equivalence of $A$ and $M$ is a bialgebra equivalence of the set of additive monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and the set of multiplicatives of $M$.

MonoidAlgebra.bialgEquivOfSubsingletondefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the bialgebra equivalence of M (from the name)

English

Let $M$ be a set. Then the bialgebra equivalence of $M$ is a bialgebra equivalence of the set of monoid algebras of $R$ and $M$ and $R$.

MonoidAlgebra.domCongrBialgEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the domain congruence bialgebra equivalence of e (from the name)

English

Let $R$ and $A$ be sets. Let $e$ be a multiplicative equivalence of $M$ and $N$. Then the domain congruence bialgebra equivalence of $e$ is a bialgebra equivalence of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and $N$.

MonoidAlgebra.liftGroupLikeBialgHomdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

no wording

English

$\operatorname{liftGroupLikeBialgHom}$ is a bialgebra homomorphism of the set of monoid algebras of $R$ and $\mathrm{GroupLike}$ applied to $R$ and $A$ and $A$.

MonoidAlgebra.liftMulEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the lift multiplicative equivalence of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the lift multiplicative equivalence of $A$ and $M$ is a multiplicative equivalence of the set of monoid homomorphisms of $M$ and $A$ and $\mathrm{WithConv}$ applied to the set of algebra homomorphisms of the set of monoid algebras of $R$ and $M$ and $A$.

MonoidAlgebra.mapDomainBialgHomdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain bialgebra homomorphism of R and f (from the name)

English

Let $R$ be a set. Let $f$ be a monoid homomorphism of $M$ and $N$. Then the map domain bialgebra homomorphism of $R$ and $f$ is a bialgebra homomorphism of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and $N$.

MonoidAlgebra.mapDomainBialgHomEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain bialgebra homomorphism equivalence (from the name)

English

The map domain bialgebra homomorphism equivalence is an equivalence from the set of monoid homomorphisms of $G$ and $H$ to the set of bialgebra homomorphisms of the set of monoid algebras of $R$ and $G$ and the set of monoid algebras of $R$ and $H$ defined as $\operatorname{mk}$ applied to $\operatorname{mapDomainBialgHom}$ applied to $R$, $\operatorname{mapDomainOfBialgHom}$, $\mathrm{MonoidAlgebra\_\_mapDomainOfBialgHom\_mapDomainBialgHom}$ and $\mathrm{MonoidAlgebra\_\_mapDomainBialgHom\_mapDomainOfBialgHom}$.

MonoidAlgebra.mapDomainBialgHomMulEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain bialgebra homomorphism multiplicative equivalence (from the name)

English

The map domain bialgebra homomorphism multiplicative equivalence is a multiplicative equivalence of the set of monoid homomorphisms of $G$ and $H$ and $\mathrm{WithConv}$ applied to the set of bialgebra homomorphisms of the set of monoid algebras of $R$ and $G$ and the set of monoid algebras of $R$ and $H$.

MonoidAlgebra.mapDomainOfBialgHomdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the map domain of f (from the name)

English

Let $f$ be a bialgebra homomorphism of the set of monoid algebras of $R$ and $G$ and the set of monoid algebras of $R$ and $H$. Then the map domain of $f$ is a monoid homomorphism of $G$ and $H$.

MonoidAlgebra.toAdditiveBialgEquivdefMathlib.RingTheory.Bialgebra.MonoidAlgebra, function or constant

Wording

the additive bialgebra equivalence of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the additive bialgebra equivalence of $A$ and $M$ is a bialgebra equivalence of the set of monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $\mathrm{Additive}$ applied to $M$.

Mathlib.RingTheory.Bialgebra.Primitive

Bialgebra.IsPrimitiveElemdefMathlib.RingTheory.Bialgebra.Primitive, predicate

Wording

a is a primitive element (from the name)

English

Let $R$ be a set. Let $a$ be an element of $A$. Then $a$ is a primitive element, if $\operatorname{IsSkewPrimitiveElem}$ holds for $R$, $1$, $1$ and $a$.

Mathlib.RingTheory.Bialgebra.Quotient

Bialgebra.Quotient.comulAlgHomdefMathlib.RingTheory.Bialgebra.Quotient, function or constant

Wording

no wording

English

Let $I$ be an ideal of $A$. Then $\operatorname{comulAlgHom}$ applied to $I$ is an algebra homomorphism of the set of quotients of $A$ and $I$ and the set of tensor products of the set of quotients of $A$ and $I$ and the set of quotients of $A$ and $I$.

Bialgebra.Quotient.counitAlgHomdefMathlib.RingTheory.Bialgebra.Quotient, function or constant

Wording

the counit algebra homomorphism of I (from the name)

English

Let $I$ be an ideal of $A$. Then the counit algebra homomorphism of $I$ is an algebra homomorphism of the set of quotients of $A$ and $I$ and $R$.

Bialgebra.Quotient.mkBialgHomdefMathlib.RingTheory.Bialgebra.Quotient, function or constant

Wording

the bialgebra homomorphism of I (from the name)

English

Let $I$ be an ideal of $A$. Then the bialgebra homomorphism of $I$ is a bialgebra homomorphism of $A$ and the set of quotients of $A$ and $I$.

Mathlib.RingTheory.Bialgebra.TensorProduct

BialgHom.lTensordefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the tensor of A and f (from the name)

English

Let $A$ be a set. Let $f$ be a bialgebra homomorphism of $B$ and $C$. Then the tensor of $A$ and $f$ is a bialgebra homomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $A$ and $C$ defined as the map of the identity of $R$ and $A$ and $f$.

BialgHom.rTensordefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the tensor of A and f (from the name)

English

Let $A$ be a set. Let $f$ be a bialgebra homomorphism of $B$ and $C$. Then the tensor of $A$ and $f$ is a bialgebra homomorphism of the set of tensor products of $B$ and $A$ and the set of tensor products of $C$ and $A$ defined as the map of $f$ and the identity of $R$ and $A$.

Bialgebra.TensorProduct.assocdefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the associator of C and D (from the name)

English

Let $R$, $S$, $A$, $C$ and $D$ be sets. Then the associator of $C$ and $D$ is a bialgebra equivalence of the set of tensor products of the set of tensor products of $A$ and $C$ and $D$ and the set of tensor products of $A$ and the set of tensor products of $C$ and $D$.

Bialgebra.TensorProduct.commdefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $A$ and $B$ be sets. Then $\operatorname{comm}$ applied to $R$, $A$ and $B$ is a bialgebra equivalence of the set of tensor products of $A$ and $B$ and the set of tensor products of $B$ and $A$.

Bialgebra.TensorProduct.liddefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$ and $B$ be sets. Then $\operatorname{lid}$ applied to $R$ and $B$ is a bialgebra equivalence of the set of tensor products of $R$ and $B$ and $B$.

Bialgebra.TensorProduct.mapdefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the map of f and g (from the name)

English

Let $f$ be a bialgebra homomorphism of $A$ and $C$. Let $g$ be a bialgebra homomorphism of $B$ and $D$. Then the map of $f$ and $g$ is a bialgebra homomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $C$ and $D$.

Bialgebra.TensorProduct.riddefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $S$ and $A$ be sets. Then $\operatorname{rid}$ applied to $R$, $S$ and $A$ is a bialgebra equivalence of the set of tensor products of $A$ and $R$ and $A$.

Bialgebra.comulBialgHomdefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{comulBialgHom}$ applied to $R$ and $A$ is a bialgebra homomorphism of $A$ and the set of tensor products of $A$ and $A$.

Bialgebra.mulBialgHomdefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the multiplicative bialgebra homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the multiplicative bialgebra homomorphism of $R$ and $A$ is a bialgebra homomorphism of the set of tensor products of $A$ and $A$ and $A$.

Bialgebra.mulCoalgHomdefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the multiplicative coalgebra homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the multiplicative coalgebra homomorphism of $R$ and $A$ is a coalgebra homomorphism of the set of tensor products of $A$ and $A$ and $A$.

Coalgebra.Repr.muldefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

the product of x5 and x6 (from the name)

English

Let $x_{5}$ be a representation of $a$ and $x$. Let $x_{6}$ be a representation of $b$ and $x_{1}$. Then the product of $x_{5}$ and $x_{6}$ is a representation of $a \times b$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{induced}$ applied to $\operatorname{tmul}$ applied to $x_{5}$ and $x_{6}$ and the multiplicative coalgebra homomorphism of $R$ and $A$.

Coalgebra.Repr.tmuldefMathlib.RingTheory.Bialgebra.TensorProduct, function or constant

Wording

no wording

English

Let $x_{7}$ be a representation of $a$ and $x$. Let $x_{8}$ be a representation of $b$ and $x_{1}$. Then $\operatorname{tmul}$ applied to $x_{7}$ and $x_{8}$ is a representation of $\operatorname{tmul}$ applied to $R$, $a$ and $b$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

Mathlib.RingTheory.Binomial

BinomialRingclassMathlib.RingTheory.Binomial, predicate

Wording

R is a binomial ring (from the name)

English

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

BinomialRing.multichoosedefMathlib.RingTheory.Binomial, function or constant

Wording

the multichoose of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of $R$. Let $x_{3}$ be a natural number. Then the multichoose of $x_{2}$ and $x_{3}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

Int.multichoosedefMathlib.RingTheory.Binomial, function or constant

Wording

the multichoose of n and k (from the name)

English

Let $n$ be an integer. Let $k$ be a natural number. Then the multichoose of $n$ and $k$ is an integer.

Ring.choosedefMathlib.RingTheory.Binomial, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $n$ be a natural number. Then $\operatorname{choose}$ applied to $r$ and $n$ is an element of $R$ defined as the multichoose function of $r - n + 1$ and $n$.

Ring.multichoosedefMathlib.RingTheory.Binomial, function or constant

Wording

the multichoose function of r and n (from the docstring)

English

Let $r$ be an element of $R$. Let $n$ be a natural number. Then the multichoose function of $r$ and $n$ is an element of $R$ defined as the multichoose of $r$ and $n$.

Mathlib.RingTheory.ChainOfDivisors

mkFactorOrderIsoOfFactorDvdEquivdefMathlib.RingTheory.ChainOfDivisors, function or constant

Wording

the order isomorphism between the factors of hd (from the docstring)

English

Assume that for all elements $l$ of $\SubtypeSet {l_{2}}{(\divides {l_{2}}{m})}$, for all elements $\mathrm{l'}$ of $\SubtypeSet {l_{1}}{(\divides {l_{1}}{m})}$, $\divides {d (l)}{d (\mathrm{l'})}$, if and only if $l$ divides $\mathrm{l'}$. Then the order isomorphism between the factors of $\mathrm{hd}$ is an order isomorphism of the set of elements of $\operatorname{Iic}$ applied to $\operatorname{mk}$ applied to $m$ and the set of elements of $\operatorname{Iic}$ applied to $\operatorname{mk}$ applied to $n$.

Mathlib.RingTheory.ClassGroup.Basic

ClassGroupdefMathlib.RingTheory.ClassGroup.Basic, type

Wording

ideal class group of R (from the docstring)

English

Let $R$ be a set. Then an ideal class group of $R$ is an element of the function that maps $R$ to the set of quotients of the set of units of the set of fractional ideals of the non zero divisor of $R$ and the set of fraction rings of $R$ and the range of the principal ideal of $R$ and the set of fraction rings of $R$.

ClassGroup.equivdefMathlib.RingTheory.ClassGroup.Basic, function or constant

Wording

the equivalence of K (from the name)

English

Let $K$ be a set. Then the equivalence of $K$ is a multiplicative equivalence of the set of ideal class groups of $R$ and the set of quotients of the set of units of the set of fractional ideals of the non zero divisor of $R$ and $K$ and the range of the principal ideal of $R$ and $K$.

ClassGroup.integralRepdefMathlib.RingTheory.ClassGroup.Basic, function or constant

Wording

the integral representation of I (from the name)

English

Let $I$ be a fractional ideal of the non zero divisor of $R$ and the set of fraction rings of $R$. Then the integral representation of $I$ is an ideal of $R$ defined as the numerator of $I$.

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

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{mk}$ applied to $K$ is a monoid homomorphism of the set of units of the set of fractional ideals of the non zero divisor of $R$ and $K$ and the set of ideal class groups of $R$ defined as the composition of $\operatorname{mk'}$ applied to the range of the principal ideal of $R$ and the set of fraction rings of $R$ and the map of the monoid homomorphism of the canonical equivalence of the non zero divisor of $R$.

ClassGroup.mk0defMathlib.RingTheory.ClassGroup.Basic, function or constant

Wording

no wording

English

$\operatorname{mk0}$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (R))}{x_{1}})}$ and the set of ideal class groups of $R$ defined as the composition of $\operatorname{mk}$ applied to the set of fraction rings of $R$ and $\operatorname{mk0}$ applied to the set of fraction rings of $R$.

ClassGroup.mulEquivUnitsSubmoduleQuotRangedefMathlib.RingTheory.ClassGroup.Basic, function or constant

Wording

the multiplicative equivalence unit submodule quotient range of R (from the name)

English

Let $R$ be a set. Then the multiplicative equivalence unit submodule quotient range of $R$ is a multiplicative equivalence of the set of ideal class groups of $R$ and the set of quotients of the set of units of the set of submodules of $R$ and the set of fraction rings of $R$ and the range of the map of the monoid homomorphism of the span singleton of $R$.

FractionalIdeal.mk0defMathlib.RingTheory.ClassGroup.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{mk0}$ applied to $K$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (R))}{x_{3}})}$ and $\UnitsMACRoAO {\mathrm{FractionalIdeal} (\mathrm{nonZeroDivisors} (R), K)}$.

toPrincipalIdealdefMathlib.RingTheory.ClassGroup.Basic, function or constant

Wording

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

English

Let $R$ and $K$ be sets. Then the principal ideal of $R$ and $K$ is a monoid homomorphism of $\UnitsMACRoAO {K}$ and the set of units of the set of fractional ideals of the non zero divisor of $R$ and $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_RingTheory\_\_ClassGroup\_\_Basic\_\_183318139\_\_\_hygCtx\_\_\_hyg\_\_2}$, $R$ and $K$.

Mathlib.RingTheory.ClassGroup.ExtendedHom

ClassGroup.extendedHomdefMathlib.RingTheory.ClassGroup.ExtendedHom, function or constant

Wording

the monoid homomorphism of A and B (from the docstring)

English

Let $A$ and $B$ be sets. Then the monoid homomorphism of $A$ and $B$ is a monoid homomorphism of the set of ideal class groups of $A$ and the set of ideal class groups of $B$.

ClassGroup.extendedIdealdefMathlib.RingTheory.ClassGroup.ExtendedHom, function or constant

Wording

the extended ideal of I (from the name)

English

Let $A$ and $B$ be sets. Let $I$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (A))}{x_{4}})}$. Then the extended ideal of $I$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (B))}{x_{3}})}$ defined as the map of the algebra map of $A$ and $B$ and $I$.

ClassGroup.mapdefMathlib.RingTheory.ClassGroup.ExtendedHom, function or constant

Wording

the map of f and hf (from the name)

English

Let $f$ be a ring homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the map of $f$ and $\mathrm{hf}$ is a monoid homomorphism of the set of ideal class groups of $A$ and the set of ideal class groups of $B$.

ClassGroup.mulEquivdefMathlib.RingTheory.ClassGroup.ExtendedHom, function or constant

Wording

the multiplicative equivalence of g (from the name)

English

Let $g$ be a ring isomorphism of $A$ and $B$. Then the multiplicative equivalence of $g$ is a multiplicative equivalence of the set of ideal class groups of $A$ and the set of ideal class groups of $B$.

Mathlib.RingTheory.Coalgebra.Basic

CoalgebraclassMathlib.RingTheory.Coalgebra.Basic, predicate

Wording

A is a coalgebra with respect to R (from the name)

English

Let $R$ and $A$ be sets. Then we can say that $A$ is a coalgebra with respect to $R$.

Coalgebra.IsCocommclassMathlib.RingTheory.Coalgebra.Basic, predicate

Wording

no wording

English

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

Coalgebra.ReprstructureMathlib.RingTheory.Coalgebra.Basic, type

Wording

representation of a and x4 (from the name)

English

Let $R$ and $x_{4}$ be sets. Let $a$ be an element of $A$. Then the representations of $a$ and $x_{4}$ are a basic type.

Coalgebra.Repr.arbitrarydefMathlib.RingTheory.Coalgebra.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $a$ be an element of $A$. Then $\operatorname{arbitrary}$ applied to $R$ and $a$ is a representation of $a$ and $\mathrm{Prod}$ applied to $A$ and $A$.

Coalgebra.Repr.indexdefMathlib.RingTheory.Coalgebra.Basic, function or constant

Wording

the finite indexing set of self (from the docstring)

English

Let $\mathrm{self}$ be a representation of $a$ and $x_{4}$. Then the finite indexing set of $\mathrm{self}$ is a finite set of $x_{4}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Coalgebra.Repr.leftdefMathlib.RingTheory.Coalgebra.Basic, function or constant

Wording

the left of self and x5 (from the name)

English

Let $\mathrm{self}$ be a representation of $a$ and $x_{4}$. Let $x_{5}$ be an element of $x_{4}$. Then the left of $\mathrm{self}$ and $x_{5}$ is an element of $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{5}$.

Coalgebra.Repr.rightdefMathlib.RingTheory.Coalgebra.Basic, function or constant

Wording

the right of self and x5 (from the name)

English

Let $\mathrm{self}$ be a representation of $a$ and $x_{4}$. Let $x_{5}$ be an element of $x_{4}$. Then the right of $\mathrm{self}$ and $x_{5}$ is an element of $A$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{5}$.

CoalgebraStructclassMathlib.RingTheory.Coalgebra.Basic, predicate

Wording

no wording

English

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

CoalgebraStruct.comuldefMathlib.RingTheory.Coalgebra.Basic, function or constant

Wording

the comultiplication of the coalgebra (from the docstring)

English

The comultiplication of the coalgebra is a linear map of $A$ and the set of tensor products of $A$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CoalgebraStruct.counitdefMathlib.RingTheory.Coalgebra.Basic, function or constant

Wording

the counit of the coalgebra (from the docstring)

English

The counit of the coalgebra is a linear map of $A$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.RingTheory.Coalgebra.CoassocSimps

CoassocSimps.assoc_comp_map_assoc_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.assoc_comp_map_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.assoc_symm_comp_map_assoc_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.assoc_symm_comp_map_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.lid_comp_map_assoc_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.lid_comp_map_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.rid_comp_map_assoc_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

CoassocSimps.rid_comp_map_simprocdefMathlib.RingTheory.Coalgebra.CoassocSimps, function or constant

Wording

no wording

English

$\operatorname{Simproc}$.

Mathlib.RingTheory.Coalgebra.Convolution

AlgHom.convPostcompdefMathlib.RingTheory.Coalgebra.Convolution, function or constant

Wording

no wording

English

Let $h$ be an algebra homomorphism of $A$ and $B$. Then $\operatorname{convPostcomp}$ applied to $h$ is an algebra homomorphism of $\mathrm{WithConv}$ applied to the set of linear maps of $C$ and $A$ and $\mathrm{WithConv}$ applied to the set of linear maps of $C$ and $B$.

CoalgHom.convPrecompdefMathlib.RingTheory.Coalgebra.Convolution, function or constant

Wording

no wording

English

Let $h$ be a coalgebra homomorphism of $B$ and $C$. Then $\operatorname{convPrecomp}$ applied to $h$ is an algebra homomorphism of $\mathrm{WithConv}$ applied to the set of linear maps of $C$ and $A$ and $\mathrm{WithConv}$ applied to the set of linear maps of $B$ and $A$.

Mathlib.RingTheory.Coalgebra.Equiv

CoalgEquivstructureMathlib.RingTheory.Coalgebra.Equiv, type

Wording

coalgebra equivalence of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the coalgebra equivalences of $A$ and $B$ are a basic type.

CoalgEquiv.invFundefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the inverse function of self and x7 (from the name)

English

Let $\mathrm{self}$ be a coalgebra equivalence of $A$ and $B$. Let $x_{7}$ be an element of $B$. Then the inverse function of $\mathrm{self}$ and $x_{7}$ is an element of $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{7}$.

CoalgEquiv.ofBijectivedefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the coalgebra equivalence of hf (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is bijective. Then the coalgebra equivalence of $\mathrm{hf}$ is a coalgebra equivalence of $A$ and $B$.

CoalgEquiv.ofClassdefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the coalgebra equivalence of f (from the name)

English

Let $f$ be an element of $F$. Then the coalgebra equivalence of $f$ is a coalgebra equivalence of $A$ and $B$.

CoalgEquiv.ofCoalgHomdefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the coalgebra equivalence of f and g (from the name)

English

Let $f$ be a coalgebra homomorphism of $A$ and $B$. Let $g$ be a coalgebra homomorphism of $B$ and $A$ such that the composition of $f$ and $g$ is equal to the identity of $R$ and $B$ and the composition of $g$ and $f$ is equal to the identity of $R$ and $A$. Then the coalgebra equivalence of $f$ and $g$ is a coalgebra equivalence of $A$ and $B$.

CoalgEquiv.refldefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the identity map of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the identity map of $R$ and $A$ is a coalgebra equivalence of $A$ and $A$.

CoalgEquiv.symmdefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be a coalgebra equivalence of $A$ and $B$. Then the inverse of $e$ is a coalgebra equivalence of $B$ and $A$.

CoalgEquiv.toEquivdefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the equivalence of x7 (from the name)

English

Let $x_{7}$ be a coalgebra equivalence of $A$ and $B$. Then the equivalence of $x_{7}$ is an equivalence from $A$ to $B$ defined as the equivalence of the linear equivalence of $x_{7}$.

CoalgEquiv.toLinearEquivdefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the linear equivalence of self (from the name)

English

Let $\mathrm{self}$ be a coalgebra equivalence of $A$ and $B$. Then the linear equivalence of $\mathrm{self}$ is a linear equivalence of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toCoalgHom}$ applied to $\mathrm{self}$, $\operatorname{invFun}$ applied to $\mathrm{self}$, $\mathrm{CoalgEquiv\_\_left\_inv}$ applied to $\mathrm{self}$ and $\mathrm{CoalgEquiv\_\_right\_inv}$ applied to $\mathrm{self}$.

CoalgEquiv.transdefMathlib.RingTheory.Coalgebra.Equiv, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a coalgebra equivalence of $A$ and $B$. Let $x_{11}$ be a coalgebra equivalence of $B$ and $C$. Then the composition of $x_{10}$ and $x_{11}$ is a coalgebra equivalence of $A$ and $C$.

CoalgEquivClassclassMathlib.RingTheory.Coalgebra.Equiv, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Coalgebra.GroupLike

GroupLikestructureMathlib.RingTheory.Coalgebra.GroupLike, type

Wording

no wording

English

Let $R$ and $A$ be sets. Then the elements of $\mathrm{GroupLike}$ applied to $R$ and $A$ are a basic type.

GroupLike.valdefMathlib.RingTheory.Coalgebra.GroupLike, function or constant

Wording

the value of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{GroupLike}$ applied to $R$ and $A$. Then the value of $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

GroupLike.valEquivdefMathlib.RingTheory.Coalgebra.GroupLike, function or constant

Wording

the value equivalence (from the name)

English

The value equivalence is an element of $\EquivMACRoAE {\mathrm{GroupLike} (R , A)}{(\SubtypeSet {a}{\mathrm{IsGroupLikeElem} (R , a)})}$.

IsGroupLikeElemstructureMathlib.RingTheory.Coalgebra.GroupLike, predicate

Wording

no wording

English

Let $R$ be a set. Let $a$ be an element of $A$. Then we can say that $\mathrm{IsGroupLikeElem}$ holds for $R$ and $a$.

Mathlib.RingTheory.Coalgebra.Hom

CoalgHomstructureMathlib.RingTheory.Coalgebra.Hom, type

Wording

coalgebra homomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the coalgebra homomorphisms of $A$ and $B$ are a basic type.

CoalgHom.compdefMathlib.RingTheory.Coalgebra.Hom, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a coalgebra homomorphism of $B$ and $C$. Let $x_{11}$ be a coalgebra homomorphism of $A$ and $B$. Then the composition of $x_{10}$ and $x_{11}$ is a coalgebra homomorphism of $A$ and $C$.

CoalgHom.copydefMathlib.RingTheory.Coalgebra.Hom, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a coalgebra homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a coalgebra homomorphism of $A$ and $B$.

CoalgHom.iddefMathlib.RingTheory.Coalgebra.Hom, function or constant

Wording

the identity of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the identity of $R$ and $A$ is a coalgebra homomorphism of $A$ and $A$.

CoalgHom.ofClassdefMathlib.RingTheory.Coalgebra.Hom, function or constant

Wording

the coalgebra homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the coalgebra homomorphism of $f$ is a coalgebra homomorphism of $A$ and $B$.

CoalgHomClassclassMathlib.RingTheory.Coalgebra.Hom, predicate

Wording

no wording

English

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

Coalgebra.Repr.induceddefMathlib.RingTheory.Coalgebra.Hom, function or constant

Wording

no wording

English

Let $\mathrm{repr}$ be a representation of $a$ and $x$. Let $x_{9}$ be an element of $F$. Then $\operatorname{induced}$ applied to $\mathrm{repr}$ and $x_{9}$ is a representation of $x_{9}$ applied to $a$ and $x$.

Coalgebra.counitCoalgHomdefMathlib.RingTheory.Coalgebra.Hom, function or constant

Wording

the counit of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the counit of $R$ and $A$ is a coalgebra homomorphism of $A$ and $R$.

Mathlib.RingTheory.Coalgebra.IsFrobenius

Coalgebra.IsFrobeniusclassMathlib.RingTheory.Coalgebra.IsFrobenius, predicate

Wording

no wording

English

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

Coalgebra.IsFrobenius.leftdefMathlib.RingTheory.Coalgebra.IsFrobenius, function or constant

Wording

the left of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the left of $R$ and $A$ is a linear map of the set of tensor products of $A$ and $A$ and the set of tensor products of $A$ and $A$ defined as the composition of the tensor of $A$ and the product of $R$ and $A$ and the composition of $\operatorname{toLinearMap}$ applied to the associator of $A$ and $A$ and the tensor of $A$ and the comultiplication of the coalgebra.

Coalgebra.IsFrobenius.rightdefMathlib.RingTheory.Coalgebra.IsFrobenius, function or constant

Wording

the right of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the right of $R$ and $A$ is a linear map of the set of tensor products of $A$ and $A$ and the set of tensor products of $A$ and $A$ defined as the composition of the tensor of $A$ and the product of $R$ and $A$ and the composition of $\operatorname{toLinearMap}$ applied to the inverse of the associator of $A$ and $A$ and the tensor of $A$ and the comultiplication of the coalgebra.

Mathlib.RingTheory.Coalgebra.Primitive

Coalgebra.IsSkewPrimitiveElemstructureMathlib.RingTheory.Coalgebra.Primitive, predicate

Wording

no wording

English

Let $R$ be a set. Let $g$, $h$ and $a$ be elements of $A$. Then we can say that $\operatorname{IsSkewPrimitiveElem}$ holds for $R$, $g$, $h$ and $a$.

Coalgebra.skewPrimitivedefMathlib.RingTheory.Coalgebra.Primitive, function or constant

Wording

no wording

English

Let $R$ be a set. Let $g$ and $h$ be elements of $A$. Then $\operatorname{skewPrimitive}$ applied to $R$, $g$ and $h$ is a submodule of $R$ and $A$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $a$ to $\operatorname{IsSkewPrimitiveElem}$ applied to $R$, $g$, $h$ and $a$ and the function that maps $x_{4}$ and $x_{5}$ to $\operatorname{add}$ and $\operatorname{zero}$ and the function that maps $r$, $x_{6}$ and $\mathrm{ha}$ to $\operatorname{smul}$ applied to $\mathrm{ha}$ and $r$.

Mathlib.RingTheory.Coalgebra.Quotient

Coalgebra.Quotient.mkQCoalgHomdefMathlib.RingTheory.Coalgebra.Quotient, function or constant

Wording

the coalgebra homomorphism of I (from the name)

English

Let $I$ be a submodule of $R$ and $C$. Then the coalgebra homomorphism of $I$ is a coalgebra homomorphism of $C$ and the set of quotients of $C$ and $I$.

Submodule.IsCoidealclassMathlib.RingTheory.Coalgebra.Quotient, predicate

Wording

no wording

English

Let $I$ be a submodule of $R$ and $C$. Then we can say that $\operatorname{IsCoideal}$ holds for $I$.

Mathlib.RingTheory.Coalgebra.TensorProduct

CoalgHom.lTensordefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

the tensor of M and f (from the name)

English

Let $M$ be a set. Let $f$ be a coalgebra homomorphism of $N$ and $P$. Then the tensor of $M$ and $f$ is a coalgebra homomorphism of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $P$ defined as the map of the identity of $R$ and $M$ and $f$.

CoalgHom.rTensordefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

the tensor of M and f (from the name)

English

Let $M$ be a set. Let $f$ be a coalgebra homomorphism of $N$ and $P$. Then the tensor of $M$ and $f$ is a coalgebra homomorphism of the set of tensor products of $N$ and $M$ and the set of tensor products of $P$ and $M$ defined as the map of $f$ and the identity of $R$ and $M$.

Coalgebra.TensorProduct.assocdefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

the associator of N and P (from the name)

English

Let $R$, $S$, $M$, $N$ and $P$ be sets. Then the associator of $N$ and $P$ is a coalgebra equivalence of the set of tensor products of the set of tensor products of $M$ and $N$ and $P$ and the set of tensor products of $M$ and the set of tensor products of $N$ and $P$.

Coalgebra.TensorProduct.liddefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$ and $P$ be sets. Then $\operatorname{lid}$ applied to $R$ and $P$ is a coalgebra equivalence of the set of tensor products of $R$ and $P$ and $P$.

Coalgebra.TensorProduct.mapdefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

the map of f and g (from the name)

English

Let $f$ be a coalgebra homomorphism of $M$ and $N$. Let $g$ be a coalgebra homomorphism of $P$ and $Q$. Then the map of $f$ and $g$ is a coalgebra homomorphism of the set of tensor products of $M$ and $P$ and the set of tensor products of $N$ and $Q$.

Coalgebra.TensorProduct.riddefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $S$ and $M$ be sets. Then $\operatorname{rid}$ applied to $R$, $S$ and $M$ is a coalgebra equivalence of the set of tensor products of $M$ and $R$ and $M$.

Coalgebra.comulCoalgHomdefMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

no wording

English

Let $R$ and $C$ be sets. Then $\operatorname{comulCoalgHom}$ applied to $R$ and $C$ is a coalgebra homomorphism of $C$ and the set of tensor products of $C$ and $C$.

TensorProduct.tacticHopf_tensor_induction_With__defMathlib.RingTheory.Coalgebra.TensorProduct, function or constant

Wording

no wording

English

generation took over the time limit

Mathlib.RingTheory.Conductor

conductordefMathlib.RingTheory.Conductor, function or constant

Wording

the conductor of R and x3 (from the name)

English

Let $R$ be a set. Let $x_{3}$ be an element of $S$. Then the conductor of $R$ and $x_{3}$ is an ideal of $S$.

quotAdjoinEquivQuotMapdefMathlib.RingTheory.Conductor, function or constant

Wording

no wording

English

Assume that the maximum of the preimage of the conductor of $R$ and $x_{3}$ under the algebra map of $R$ and $S$ and $I$ is equal to the top. Assume that $\operatorname{coe}$ applied to the algebra map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{6}})}$ and $S$ is injective. Then $\mathrm{quotAdjoinEquivQuotMap}$ applied to $\mathrm{hx}$ and $\mathrm{h\_alg}$ is a ring isomorphism of the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$ and the map of the algebra map of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , \operatorname{singleton} (x_{3}))}{x_{5}})}$ and $I$ and the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $I$.

Mathlib.RingTheory.Congruence.Basic

RingCon.gidefMathlib.RingTheory.Congruence.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{gi}$ applied to $R$ is a Galois insertion of $\mathrm{ringConGen}$ and $\operatorname{coe}$.

RingCon.mkₐdefMathlib.RingTheory.Congruence.Basic, function or constant

Wording

no wording

English

Let $x$ be a set. Let $c$ be a ring congruence relation of $R$. Then $\mathrm{RingCon\_\_mk\_u2090\_}$ applied to $x$ and $c$ is an algebra homomorphism of $R$ and the set of quotients of $c$.

Mathlib.RingTheory.Congruence.Defs

RingConstructureMathlib.RingTheory.Congruence.Defs, type

Wording

ring congruence relation of R (from the name)

English

Let $R$ be a set. Then the ring congruence relations of $R$ are a basic type.

RingCon.QuotientdefMathlib.RingTheory.Congruence.Defs, type

Wording

quotient of c (from the name)

English

Let $c$ be a ring congruence relation of $R$. Then a quotient of $c$ is an element of the function that maps $c$ to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $\operatorname{toCon}$ applied to $c$.

RingCon.comapdefMathlib.RingTheory.Congruence.Defs, function or constant

Wording

the preimage of J and f (from the name)

English

Let $J$ be a ring congruence relation of $\mathrm{R'}$. Let $f$ be an element of $F$. Then the preimage of $J$ and $f$ is a ring congruence relation of $R$ defined as $\operatorname{mk}$ applied to the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{toCon}$ applied to $J$ and $\operatorname{add'}$ applied to the preimage of $\operatorname{coe}$ applied to $f$ and the additive congruence relation of $J$.

RingCon.mk'defMathlib.RingTheory.Congruence.Defs, function or constant

Wording

no wording

English

Let $c$ be a ring congruence relation of $R$. Then $\operatorname{mk'}$ applied to $c$ is a ring homomorphism of $R$ and the set of quotients of $c$.

RingCon.toAddCondefMathlib.RingTheory.Congruence.Defs, function or constant

Wording

the additive congruence relation of self (from the name)

English

Let $\mathrm{self}$ be a ring congruence relation of $R$. Then the additive congruence relation of $\mathrm{self}$ is an additive congruence relation of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toSetoid}$ applied to $\operatorname{toCon}$ applied to $\mathrm{self}$ and $\operatorname{add'}$ applied to $\mathrm{self}$.

RingCon.toQuotientdefMathlib.RingTheory.Congruence.Defs, function or constant

Wording

the morphism into the quotient by a congruence relation of r (from the docstring)

English

Let $r$ be an element of $R$. Then the morphism into the quotient by a congruence relation of $r$ is a quotient of $c$ defined as $\operatorname{mk''}$ applied to $r$.

RingConGen.RelinductiveMathlib.RingTheory.Congruence.Defs, predicate

Wording

no wording

English

Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Let $x_{2}$ and $x_{3}$ be elements of $R$. Then we can say that $\operatorname{Rel}$ holds for $r$, $x_{2}$ and $x_{3}$.

RingConGen.Rel.belowinductiveMathlib.RingTheory.Congruence.Defs, predicate

Wording

no wording

English

Assume that $\operatorname{Rel}$ holds for $r$, $x_{2}$ and $x_{3}$. Then we can say that $\operatorname{below}$ holds for $t$.

ringConGendefMathlib.RingTheory.Congruence.Defs, function or constant

Wording

the ring congruence relation generator of r (from the name)

English

Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Then the ring congruence relation generator of $r$ is a ring congruence relation of $R$.

Mathlib.RingTheory.Congruence.Hom

RingCon.comapQuotientEquivOfSurjdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the preimage quotient equivalence of c and f (from the name)

English

Let $c$ be a ring congruence relation of $M$. Let $f$ be a ring homomorphism of $N$ and $M$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$ and $d$ is equal to the preimage of $c$ and $f$. Then the preimage quotient equivalence of $c$ and $f$ is a ring isomorphism of the set of quotients of $d$ and the set of quotients of $c$.

RingCon.comapQuotientEquivRangedefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the preimage quotient equivalence range of c and f (from the name)

English

Let $c$ be a ring congruence relation of $M$. Let $f$ be a ring homomorphism of $N$ and $M$ such that $\EqtMACRoH {d}{\operatorname{comap} (c , f)}$. Then the preimage quotient equivalence range of $c$ and $f$ is a ring isomorphism of the set of quotients of $d$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{comp} (\operatorname{mk'} (c), f))}{x_{2}})}$ defined as the preimage quotient equivalence range of $c$ and $f$.

RingCon.comapQuotientEquivRangeSdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the preimage quotient equivalence range of c and f (from the name)

English

Let $c$ be a ring congruence relation of $M$. Let $f$ be a ring homomorphism of $N$ and $M$ such that $\EqtMACRoH {d}{\operatorname{comap} (c , f)}$. Then the preimage quotient equivalence range of $c$ and $f$ is a ring isomorphism of the set of quotients of $d$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{rangeS} (\operatorname{comp} (\operatorname{mk'} (c), f))}{x_{2}})}$.

RingCon.comapQuotientEquivRangeₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the preimage quotient equivalence range of c and f (from the name)

English

Let $c$ be a ring congruence relation of $M$. Let $f$ be an algebra homomorphism of $N$ and $M$ such that $\EqtMACRoH {d}{\operatorname{comap} (c , f)}$. Then the preimage quotient equivalence range of $c$ and $f$ is an algebra isomorphism of the set of quotients of $d$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{comp} (\mathrm{RingCon\_\_mk\_u2090\_} (R , c), f))}{x_{5}})}$.

RingCon.congrdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the congruence of e and h (from the name)

English

Let $e$ be a ring isomorphism of $M$ and $N$ such that $c$ is equal to the preimage of $d$ and $e$. Then the congruence of $e$ and $h$ is a ring isomorphism of the set of quotients of $c$ and the set of quotients of $d$.

RingCon.congrₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the congruence of e (from the name)

English

Let $R$ be a set. Let $e$ be an algebra isomorphism of $M$ and $N$ such that $c$ is equal to the preimage of $d$ and $e$. Then the congruence of $e$ is an algebra isomorphism of the set of quotients of $c$ and the set of quotients of $d$.

RingCon.correspondencedefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the correspondence (from the name)

English

The correspondence is an order isomorphism of the set of elements of $\operatorname{Ici}$ applied to $c$ and the set of ring congruence relations of the set of quotients of $c$.

RingCon.factorₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the factor of R and h (from the name)

English

Let $R$ be a set. Assume that $c \leq d$. Then the factor of $R$ and $h$ is an algebra homomorphism of the set of quotients of $c$ and the set of quotients of $d$.

RingCon.kerdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a ring homomorphism of $M$ and $N$. Then the kernel of $f$ is a ring congruence relation of $M$ defined as the preimage of the bottom and $f$.

RingCon.kerLiftdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the kernel lift of f (from the name)

English

Let $f$ be a ring homomorphism of $M$ and $P$. Then the kernel lift of $f$ is a ring homomorphism of the set of quotients of the kernel of $f$ and $P$.

RingCon.kerLiftₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the kernel lift of f (from the name)

English

Let $f$ be an algebra homomorphism of $M$ and $P$. Then the kernel lift of $f$ is an algebra homomorphism of the set of quotients of the kernel of $\operatorname{toRingHom}$ applied to $f$ and $P$.

RingCon.liftdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the lift of c and f (from the name)

English

Let $c$ be a ring congruence relation of $M$. Let $f$ be a ring homomorphism of $M$ and $P$ such that $c$ is less than or equal to the kernel of $f$. Then the lift of $c$ and $f$ is a ring homomorphism of the set of quotients of $c$ and $P$.

RingCon.liftₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the lift of c and f (from the name)

English

Let $c$ be a ring congruence relation of $M$. Let $f$ be an algebra homomorphism of $M$ and $P$ such that $c$ is less than or equal to the kernel of $\operatorname{toRingHom}$ applied to $f$. Then the lift of $c$ and $f$ is an algebra homomorphism of the set of quotients of $c$ and $P$.

RingCon.liftₐEquivdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the lift equivalence of c (from the name)

English

Let $c$ be a ring congruence relation of $M$. Then the lift equivalence of $c$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{Leq} (c , \operatorname{ker} (\operatorname{toRingHom} (f)))})}{\mathrm{AlgHom} (\operatorname{Quotient} (c), P)}$.

RingCon.mapdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the map of c and d (from the name)

English

Let $c$ and $d$ be ring congruence relations of $M$ such that $c \leq d$. Then the map of $c$ and $d$ is a ring homomorphism of the set of quotients of $c$ and the set of quotients of $d$.

RingCon.mapGendefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the map generator of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Then the map generator of $f$ is a ring congruence relation of $N$ defined as the ring congruence relation generator of $\operatorname{Map}$ applied to $\operatorname{coe}$ applied to $c$, $f$ and $f$.

RingCon.quotientKerEquivOfRightInversedefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient kernel equivalence of f and g (from the name)

English

Let $f$ be a ring homomorphism of $M$ and $P$. Let $g$ be a function from elements of $P$ to elements of $M$ such that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $g$ is a ring isomorphism of the set of quotients of the kernel of $f$ and $P$.

RingCon.quotientKerEquivOfSurjectivedefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient kernel equivalence of f and hf (from the name)

English

Let $f$ be a ring homomorphism of $M$ and $P$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $\mathrm{hf}$ is a ring isomorphism of the set of quotients of the kernel of $f$ and $P$.

RingCon.quotientKerEquivRangedefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient kernel equivalence range of f (from the name)

English

Let $f$ be a ring homomorphism of $M$ and $P$. Then the quotient kernel equivalence range of $f$ is a ring isomorphism of the set of quotients of the kernel of $f$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$ defined as the quotient kernel equivalence range of $f$.

RingCon.quotientKerEquivRangeSdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient kernel equivalence range of f (from the name)

English

RingCon.quotientKerEquivRangeₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient kernel equivalence range of f (from the name)

English

Let $f$ be an algebra homomorphism of $M$ and $P$. Then the quotient kernel equivalence range of $f$ is an algebra isomorphism of the set of quotients of the kernel of the ring homomorphism of $f$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$.

RingCon.quotientQuotientEquivQuotientdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient quotient equivalence quotient of c and d (from the name)

English

Let $c$ and $d$ be ring congruence relations of $M$ such that $c \leq d$. Then the quotient quotient equivalence quotient of $c$ and $d$ is a ring isomorphism of the set of quotients of the kernel of the map of $c$ and $d$ and the set of quotients of $d$.

RingCon.quotientQuotientEquivQuotientₐdefMathlib.RingTheory.Congruence.Hom, function or constant

Wording

the quotient quotient equivalence quotient of R and h (from the name)

English

Let $R$ be a set. Assume that $c \leq d$. Then the quotient quotient equivalence quotient of $R$ and $h$ is an algebra isomorphism of the set of quotients of the kernel of the ring homomorphism of the factor of $R$ and $h$ and the set of quotients of $d$.

Mathlib.RingTheory.Congruence.Opposite

RingCon.opdefMathlib.RingTheory.Congruence.Opposite, function or constant

Wording

the opposite of c (from the name)

English

Let $c$ be a ring congruence relation of $R$. Then the opposite of $c$ is a ring congruence relation of the set of multiplicative opposites of $R$.

RingCon.opOrderIsodefMathlib.RingTheory.Congruence.Opposite, function or constant

Wording

the opposite order isomorphism (from the name)

English

The opposite order isomorphism is an order isomorphism of the set of ring congruence relations of $R$ and the set of ring congruence relations of the set of multiplicative opposites of $R$.

RingCon.unopdefMathlib.RingTheory.Congruence.Opposite, function or constant

Wording

the opposite of c (from the name)

English

Let $c$ be a ring congruence relation of the set of multiplicative opposites of $R$. Then the opposite of $c$ is a ring congruence relation of $R$.

Mathlib.RingTheory.Coprime.Basic

IsCoprimedefMathlib.RingTheory.Coprime.Basic, predicate

Wording

x1 is coprime to y (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Then $x_{1}$ is coprime to $y$, if there exist elements $a$ and $b$ of $R$, such that $\EqtMACRoH {a \times x_{1} + b \times y}{1}$.

Mathlib.RingTheory.DedekindDomain.AdicValuation.Completion

IsDedekindDomain.HeightOneSpectrum.adicCompletionstructureMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, type

Wording

adic completion of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the adic completions of $K$ and $v$ are a basic type.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivdefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the equivalence of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the equivalence of $K$ and $v$ is a ring isomorphism of the set of adic completions of $K$ and $v$ and the set of completions of the valuation of $K$ and $v$.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletiondefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the equivalence completion of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the equivalence completion of $K$ and $v$ is an equivalence from the set of adic completions of $K$ and $v$ to the set of completions of the valuation of $K$ and $v$.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletiondefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the underlying element of the completion of self (from the docstring)

English

Let $\mathrm{self}$ be an adic completion of $K$ and $v$. Then the underlying element of the completion of $\mathrm{self}$ is a completion of the valuation of $K$ and $v$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquivdefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the uniform equivalence of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the uniform equivalence of $K$ and $v$ is a uniform equivalence of the set of adic completions of $K$ and $v$ and the set of completions of the valuation of $K$ and $v$.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuationdefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the valuation of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the valuation of $K$ and $v$ is a valuation of the set of adic completions of $K$ and $v$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as the preimage of the ring homomorphism of the equivalence of $K$ and $v$ and the extension of the valuation of the valuation of $K$ and $v$.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquivdefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the value group of K and v (from the docstring)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the value group of $K$ and $v$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (\operatorname{valuation} (K , v)))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (\operatorname{extension} (\operatorname{valuation} (\operatorname{valuation} (K , v)))))}{x_{4}})}$.

IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIsodefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the value group with zero of K and v (from the docstring)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the value group with zero of $K$ and $v$ is an order monoid isomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to the valuation of $K$ and $v$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to the extension of the valuation of the valuation of $K$ and $v$.

IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersdefMathlib.RingTheory.DedekindDomain.AdicValuation.Completion, function or constant

Wording

the adic completion integer of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the adic completion integer of $K$ and $v$ is a valuation subring of the set of adic completions of $K$ and $v$ defined as the valuation subring of $\operatorname{v}$.

Mathlib.RingTheory.DedekindDomain.AdicValuation.Valuation

IsDedekindDomain.HeightOneSpectrum.adicAbvdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of $R$. Assume that $1 < b$. Then $\operatorname{adicAbv}$ applied to $v$ and $\mathrm{hb}$ is an absolute value of $K$ and $\Real$.

IsDedekindDomain.HeightOneSpectrum.adicAbvDefdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of $R$. Assume that $1 < b$. Let $x_{3}$ be an element of $K$. Then $\operatorname{adicAbvDef}$ applied to $v$, $\mathrm{hb}$ and $x_{3}$ is an element of $\mathrm{NNReal}$.

IsDedekindDomain.HeightOneSpectrum.intAdicAbvdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of $R$. Assume that $1 < b$. Then $\operatorname{intAdicAbv}$ applied to $v$ and $\mathrm{hb}$ is an absolute value of $R$ and $\Real$.

IsDedekindDomain.HeightOneSpectrum.intAdicAbvDefdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of $R$. Assume that $1 < b$. Let $r$ be an element of $R$. Then $\operatorname{intAdicAbvDef}$ applied to $v$, $\mathrm{hb}$ and $r$ is an element of $\mathrm{NNReal}$.

IsDedekindDomain.HeightOneSpectrum.intValuationdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

the integer valuation of v (from the name)

English

Let $v$ be a height one spectrum of $R$. Then the integer valuation of $v$ is a valuation of $R$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{intValuationDef}$ applied to $v$ and $\mathrm{IsDedekindDomain\_\_HeightOneSpectrum\_\_intValuation\_\_map\_zero'}$ applied to $v$, $\mathrm{IsDedekindDomain\_\_HeightOneSpectrum\_\_intValuation\_\_map\_one'}$ applied to $v$ and $\mathrm{IsDedekindDomain\_\_HeightOneSpectrum\_\_intValuation\_\_map\_mul'}$ applied to $v$ and $\mathrm{IsDedekindDomain\_\_HeightOneSpectrum\_\_intValuation\_\_map\_add\_le\_max'}$ applied to $v$.

IsDedekindDomain.HeightOneSpectrum.intValuationDefdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

the integer valuation of v and r (from the name)

English

Let $v$ be a height one spectrum of $R$. Let $r$ be an element of $R$. Then the integer valuation of $v$ and $r$ is an element of $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as $\iteMACRoG {(\EqtMACRoH {r}{0})}{0}{\operatorname{exp} (\operatorname{neg} (\operatorname{count} (\operatorname{mk} (\operatorname{asIdeal} (v)), \operatorname{factors} (\operatorname{mk} (\operatorname{span} (\operatorname{singleton} (r)))))))}$.

IsDedekindDomain.HeightOneSpectrum.valuationdefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

the valuation of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the valuation of $K$ and $v$ is a valuation of $K$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$.

IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrimedefMathlib.RingTheory.DedekindDomain.AdicValuation.Valuation, function or constant

Wording

the valuation subring at prime of K and v (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the valuation subring at prime of $K$ and $v$ is a valuation subring of $K$.

Mathlib.RingTheory.DedekindDomain.Basic

IsDedekindDomainclassMathlib.RingTheory.DedekindDomain.Basic, predicate

Wording

A is a Dedekind domain (from the name)

English

Let $A$ be a set. Then we can say that $A$ is a Dedekind domain.

IsDedekindRingclassMathlib.RingTheory.DedekindDomain.Basic, predicate

Wording

A is a Dedekind ring (from the name)

English

Let $A$ be a set. Then we can say that $A$ is a Dedekind ring.

Ring.DimensionLEOneclassMathlib.RingTheory.DedekindDomain.Basic, predicate

Wording

no wording

English

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

Mathlib.RingTheory.DedekindDomain.Different

FractionalIdeal.dualdefMathlib.RingTheory.DedekindDomain.Different, function or constant

Wording

the dual of I (from the name)

English

Let $A$ and $K$ be sets. Let $I$ be a fractional ideal of the non zero divisor of $B$ and $L$. Then the dual of $I$ is a fractional ideal of the non zero divisor of $B$ and $L$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {I}{0}$, the function that maps $\mathrm{hI}$ to $0$ and the function that maps $\mathrm{hI1}$ to the trace dual of the coercion to submodule of $I$.

Submodule.traceDualdefMathlib.RingTheory.DedekindDomain.Different, function or constant

Wording

the trace dual of I (from the name)

English

Let $A$ and $K$ be sets. Let $I$ be a submodule of $B$ and $L$. Then the trace dual of $I$ is a submodule of $B$ and $L$.

differentIdealdefMathlib.RingTheory.DedekindDomain.Different, function or constant

Wording

the different ideal of A and B (from the docstring)

English

Let $A$ and $B$ be sets. Then the different ideal of $A$ and $B$ is an ideal of $B$ defined as the preimage of the linear map of $B$ and the set of fraction rings of $B$ and the quotient of $1$ and the trace dual of $1$.

Mathlib.RingTheory.DedekindDomain.Factorization

FractionalIdeal.countdefMathlib.RingTheory.DedekindDomain.Factorization, function or constant

Wording

the count of v and I (from the name)

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Let $I$ be a fractional ideal of the non zero divisor of $R$ and $K$. Then the count of $v$ and $I$ is an integer.

FractionalIdeal.divModdefMathlib.RingTheory.DedekindDomain.Factorization, function or constant

Wording

no wording

English

Let $c$, $b$ and $a$ be fractional ideals of the non zero divisor of $R$ and $K$. Then $\operatorname{divMod}$ applied to $c$, $b$ and $a$ is an element of $K$.

FractionalIdeal.quotientEquivdefMathlib.RingTheory.DedekindDomain.Factorization, function or constant

Wording

the quotient equivalence of H and h2 (from the name)

English

Let $I$, $J$, $\mathrm{I'}$ and $\mathrm{J'}$ be fractional ideals of the non zero divisor of $R$ and $K$ such that $\EqtMACRoH {I \times \mathrm{J'}}{\mathrm{I'} \times J}$, $J \leq I$, $\mathrm{J'} \leq \mathrm{I'}$, $\mathrm{J'} \neq 0$ and $I \neq 0$. Then the quotient equivalence of $\mathrm{I'}$ and $\mathrm{J'}$ is a linear equivalence of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (I)}{x_{3}})}$ and the preimage of the subtype of the coercion to submodule of $I$ and the coercion to submodule of $J$ and the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{coeToSubmodule} (\mathrm{I'})}{x_{4}})}$ and the preimage of the subtype of the coercion to submodule of $\mathrm{I'}$ and the coercion to submodule of $\mathrm{J'}$.

IsDedekindDomain.HeightOneSpectrum.maxPowDividingdefMathlib.RingTheory.DedekindDomain.Factorization, function or constant

Wording

no wording

English

Let $v$ be a height one spectrum of $R$. Let $I$ be an ideal of $R$. Then $\operatorname{maxPowDividing}$ applied to $v$ and $I$ is an ideal of $R$ defined as the exponentiation of $\operatorname{asIdeal}$ applied to $v$ to the count of $\operatorname{mk}$ applied to $\operatorname{asIdeal}$ applied to $v$ and the factor of $\operatorname{mk}$ applied to $I$.

Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

IsDedekindDomain.FiniteAdeleRingdefMathlib.RingTheory.DedekindDomain.FiniteAdeleRing, type

Wording

finite adele ring of R and K (from the name)

English

Let $R$ and $K$ be sets. Then a finite adele ring of $R$ and $K$ is an element of the function that maps $R$ and $K$ to the set of restricted products of the function that maps $v_{1}$ to the adic completion integer of $K$ and $v_{1}$ and the cofinite filter.

IsDedekindDomain.FiniteAdeleRing.algebraMapdefMathlib.RingTheory.DedekindDomain.FiniteAdeleRing, function or constant

Wording

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

English

Let $R$ and $K$ be sets. Then the algebra map of $R$ and $K$ is a ring homomorphism of $K$ and the set of finite adele rings of $R$ and $K$.

IsDedekindDomain.FiniteAdeleRing.ofAdicCompletiondefMathlib.RingTheory.DedekindDomain.FiniteAdeleRing, function or constant

Wording

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

English

Let $K$ be a set. Let $v$ be a height one spectrum of $R$. Then the embedding of the completion of $K$ and $v$ is a monoid homomorphism of the set of adic completions of $K$ and $v$ and the set of finite adele rings of $R$ and $K$ defined as the multiplicative single monoid homomorphism of the function that maps $w$ to the adic completion integer of $K$ and $w$ and $v$.

IsDedekindDomain.FiniteAdeleRing.unitEmbeddingdefMathlib.RingTheory.DedekindDomain.FiniteAdeleRing, function or constant

Wording

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

English

Let $R$ and $K$ be sets. Then the unit embedding of $R$ and $K$ is a monoid homomorphism of $\UnitsMACRoAO {K}$ and the set of units of the set of finite adele rings of $R$ and $K$ defined as the map of the monoid homomorphism of the algebra map of $K$ and the set of finite adele rings of $R$ and $K$.

IsDedekindDomain.HeightOneSpectrum.SupportdefMathlib.RingTheory.DedekindDomain.FiniteAdeleRing, function or constant

Wording

the support of R and k (from the docstring)

English

Let $R$ be a set. Let $k$ be an element of $K$. Then the support of $R$ and $k$ is an element of the power set of the set of height one spectra of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to $\mathrm{Lt} (1 , \operatorname{valuation} (K , v , k))$.

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Ideal.normalizedFactorsEquivSpanNormalizedFactorsdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the normalized factor equivalence span normalized factor of hr (from the name)

English

Assume that $r \neq 0$. Then the normalized factor equivalence span normalized factor of $\mathrm{hr}$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $d$ to the proposition that $d$ is an element of the normalized factor of $r$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $I$ to the proposition that $I$ is an element of the normalized factor of the span of $\operatorname{singleton}$ applied to $r$.

IsDedekindDomain.HeightOneSpectrumstructureMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, type

Wording

height one spectrum of R (from the name)

English

Let $R$ be a set. Then the height one spectra of $R$ are a basic type.

IsDedekindDomain.HeightOneSpectrum.asIdealdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a height one spectrum of $R$. Then $\operatorname{asIdeal}$ applied to $\mathrm{self}$ is an ideal of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

IsDedekindDomain.HeightOneSpectrum.comapdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the preimage of f and v (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $v$ be a height one spectrum of $S$. Then the preimage of $f$ and $v$ is a height one spectrum of $R$.

IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrumdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the equivalence maximal spectrum of hR (from the name)

English

Assume that $R$ is not a field. Then the equivalence maximal spectrum of $\mathrm{hR}$ is an equivalence from the set of height one spectra of $R$ to the set of maximal spectra of $R$.

IsDedekindDomain.HeightOneSpectrum.equivOfRingEquivdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then the equivalence of $e$ is an equivalence from the set of height one spectra of $R$ to the set of height one spectra of $S$.

IsDedekindDomain.HeightOneSpectrum.equivPrimesOverdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

no wording

English

Let $B$ be a set. Assume that $p \neq 0$. Then $\operatorname{equivPrimesOver}$ applied to $B$ and $\mathrm{hp}$ is an element of $\EquivMACRoAE {(\SubtypeSet {v}{(\divides {\operatorname{asIdeal} (v)}{\operatorname{map} (\operatorname{algebraMap} (A , B), p)})})}{\operatorname{Elem} (\operatorname{primesOver} (p , B))}$.

IsDedekindDomain.HeightOneSpectrum.ofPrimedefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the height one spectrum of hp (from the name)

English

Assume that $p$ is prime. Then the height one spectrum of $\mathrm{hp}$ is a height one spectrum of $R$.

IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEqdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the quotient equivalence product of P and e (from the name)

English

Let $I$ be an ideal of $R$. Let $P$ be a function from elements of $x_{1}$ to height one spectra of $R$. Let $e$ be a function from elements of $x_{1}$ to natural numbers. Assume that the function that maps $i_{2}$ and $j$ to $\mathrm{Neq} (P (i_{2}), P (j))$ is pairwise. Assume that $\EqtMACRoH {\FinsetProd {\FinsetunivMACRoAC}{i_{1}}{(\operatorname{asIdeal} (P (i_{1}))^ {e (i_{1})})}}{I}$. Then the quotient equivalence product of $P$ and $e$ is a ring isomorphism of the set of quotients of $R$ and $I$ and the set of functions from elements $i$ of $x_{1}$ to quotients of $R$ and $\operatorname{asIdeal} (P (i))^ {e (i)}$.

IsDedekindDomain.HeightOneSpectrum.underdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

no wording

English

Let $A$ be a set. Let $w$ be a height one spectrum of $B$. Then $\operatorname{under}$ applied to $A$ and $w$ is a height one spectrum of $A$.

IsDedekindDomain.idealFactorsEquivOfQuotEquivdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the ideal factor equivalence of f (from the name)

English

Let $f$ be a ring isomorphism of the set of quotients of $R$ and $I$ and the set of quotients of $A$ and $J$. Then the ideal factor equivalence of $f$ is an order isomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $p$ to $\divides {p}{I}$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $p_{1}$ to $\divides {p_{1}}{J}$.

IsDedekindDomain.idealFactorsFunOfQuotHomdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the ideal factor function of hf (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the ideal factor function of $\mathrm{hf}$ is an order homomorphism of $\SubtypeSet {p}{(\divides {p}{I})}$ and $\SubtypeSet {p_{1}}{(\divides {p_{1}}{J})}$.

IsDedekindDomain.normalizedFactorsEquivOfQuotEquivdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the normalized factor equivalence of f (from the name)

English

Let $f$ be a ring isomorphism of the set of quotients of $R$ and $I$ and the set of quotients of $A$ and $J$. Assume that $I$ is distinct from the bottom. Assume that $J$ is distinct from the bottom. Then the normalized factor equivalence of $f$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $L$ to the proposition that $L$ is an element of the normalized factor of $I$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $M$ to the proposition that $M$ is an element of the normalized factor of $J$.

IsDedekindDomain.primesOverFinsetdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the prime over finite set of p and B (from the name)

English

Let $p$ be an ideal of $A$. Let $B$ be a set. Then the prime over finite set of $p$ and $B$ is a finite set of the set of ideals of $B$ defined as the finite set of the factor of the map of the algebra map of $A$ and $B$ and $p$.

IsDedekindDomain.quotientEquivPiFactorsdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the quotient equivalence product factor of hI (from the name)

English

Assume that $I \neq \operatorname{bot}$. Then the quotient equivalence product factor of $\mathrm{hI}$ is a ring isomorphism of the set of quotients of $R$ and $I$ and the set of functions from elements $P$ of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{factors} (I))}{x_{1}})}$ to quotients of $R$ and $P ^ {\operatorname{count} (P , \operatorname{factors} (I))}$.

IsDedekindDomain.quotientEquivPiOfFinsetProdEqdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the quotient equivalence product of P and e (from the name)

English

Let $I$ be an ideal of $R$. Let $P$ be a function from elements of $x_{1}$ to ideals of $R$. Let $e$ be a function from elements of $x_{1}$ to natural numbers. Assume that for all elements $i_{3}$ of $x_{1}$, if $i_{3}$ is an element of $s$, then $P$ applied to $i_{3}$ is prime. Assume that for all elements $i_{2}$ of $x_{1}$, if $i_{2}$ is an element of $s$, then for all elements $j$ of $x_{1}$, if $j$ is an element of $s$, then if $i_{2} \neq j$, then $P (i_{2})\neq P (j)$. Assume that $\EqtMACRoH {\FinsetProd {s}{i_{1}}{(P (i_{1})^ {e (i_{1})})}}{I}$. Then the quotient equivalence product of $P$ and $e$ is a ring isomorphism of the set of quotients of $R$ and $I$ and the set of functions from elements $i$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ to quotients of $R$ and $P (i)^ {e (i)}$.

IsDedekindDomain.quotientEquivPiOfProdEqdefMathlib.RingTheory.DedekindDomain.Ideal.Lemmas, function or constant

Wording

the quotient equivalence product of P and e (from the name)

English

Let $I$ be an ideal of $R$. Let $P$ be a function from elements of $x_{1}$ to ideals of $R$. Let $e$ be a function from elements of $x_{1}$ to natural numbers. Assume that for all elements $i_{3}$ of $x_{1}$, $P$ applied to $i_{3}$ is prime. Assume that the function that maps $i_{2}$ and $j$ to $\mathrm{Neq} (P (i_{2}), P (j))$ is pairwise. Assume that $\EqtMACRoH {\FinsetProd {\FinsetunivMACRoAC}{i_{1}}{(P (i_{1})^ {e (i_{1})})}}{I}$. Then the quotient equivalence product of $P$ and $e$ is a ring isomorphism of the set of quotients of $R$ and $I$ and the set of functions from elements $i$ of $x_{1}$ to quotients of $R$ and $P (i)^ {e (i)}$.

Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Module.Basis.ofIsCoprimeDifferentIdealdefMathlib.RingTheory.DedekindDomain.LinearDisjoint, function or constant

Wording

the basis of b (from the name)

English

Let $A$, $B$, $x_{8}$ and $x_{9}$ be sets. Assume that $\operatorname{LinearDisjoint}$ holds for $x_{18}$ and $\SubtypeSet {x_{24}}{(\MembershipmemMACRoT {x_{19}}{x_{24}})}$. Assume that $\MaxmaxMACRoAF {\operatorname{toSubalgebra} (x_{18})}{\operatorname{toSubalgebra} (x_{19})}$ is equal to the top. Assume that the map of the algebra map of $x_{8}$ and $B$ and the different ideal of $A$ and $x_{8}$ is coprime to the map of the algebra map of $x_{9}$ and $B$ and the different ideal of $A$ and $x_{9}$. Let $b$ be a basis of $A$ and $x_{9}$. Then the basis of $b$ is a basis of $x_{8}$ and $B$.

Mathlib.RingTheory.DedekindDomain.SInteger

Set.integerdefMathlib.RingTheory.DedekindDomain.SInteger, function or constant

Wording

the integer of S and K (from the name)

English

Let $S$ be an element of the power set of the set of height one spectra of $R$. Let $K$ be a set. Then the integer of $S$ and $K$ is a subalgebra of $R$ and $K$.

Set.unitdefMathlib.RingTheory.DedekindDomain.SInteger, function or constant

Wording

the unit of S and K (from the name)

English

Let $S$ be an element of the power set of the set of height one spectra of $R$. Let $K$ be a set. Then the unit of $S$ and $K$ is a subgroup of $\UnitsMACRoAO {K}$.

Set.unitEquivUnitsIntegerdefMathlib.RingTheory.DedekindDomain.SInteger, function or constant

Wording

the unit equivalence unit integer of S and K (from the name)

English

Let $S$ be an element of $\wp \operatorname{HeightOneSpectrum} (R)$. Let $K$ be a set. Then the unit equivalence unit integer of $S$ and $K$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{unit} (S , K)}{x_{3}})}$ and $\UnitsMACRoAO {(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{integer} (S , K)}{x_{4}})})}$.

Mathlib.RingTheory.DedekindDomain.SelmerGroup

IsDedekindDomain.HeightOneSpectrum.valuationOfNeZerodefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

the valuation of v (from the name)

English

Let $v$ be a height one spectrum of $R$. Then the valuation of $v$ is a monoid homomorphism of $\UnitsMACRoAO {K}$ and the set of multiplicatives of $\Integer$.

IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroModdefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

the valuation of v and n (from the name)

English

Let $v$ be a height one spectrum of $R$. Let $n$ be a natural number. Then the valuation of $v$ and $n$ is a monoid homomorphism of the set of quotients of $\UnitsMACRoAO {K}$ and the range of the power monoid homomorphism of $n$ and the set of multiplicatives of $\mathrm{ZMod}$ applied to $n$.

IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFundefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

the valuation of v and x3 (from the name)

English

Let $v$ be a height one spectrum of $R$. Let $x_{3}$ be a unit of $K$. Then the valuation of $v$ and $x_{3}$ is a multiplicative of $\Integer$ defined as $\operatorname{ofAdd}$ applied to the difference between $\operatorname{neg}$ applied to the count of $\operatorname{mk}$ applied to $\operatorname{asIdeal}$ applied to $v$ and the factor of $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to the first element of $\operatorname{sec}$ applied to the non zero divisor of $R$ and the underlying value in the base of $x_{3}$ and $\operatorname{neg}$ applied to the count of $\operatorname{mk}$ applied to $\operatorname{asIdeal}$ applied to $v$ and the factor of $\operatorname{mk}$ applied to the span of $\operatorname{singleton}$ applied to the second element of $\operatorname{sec}$ applied to the non zero divisor of $R$ and the underlying value in the base of $x_{3}$.

IsDedekindDomain.selmerGroupdefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

no wording

English

$\operatorname{selmerGroup}$ is a subgroup of the set of quotients of $\UnitsMACRoAO {K}$ and the range of the power monoid homomorphism of $n$.

IsDedekindDomain.selmerGroup.fromUnitdefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

no wording

English

$\operatorname{fromUnit}$ is a monoid homomorphism of $\UnitsMACRoAO {R}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{selmerGroup}}{x_{3}})}$.

IsDedekindDomain.selmerGroup.fromUnitLiftdefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

no wording

English

$\operatorname{fromUnitLift}$ is a monoid homomorphism of the set of quotients of $\UnitsMACRoAO {R}$ and the range of the power monoid homomorphism of $n$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{selmerGroup}}{x_{3}})}$ defined as the composition of the induced map from the quotient by the kernel to the codomain of $\operatorname{fromUnit}$ and the monoid homomorphism of the inverse of the quotient multiplicative equivalence of $\mathrm{IsDedekindDomain\_\_selmerGroup\_\_fromUnit\_ker}$.

IsDedekindDomain.selmerGroup.valuationdefMathlib.RingTheory.DedekindDomain.SelmerGroup, function or constant

Wording

the valuation (from the name)

English

The valuation is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{selmerGroup}}{x_{3}})}$ and the set of functions from elements of $S$ to multiplicatives of $\mathrm{ZMod}$ applied to $n$.

Mathlib.RingTheory.Depth.Basic

Ideal.depthdefMathlib.RingTheory.Depth.Basic, function or constant

Wording

the depth of I and M (from the docstring)

English

Let $I$ be an ideal of $R$. Let $M$ be a module category of $R$. Then the depth of $I$ and $M$ is a natural number defined as the depth between two of $\operatorname{of}$ applied to $R$ and the set of shrinks of the set of quotients of $R$ and $I$ and $M$.

IsLocalRing.depthdefMathlib.RingTheory.Depth.Basic, function or constant

Wording

the depth of M (from the name)

English

Let $M$ be a module category of $R$. Then the depth of $M$ is a natural number defined as the depth of the maximal ideal of $R$ and $M$.

ModuleCat.depthdefMathlib.RingTheory.Depth.Basic, function or constant

Wording

the depth between two of N and M (from the docstring)

English

Let $N$ and $M$ be module categories of $R$. Then the depth between two of $N$ and $M$ is a natural number defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that for all natural numbers $i$, if $i < n$, then the set of extensions of $M$ and $i$ is a subsingleton.

Mathlib.RingTheory.Derivation.Basic

DerivationstructureMathlib.RingTheory.Derivation.Basic, type

Wording

derivation of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the derivations of $A$ and $M$ are a basic type.

Derivation.coeAddMonoidHomdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

the coercion additive monoid homomorphism (from the name)

English

The coercion additive monoid homomorphism is an additive monoid homomorphism of the set of derivations of $A$ and $M$ and the set of linear maps of $A$ and $M$.

Derivation.coeFnAddMonoidHomdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of derivations of $A$ and $M$ and the set of functions from elements of $A$ to elements of $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{Derivation\_\_coe\_zero}$ and $\mathrm{Derivation\_\_coe\_add}$.

Derivation.compAlgebraMapdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

the composition algebra map of A and d (from the name)

English

Let $A$ be a set. Let $d$ be a derivation of $B$ and $M$. Then the composition algebra map of $A$ and $d$ is a derivation of $A$ and $M$.

Derivation.compAlgebraMapLdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

the composition algebra map of B and M (from the name)

English

Let $R$, $A$, $B$ and $M$ be sets. Then the composition algebra map of $B$ and $M$ is a linear map of the set of derivations of $B$ and $M$ and the set of derivations of $A$ and $M$.

Derivation.liftOfRightInversedefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

the lift of hf and hd (from the name)

English

Assume that $\operatorname{RightInverse}$ holds for $\mathrm{f\_inv}$ and $\operatorname{coe}$ applied to $f$. Assume that for all elements $x_{6}$ of $A$, if $\EqtMACRoH {f (x_{6})}{0}$, then $\EqtMACRoH {f (d (x_{6}))}{0}$. Then the lift of $\mathrm{hf}$ and $\mathrm{hd}$ is a derivation of $M$ and $M$.

Derivation.liftOfSurjectivedefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

the lift of hf and hd (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Assume that for all elements $x_{6}$ of $A$, if $\EqtMACRoH {f (x_{6})}{0}$, then $\EqtMACRoH {f (d (x_{6}))}{0}$. Then the lift of $\mathrm{hf}$ and $\mathrm{hd}$ is a derivation of $M$ and $M$.

Derivation.llcompdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

no wording

English

$\operatorname{llcomp}$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of the set of derivations of $A$ and $M$ and the set of derivations of $A$ and $N$.

Derivation.mk'defMathlib.RingTheory.Derivation.Basic, function or constant

Wording

no wording

English

Let $D$ be a linear map of $A$ and $M$ such that for all elements $a$ and $b$ of $A$, $\EqtMACRoH {D (a \times b)}{\HSMulhSMulMACRoAL {a}{D (b)}+ \HSMulhSMulMACRoAL {b}{D (a)}}$. Then $\operatorname{mk'}$ applied to $D$ and $h$ is a derivation of $A$ and $M$.

Derivation.restrictScalarsdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $d$ be a derivation of $A$ and $M$. Then $\operatorname{restrictScalars}$ applied to $R$ and $d$ is a derivation of $A$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{toLinearMap}$ applied to $d$, $\mathrm{Derivation\_\_map\_one\_eq\_zero}$ applied to $d$ and $\operatorname{leibniz}$ applied to $d$.

LinearEquiv.compDerdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

no wording

English

Let $e$ be a linear equivalence of $M$ and $N$. Then $\operatorname{compDer}$ applied to $e$ is a linear equivalence of the set of derivations of $A$ and $M$ and the set of derivations of $A$ and $N$.

LinearMap.compDerdefMathlib.RingTheory.Derivation.Basic, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and $N$. Then $\operatorname{compDer}$ applied to $f$ is a linear map of the set of derivations of $A$ and $M$ and the set of derivations of $A$ and $N$.

Mathlib.RingTheory.Derivation.DifferentialRing

DifferentialclassMathlib.RingTheory.Derivation.DifferentialRing, predicate

Wording

R is differential (from the name)

English

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

Differential.ContainConstantsclassMathlib.RingTheory.Derivation.DifferentialRing, predicate

Wording

no wording

English

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

Differential.derivdefMathlib.RingTheory.Derivation.DifferentialRing, function or constant

Wording

the derivative (from the name)

English

The derivative is a derivation of $R$ and $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

DifferentialAlgebraclassMathlib.RingTheory.Derivation.DifferentialRing, predicate

Wording

no wording

English

Let $A$ and $B$ be sets. Then we can say that $\mathrm{DifferentialAlgebra}$ holds for $A$ and $B$.

Mathlib.RingTheory.Derivation.Lie

Derivation.Compatible.mkdefMathlib.RingTheory.Derivation.Lie, function or constant

Wording

no wording

English

Let $x_{6}$ be a derivation of $\mathrm{A'}$ and $\mathrm{A'}$. Let $y$ be a derivation of $A$ and $A$ such that $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $x_{6}$ and $\operatorname{coe}$ applied to the algebra of $A$ and $\mathrm{A'}$ is equal to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the algebra of $A$ and $\mathrm{A'}$ and $\operatorname{coe}$ applied to $y$. Then $\operatorname{mk}$ applied to $x_{6}$, $y$ and $h_{1}$ is an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{couple} (R , A , \mathrm{A'})}{x_{7}})}$ defined as $\ProdmkMACRoU {x_{6}}{y}$.

Derivation.coupledefMathlib.RingTheory.Derivation.Lie, function or constant

Wording

no wording

English

Let $R$, $A$ and $\mathrm{A'}$ be sets. Then $\operatorname{couple}$ applied to $R$, $A$ and $\mathrm{A'}$ is a Lie subalgebra of $R$ and $\mathrm{Prod}$ applied to the set of derivations of $\mathrm{A'}$ and $\mathrm{A'}$ and the set of derivations of $A$ and $A$.

Mathlib.RingTheory.Derivation.MapCoeffs

Derivation.mapCoeffsdefMathlib.RingTheory.Derivation.MapCoeffs, function or constant

Wording

no wording

English

Let $d$ be a derivation of $A$ and $M$. Then $\operatorname{mapCoeffs}$ applied to $d$ is a derivation of the set of polynomials of $A$ and the set of polynomial modules of $A$ and $M$.

Differential.implicitDerivdefMathlib.RingTheory.Derivation.MapCoeffs, function or constant

Wording

the implicit derivative of v (from the name)

English

Let $v$ be a polynomial of $A$. Then the implicit derivative of $v$ is a derivation of the set of polynomials of $A$ and the set of polynomials of $A$ defined as $\operatorname{mapCoeffs} + \HSMulhSMulMACRoAL {v}{\operatorname{restrictScalars} (\Integer , \operatorname{derivative'})}$.

Differential.mapCoeffsdefMathlib.RingTheory.Derivation.MapCoeffs, function or constant

Wording

no wording

English

$\operatorname{mapCoeffs}$ is a derivation of the set of polynomials of $A$ and the set of polynomials of $A$ defined as $\operatorname{compDer}$ applied to the equivalence polynomial self and $\operatorname{mapCoeffs}$ applied to the derivative.

Mathlib.RingTheory.Derivation.ToSquareZero

derivationToSquareZeroEquivLiftdefMathlib.RingTheory.Derivation.ToSquareZero, function or constant

Wording

the derivation to square zero equivalence lift of I and hI (from the name)

English

Let $I$ be an ideal of $B$ such that $\EqtMACRoH {I ^ {2}}{\operatorname{bot}}$. Then the derivation to square zero equivalence lift of $I$ and $\mathrm{hI}$ is an element of $\EquivMACRoAE {\mathrm{Derivation} (A , \SubtypeSet {x_{6}}{(\MembershipmemMACRoT {I}{x_{6}})})}{(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_} (R , I), f)}{\operatorname{toAlgHom} (A , \operatorname{Quotient} (B , I))})})}$.

derivationToSquareZeroOfLiftdefMathlib.RingTheory.Derivation.ToSquareZero, function or constant

Wording

the derivation to square zero of I and f (from the name)

English

Let $I$ be an ideal of $B$ such that $I ^ {2}$ is equal to the bottom. Let $f$ be an algebra homomorphism of $A$ and $B$ such that the composition of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $f$ is equal to the algebra homomorphism of $A$ and the set of quotients of $B$ and $I$. Then the derivation to square zero of $I$ and $f$ is a derivation of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {I}{x_{6}})}$.

diffToIdealOfQuotientCompEqdefMathlib.RingTheory.Derivation.ToSquareZero, function or constant

Wording

the difference to ideal of x5 and x6 (from the name)

English

Let $I$ be an ideal of $B$. Let $x_{5}$ and $x_{6}$ be algebra homomorphisms of $A$ and $B$ such that the composition of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $x_{5}$ is equal to the composition of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $x_{6}$. Then the difference to ideal of $x_{5}$ and $x_{6}$ is a linear map of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {I}{x_{7}})}$.

liftOfDerivationToSquareZerodefMathlib.RingTheory.Derivation.ToSquareZero, function or constant

Wording

the lift of I and f (from the name)

English

Let $I$ be an ideal of $B$ such that $I ^ {2}$ is equal to the bottom. Let $f$ be a derivation of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {I}{x_{6}})}$. Then the lift of $I$ and $f$ is an algebra homomorphism of $A$ and $B$.

Mathlib.RingTheory.DiscreteValuationRing.Basic

IsDiscreteValuationRingclassMathlib.RingTheory.DiscreteValuationRing.Basic, predicate

Wording

R is a discrete valuation ring (from the name)

English

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

IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorizationdefMathlib.RingTheory.DiscreteValuationRing.Basic, predicate

Wording

R has unit multiplicative power irreducible factorizations (from the name)

English

Let $R$ be a set. Then $R$ has unit multiplicative power irreducible factorizations, if there exists an element $p$ of $R$, such that $p$ is irreducible and for all elements $x_{1}$ of $R$, if $x_{1} \neq 0$, then there exists a natural number $n$ such that $\mathrm{Associated}$ holds for $p ^ {n}$ and $x_{1}$.

IsDiscreteValuationRing.addValdefMathlib.RingTheory.DiscreteValuationRing.Basic, function or constant

Wording

the additive value of R (from the name)

English

Let $R$ be a set. Then the additive value of $R$ is an additive valuation of $R$ and the set of natural numbers.

IsDiscreteValuationRing.idealOrderIsoENatdefMathlib.RingTheory.DiscreteValuationRing.Basic, function or constant

Wording

the ideal order isomorphism natural number of R (from the name)

English

Let $R$ be a set. Then the ideal order isomorphism natural number of $R$ is an order isomorphism of the set of ideals of $R$ and the set of order duals of the set of natural numbers.

IsDiscreteValuationRing.quotientdefMathlib.RingTheory.DiscreteValuationRing.Basic, function or constant

Wording

the quotient of x1 and y (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Then the quotient of $x_{1}$ and $y$ is an element of $R$ defined as $\iteMACRoG {(\EqtMACRoH {y}{0})}{0}{\mathrm{dite} (\divides {y}{x_{1}}, \lambda h . \operatorname{choose} (h), \lambda h_{1} . 0)}$.

IsDiscreteValuationRing.remainderdefMathlib.RingTheory.DiscreteValuationRing.Basic, function or constant

Wording

the remainder of x1 and y (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Then the remainder of $x_{1}$ and $y$ is an element of $R$ defined as $\iteMACRoG {(\divides {y}{x_{1}})}{0}{x_{1}}$.

IsDiscreteValuationRing.toWithBotNatdefMathlib.RingTheory.DiscreteValuationRing.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Then $\operatorname{toWithBotNat}$ applied to $x_{1}$ is an element of $\mathrm{WithBot}$ applied to $\Natural$ defined as $\operatorname{addVal}$ applied to $R$ and $x_{1}$.