Definitions: Mathlib.RingTheory, part 3 of 6

HomogeneousLocalizationdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, type

Wording

homogeneous localization of x4 and x5 (from the name)

English

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be a submonoid of $A$. Then a homogeneous localization of $x_{4}$ and $x_{5}$ is an element of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $\operatorname{embedding}$ applied to $x_{5}$.

HomogeneousLocalization.AtPrimedefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, type

Wording

no wording

English

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be an ideal of $A$. Then an element of $\operatorname{AtPrime}$ applied to $x_{4}$ and $x_{5}$ is an element of the function that maps $x_{4}$ and $x_{5}$ to the set of homogeneous localizations of $x_{4}$ and the complement of $x_{5}$.

HomogeneousLocalization.AwaydefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, type

Wording

no wording

English

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $f$ be an element of $A$. Then an element of $\operatorname{Away}$ applied to $x_{4}$ and $f$ is an element of the function that maps $x_{4}$ and $f$ to the set of homogeneous localizations of $x_{4}$ and the power of $f$.

HomogeneousLocalization.Away.isLocalizationElemdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the element of hf and hg (from the docstring)

English

Assume that $\MembershipmemMACRoT {x_{3} (d)}{f}$. Assume that $\MembershipmemMACRoT {x_{3} (e)}{g}$. Then the element of $\mathrm{hf}$ and $\mathrm{hg}$ is an element of $\operatorname{Away}$ applied to $x_{3}$ and $f$.

HomogeneousLocalization.Away.mapdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the map of g and f (from the name)

English

Let $g$ be a graded ring homomorphism of $x_{6}$ and $x_{11}$. Let $f$ be an element of $A$. Then the map of $g$ and $f$ is a ring homomorphism of $\operatorname{Away}$ applied to $x_{6}$ and $f$ and $\operatorname{Away}$ applied to $x_{11}$ and $g$ applied to $f$.

HomogeneousLocalization.Away.mkdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

no wording

English

Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\MembershipmemMACRoT {x_{6} (d)}{f}$. Let $n$ be a natural number. Let $x_{8}$ be an element of $A$ such that $\MembershipmemMACRoT {x_{6} (\HSMulhSMulMACRoAL {n}{d})}{x_{8}}$. Then $\operatorname{mk}$ applied to $x_{6}$, $\mathrm{hf}$, $n$, $x_{8}$ and $\mathrm{hx}$ is an element of $\operatorname{Away}$ applied to $x_{6}$ and $f$.

HomogeneousLocalization.NumDenSameDegstructureMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, type

Wording

numerator denominator same degree of x4 and x5 (from the name)

English

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be a submonoid of $A$. Then the numerator denominator same degrees of $x_{4}$ and $x_{5}$ are a basic type.

HomogeneousLocalization.NumDenSameDeg.degdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the degree of self (from the name)

English

Let $\mathrm{self}$ be a numerator denominator same degree of $x_{4}$ and $x_{5}$. Then the degree of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

HomogeneousLocalization.NumDenSameDeg.dendefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the denominator of self (from the name)

English

Let $\mathrm{self}$ be a numerator denominator same degree of $x_{4}$ and $x_{5}$. Then the denominator of $\mathrm{self}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {x_{4} (\operatorname{deg} (\mathrm{self}))}{x_{6}})}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

HomogeneousLocalization.NumDenSameDeg.embeddingdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the embedding of x5 and p (from the name)

English

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be a submonoid of $A$. Let $p$ be a numerator denominator same degree of $x_{4}$ and $x_{5}$. Then the embedding of $x_{5}$ and $p$ is a localization of $x_{5}$ defined as $\operatorname{mk}$ applied to the numerator of $p$ and the denominator of $p$.

HomogeneousLocalization.NumDenSameDeg.mapdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the map of f and c (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{4}$ and $x_{8}$ such that $x_{9}$ is less than or equal to the preimage of $f$ and $x_{10}$. Let $c$ be a numerator denominator same degree of $x_{4}$ and $x_{9}$. Then the map of $f$ and $c$ is a numerator denominator same degree of $x_{8}$ and $x_{10}$.

HomogeneousLocalization.NumDenSameDeg.numdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the numerator of self (from the name)

English

Let $\mathrm{self}$ be a numerator denominator same degree of $x_{4}$ and $x_{5}$. Then the numerator of $\mathrm{self}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {x_{4} (\operatorname{deg} (\mathrm{self}))}{x_{6}})}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

HomogeneousLocalization.awayMapdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

no wording

English

Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\MembershipmemMACRoT {x_{6} (e)}{g}$. Assume that $\EqtMACRoH {x_{8}}{f \times g}$. Then $\operatorname{awayMap}$ applied to $x_{6}$, $\mathrm{hg}$ and $\mathrm{hx}$ is a ring homomorphism of $\operatorname{Away}$ applied to $x_{6}$ and $f$ and $\operatorname{Away}$ applied to $x_{6}$ and $x_{8}$.

HomogeneousLocalization.awayMapₐdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

no wording

English

Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\MembershipmemMACRoT {x_{6} (e)}{g}$. Assume that $\EqtMACRoH {x_{8}}{f \times g}$. Then $\mathrm{HomogeneousLocalization\_\_awayMap\_u2090\_}$ applied to $x_{6}$, $\mathrm{hg}$ and $\mathrm{hx}$ is an algebra homomorphism of $\operatorname{Away}$ applied to $x_{6}$ and $f$ and $\operatorname{Away}$ applied to $x_{6}$ and $x_{8}$ defined as $\operatorname{mk}$ applied to $\operatorname{awayMap}$ applied to $x_{6}$, $\mathrm{hg}$ and $\mathrm{hx}$ and the function that maps $x_{9}$ to $\mathrm{HomogeneousLocalization\_\_awayMap\_fromZeroRingHom}$ applied to $x_{6}$, $\mathrm{hg}$, $\mathrm{hx}$ and $x_{9}$.

HomogeneousLocalization.degdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the degree of f (from the name)

English

Let $f$ be a homogeneous localization of $x_{4}$ and $x_{5}$. Then the degree of $f$ is an element of $x$ defined as the degree of $\operatorname{out}$ applied to $f$.

HomogeneousLocalization.dendefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the denominator of f (from the name)

English

Let $f$ be a homogeneous localization of $x_{4}$ and $x_{5}$. Then the denominator of $f$ is an element of $A$ defined as the denominator of $\operatorname{out}$ applied to $f$.

HomogeneousLocalization.fromZeroRingHomdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

no wording

English

Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{8}$ be a submonoid of $A$. Then $\operatorname{fromZeroRingHom}$ applied to $x_{6}$ and $x_{8}$ is a ring homomorphism of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{6} (0)}{x_{9}})}$ and the set of homogeneous localizations of $x_{6}$ and $x_{8}$.

HomogeneousLocalization.localRingHomdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the local ring homomorphism of I and J (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{6}$ and $x_{11}$. Let $I$ be an ideal of $A$. Let $J$ be an ideal of $B$ such that $I$ is equal to the preimage of $J$ under $f$. Then the local ring homomorphism of $I$ and $J$ is a ring homomorphism of $\operatorname{AtPrime}$ applied to $x_{6}$ and $I$ and $\operatorname{AtPrime}$ applied to $x_{11}$ and $J$.

HomogeneousLocalization.mapdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the map of g and comap_le (from the name)

English

Let $g$ be a graded ring homomorphism of $x_{6}$ and $x_{11}$ such that $P$ is less than or equal to the preimage of $g$ and $Q$. Then the map of $g$ and $\mathrm{comap\_le}$ is a ring homomorphism of the set of homogeneous localizations of $x_{6}$ and $P$ and the set of homogeneous localizations of $x_{11}$ and $Q$.

HomogeneousLocalization.mapIddefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the map identity of x6 and h1 (from the name)

English

Let $x_{6}$ be a function from elements of $x$ to elements of $x_{1}$. Assume that $P \leq Q$. Then the map identity of $x_{6}$ and $h_{1}$ is a ring homomorphism of the set of homogeneous localizations of $x_{6}$ and $P$ and the set of homogeneous localizations of $x_{6}$ and $Q$ defined as the map of the identity graded ring homomorphism of $x_{6}$ and $h_{1}$.

HomogeneousLocalization.mkdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

no wording

English

Let $y$ be a numerator denominator same degree of $x_{4}$ and $x_{5}$. Then $\operatorname{mk}$ applied to $y$ is a homogeneous localization of $x_{4}$ and $x_{5}$ defined as $\operatorname{mk''}$ applied to $y$.

HomogeneousLocalization.numdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the numerator of f (from the name)

English

Let $f$ be a homogeneous localization of $x_{4}$ and $x_{5}$. Then the numerator of $f$ is an element of $A$ defined as the numerator of $\operatorname{out}$ applied to $f$.

HomogeneousLocalization.valdefMathlib.RingTheory.GradedAlgebra.HomogeneousLocalization, function or constant

Wording

the value of y (from the name)

English

Let $y$ be a homogeneous localization of $x_{4}$ and $x_{5}$. Then the value of $y$ is a localization of $x_{5}$.

Mathlib.RingTheory.GradedAlgebra.Radical

HomogeneousIdeal.radicaldefMathlib.RingTheory.GradedAlgebra.Radical, function or constant

Wording

the radical of I (from the docstring)

English

Let $I$ be a homogeneous ideal of $x_{6}$. Then the radical of $I$ is a homogeneous ideal of $x_{6}$.

Mathlib.RingTheory.GradedAlgebra.RingHom

GradedRingHomstructureMathlib.RingTheory.GradedAlgebra.RingHom, type

Wording

graded ring homomorphism of x7 and x8 (from the name)

English

Let $x_{7}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{8}$ be a function from elements of $x$ to elements of $x_{2}$. Then the graded ring homomorphisms of $x_{7}$ and $x_{8}$ are a basic type.

GradedRingHom.compdefMathlib.RingTheory.GradedAlgebra.RingHom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a graded ring homomorphism of $x_{11}$ and $x_{12}$. Let $f$ be a graded ring homomorphism of $x_{10}$ and $x_{11}$. Then the composition of $g$ and $f$ is a graded ring homomorphism of $x_{10}$ and $x_{12}$.

GradedRingHom.copydefMathlib.RingTheory.GradedAlgebra.RingHom, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{7}$ and $x_{8}$. 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 graded ring homomorphism of $x_{7}$ and $x_{8}$.

GradedRingHom.gradedAddHomdefMathlib.RingTheory.GradedAlgebra.RingHom, function or constant

Wording

the graded additive homomorphism of f and i (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{7}$ and $x_{8}$. Let $i$ be an element of $x$. Then the graded additive homomorphism of $f$ and $i$ is an additive monoid homomorphism of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{7} (i)}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {x_{8} (i)}{x_{10}})}$.

GradedRingHom.gradedZeroRingHomdefMathlib.RingTheory.GradedAlgebra.RingHom, function or constant

Wording

the graded zero ring homomorphism of f (from the name)

English

Let $f$ be a graded ring homomorphism of $x_{7}$ and $x_{8}$. Then the graded zero ring homomorphism of $f$ is a ring homomorphism of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {x_{7} (0)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {x_{8} (0)}{x_{11}})}$.

GradedRingHom.iddefMathlib.RingTheory.GradedAlgebra.RingHom, function or constant

Wording

the identity graded ring homomorphism of x4 (from the docstring)

English

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Then the identity graded ring homomorphism of $x_{4}$ is a graded ring homomorphism of $x_{4}$ and $x_{4}$ defined as $\operatorname{mk}$ applied to the identity ring homomorphism of $A$ and the function that maps $x_{5}$, $x_{6}$ and $h$ to $h$.

GradedRingHom.ofClassdefMathlib.RingTheory.GradedAlgebra.RingHom, function or constant

Wording

the graded ring homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the graded ring homomorphism of $f$ is a graded ring homomorphism of $x_{7}$ and $x_{8}$ defined as $\operatorname{mk}$ applied to the ring homomorphism of $f$ and the function that maps $x_{10}$ and $x_{11}$ to $\mathrm{Graded\_\_map\_mem}$ applied to $f$.

Mathlib.RingTheory.GradedAlgebra.TensorProduct

GradedAlgHom.includeRightdefMathlib.RingTheory.GradedAlgebra.TensorProduct, function or constant

Wording

no wording

English

Let $S$ be a set. Let $x_{7}$ be a function from elements of $x$ to submodules of $R$ and $A$. Then $\operatorname{includeRight}$ applied to $S$ and $x_{7}$ is a graded algebra homomorphism of $x_{7}$ and the function that maps $x_{10}$ to $\operatorname{restrictScalars}$ applied to $R$ and the base change of $S$ and $x_{7}$ applied to $x_{10}$.

GradedAlgHom.liftEquivdefMathlib.RingTheory.GradedAlgebra.TensorProduct, function or constant

Wording

the lift equivalence of x9 and x10 (from the name)

English

Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{10}$ be a function from elements of $x$ to submodules of $S$ and $B$. Then the lift equivalence of $x_{9}$ and $x_{10}$ is an equivalence from the set of graded algebra homomorphisms of $x_{9}$ and the function that maps $x_{15}$ to $\operatorname{restrictScalars}$ applied to $R$ and $x_{10}$ applied to $x_{15}$ to the set of graded algebra homomorphisms of the function that maps $x_{16}$ to the base change of $S$ and $x_{9}$ applied to $x_{16}$ and $x_{10}$.

Mathlib.RingTheory.Grassmannian

Module.GrassmannianstructureMathlib.RingTheory.Grassmannian, type

Wording

no wording

English

Let $R$ and $M$ be sets. Let $k$ be a natural number. Then the elements of $\operatorname{Grassmannian}$ applied to $R$, $M$ and $k$ are a basic type.

Module.Grassmannian.baseChangeMkQdefMathlib.RingTheory.Grassmannian, function or constant

Wording

the base change of B and N (from the name)

English

Let $B$ be a set. Let $N$ be a submodule of $A$ and the set of tensor products of $A$ and $M$. Then the base change of $B$ and $N$ is a linear map of the set of tensor products of $B$ and $M$ and the set of tensor products of $B$ and the set of quotients of the set of tensor products of $A$ and $M$ and $N$ defined as the composition of the base change of $B$ and $\operatorname{mkQ}$ applied to $N$ and $\operatorname{toLinearMap}$ applied to the inverse of $\operatorname{cancelBaseChange}$ applied to $R$, $A$, $B$, $B$ and $M$.

Module.Grassmannian.baseChangeMkQEquivdefMathlib.RingTheory.Grassmannian, function or constant

Wording

the base change equivalence of N (from the name)

English

Let $N$ be a submodule of $A$ and the set of tensor products of $A$ and $M$. Then the base change equivalence of $N$ is a linear equivalence of the set of quotients of the set of tensor products of $B$ and $M$ and the kernel of the base change of $B$ and $N$ and the set of tensor products of $B$ and the set of quotients of the set of tensor products of $A$ and $M$ and $N$ defined as the quotient kernel equivalence of the base change of $B$ and $N$ and $\mathrm{Module\_\_Grassmannian\_\_baseChangeMkQ\_surjective}$ applied to $N$.

Module.Grassmannian.functordefMathlib.RingTheory.Grassmannian, function or constant

Wording

the functor of k (from the name)

English

Let $k$ be a natural number. Then the functor of $k$ is a functor of the set of commutative algebra categories of $R$ and the set of sets.

Module.Grassmannian.mapdefMathlib.RingTheory.Grassmannian, function or constant

Wording

the map of f and N (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $N$ be an element of $\operatorname{Grassmannian}$ applied to $A$, the set of tensor products of $A$ and $M$ and $k$. Then the map of $f$ and $N$ is an element of $\operatorname{Grassmannian}$ applied to $B$, the set of tensor products of $B$ and $M$ and $k$.

Mathlib.RingTheory.HahnSeries.Addition

HahnSeries.addOppositeEquivdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the additive opposite equivalence (from the name)

English

The additive opposite equivalence is an additive equivalence of the set of Hahn series of $x$ and the set of additive opposites of $R$ and the set of additive opposites of the set of Hahn series of $x$ and $R$.

HahnSeries.coeff.addMonoidHomdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the additive monoid homomorphism of g (from the name)

English

Let $g$ be an element of $x$. Then the additive monoid homomorphism of $g$ is an additive monoid homomorphism of the set of Hahn series of $x$ and $R$ and $R$.

HahnSeries.coeff.linearMapdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the linear map of g (from the name)

English

Let $g$ be an element of $x$. Then the linear map of $g$ is a linear map of the set of Hahn series of $x$ and $V$ and $V$.

HahnSeries.embDomainLinearMapdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the embedding domain linear map of f (from the name)

English

Let $f$ be an order embedding of $x$ and $x_{1}$. Then the embedding domain linear map of $f$ is a linear map of the set of Hahn series of $x$ and $R$ and the set of Hahn series of $x_{1}$ and $R$.

HahnSeries.ofFinsuppLinearMapdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the Hahn series of R (from the name)

English

Let $R$ be a set. Then the Hahn series of $R$ is a linear map of $\FinsuppMACRoQ {x}{V}$ and the set of Hahn series of $x$ and $V$.

HahnSeries.single.addMonoidHomdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the additive monoid homomorphism of a (from the name)

English

Let $a$ be an element of $x$. Then the additive monoid homomorphism of $a$ is an additive monoid homomorphism of $R$ and the set of Hahn series of $x$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $a$ and $\mathrm{HahnSeries\_\_single\_add}$ applied to $a$.

HahnSeries.single.linearMapdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

the linear map of a (from the name)

English

Let $a$ be an element of $x$. Then the linear map of $a$ is a linear map of $V$ and the set of Hahn series of $x$ and $V$.

HahnSeries.truncLTLinearMapdefMathlib.RingTheory.HahnSeries.Addition, function or constant

Wording

no wording

English

Let $R$ be a set. Let $c$ be an element of $x$. Then $\operatorname{truncLTLinearMap}$ applied to $R$ and $c$ is a linear map of the set of Hahn series of $x$ and $V$ and the set of Hahn series of $x$ and $V$.

Mathlib.RingTheory.HahnSeries.Basic

HahnSeriesstructureMathlib.RingTheory.HahnSeries.Basic, type

Wording

Hahn series of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the Hahn series of $x$ and $R$ are a basic type.

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

Wording

the coefficient function of self and x3 (from the docstring)

English

Let $\mathrm{self}$ be a Hahn series of $x$ and $R$. Let $x_{3}$ be an element of $x$. Then the coefficient function of $\mathrm{self}$ and $x_{3}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

HahnSeries.embDomaindefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the embedding domain of f and x5 (from the name)

English

Let $f$ be an order embedding of $x$ and $x_{1}$. Let $x_{5}$ be a Hahn series of $x$ and $R$. Then the embedding domain of $f$ and $x_{5}$ is a Hahn series of $x_{1}$ and $R$.

HahnSeries.iterateEquivdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

no wording

English

$\operatorname{iterateEquiv}$ is an equivalence from the set of Hahn series of $x$ and the set of Hahn series of $x_{1}$ and $R$ to the set of Hahn series of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $R$.

HahnSeries.leadingCoeffdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the leading coefficient of x3 (from the name)

English

Let $x_{3}$ be a Hahn series of $x$ and $R$. Then the leading coefficient of $x_{3}$ is an element of $R$ defined as $\operatorname{recTopCoe}$ applied to $0$, $\operatorname{coeff}$ applied to $x_{3}$ and the order top of $x_{3}$.

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

Wording

the map of x4 and f (from the name)

English

Let $x_{4}$ be a Hahn series of $x$ and $R$. Let $f$ be an element of $F$. Then the map of $x_{4}$ and $f$ is a Hahn series of $x$ and $S$.

HahnSeries.ofFinsuppdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the Hahn series (from the name)

English

The Hahn series is a zero homomorphism of $\FinsuppMACRoQ {x}{R}$ and the set of Hahn series of $x$ and $R$.

HahnSeries.ofIteratedefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the Hahn series of x5 (from the name)

English

Let $x_{5}$ be a Hahn series of $x$ and the set of Hahn series of $x_{1}$ and $R$. Then the Hahn series of $x_{5}$ is a Hahn series of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $R$.

HahnSeries.ofSuppBddBelowdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the Hahn series of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $R$ such that the support of $f$ is bounded below. Then the Hahn series of $f$ and $\mathrm{hf}$ is a Hahn series of $x$ and $R$.

HahnSeries.orderdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the order of x4 (from the docstring)

English

Let $x_{4}$ be a Hahn series of $x$ and $R$. Then the order of $x_{4}$ is an element of $x$.

HahnSeries.orderTopdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the order top of x3 (from the name)

English

Let $x_{3}$ be a Hahn series of $x$ and $R$. Then the order top of $x_{3}$ is an element of $\mathrm{WithTop}$ applied to $x$.

HahnSeries.singledefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{single}$ applied to $a$ is a zero homomorphism of $R$ and the set of Hahn series of $x$ and $R$.

HahnSeries.supportdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

the support of x3 (from the docstring)

English

Let $x_{3}$ be a Hahn series of $x$ and $R$. Then the support of $x_{3}$ is an element of $\wp x$ defined as the support of $\operatorname{coeff}$ applied to $x_{3}$.

HahnSeries.toIteratedefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

no wording

English

Let $x_{5}$ be a Hahn series of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $R$. Then $\operatorname{toIterate}$ applied to $x_{5}$ is a Hahn series of $x$ and the set of Hahn series of $x_{1}$ and $R$.

HahnSeries.truncLTdefMathlib.RingTheory.HahnSeries.Basic, function or constant

Wording

no wording

English

Let $c$ be an element of $x$. Then $\operatorname{truncLT}$ applied to $c$ is a zero homomorphism of the set of Hahn series of $x$ and $R$ and the set of Hahn series of $x$ and $R$.

Mathlib.RingTheory.HahnSeries.Binomial

HahnSeries.SummableFamily.binomialFamilydefMathlib.RingTheory.HahnSeries.Binomial, function or constant

Wording

the binomial family of x7 and r (from the name)

English

Let $x_{7}$ be a Hahn series of $x$ and $A$. Let $r$ be an element of $R$. Then the binomial family of $x_{7}$ and $r$ is a summable family of $A$ and $\Natural$ defined as the power series family of $x_{7} - 1$ and the binomial series of $A$ and $r$.

Mathlib.RingTheory.HahnSeries.Cardinal

HahnSeries.cardSuppdefMathlib.RingTheory.HahnSeries.Cardinal, function or constant

Wording

the cardinality of the support of x3 (from the docstring)

English

Let $x_{3}$ be a Hahn series of $x$ and $R$. Then the cardinality of the support of $x_{3}$ is a cardinal defined as $\operatorname{mk}$ applied to the set of elements of the support of $x_{3}$.

HahnSeries.cardSuppLTAddSubgroupdefMathlib.RingTheory.HahnSeries.Cardinal, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{1}$ be a cardinal. Then $\operatorname{cardSuppLTAddSubgroup}$ applied to $x$, $R$ and $x_{1}$ is an additive subgroup of the set of Hahn series of $x$ and $R$.

HahnSeries.cardSuppLTAddSubmonoiddefMathlib.RingTheory.HahnSeries.Cardinal, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{1}$ be a cardinal. Then $\operatorname{cardSuppLTAddSubmonoid}$ applied to $x$, $R$ and $x_{1}$ is an additive submonoid of the set of Hahn series of $x$ and $R$.

HahnSeries.cardSuppLTSubfielddefMathlib.RingTheory.HahnSeries.Cardinal, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{1}$ be a cardinal. Then $\operatorname{cardSuppLTSubfield}$ applied to $x$, $R$ and $x_{1}$ is a subfield of the set of Hahn series of $x$ and $R$.

HahnSeries.cardSuppLTSubringdefMathlib.RingTheory.HahnSeries.Cardinal, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{1}$ be a cardinal. Then $\operatorname{cardSuppLTSubring}$ applied to $x$, $R$ and $x_{1}$ is a subring of the set of Hahn series of $x$ and $R$.

Mathlib.RingTheory.HahnSeries.HEval

HahnSeries.SummableFamily.powerSeriesFamilydefMathlib.RingTheory.HahnSeries.HEval, function or constant

Wording

the power series family of x6 and f (from the name)

English

Let $x_{6}$ be a Hahn series of $x$ and $V$. Let $f$ be a power series of $R$. Then the power series family of $x_{6}$ and $f$ is a summable family of $V$ and $\Natural$ defined as the scalar multiple family of the function that maps $n$ to $\operatorname{coeff}$ applied to $n$ and $f$ and the power of $x_{6}$.

PowerSeries.hevaldefMathlib.RingTheory.HahnSeries.HEval, function or constant

Wording

no wording

English

Let $x_{4}$ be a Hahn series of $x$ and $R$. Then $\operatorname{heval}$ applied to $x_{4}$ is an algebra homomorphism of the set of power series of $R$ and the set of Hahn series of $x$ and $R$.

Mathlib.RingTheory.HahnSeries.Lex

HahnSeries.archimedeanClassOrderIsoWithTopdefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

the archimedean class order isomorphism with top of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the archimedean class order isomorphism with top of $x$ and $R$ is an order isomorphism of the set of archimedean classes of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $\mathrm{WithTop}$ applied to $x$ defined as the composition of the inverse of $\operatorname{withTopOrderIso}$ applied to $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $\operatorname{withTopCongr}$ applied to the finite archimedean class order isomorphism of $x$ and $R$.

HahnSeries.embDomainOrderAddMonoidHomdefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

the embedding domain order additive monoid homomorphism of f (from the name)

English

Let $f$ be an order embedding of $x$ and $x_{3}$. Then the embedding domain order additive monoid homomorphism of $f$ is an order additive monoid homomorphism of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $\mathrm{Lex}$ applied to the set of Hahn series of $x_{3}$ and $R$.

HahnSeries.embDomainOrderEmbeddingdefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

the embedding domain order embedding of f (from the name)

English

Let $f$ be an order embedding of $x$ and $x_{3}$. Then the embedding domain order embedding of $f$ is an order embedding of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $\mathrm{Lex}$ applied to the set of Hahn series of $x_{3}$ and $R$.

HahnSeries.finiteArchimedeanClassOrderHomInvLexdefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Then $\operatorname{finiteArchimedeanClassOrderHomInvLex}$ applied to $x$ and $R$ is an order homomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and the set of finite archimedean classes of $R$ and the set of finite archimedean classes of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$.

HahnSeries.finiteArchimedeanClassOrderHomLexdefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Then $\operatorname{finiteArchimedeanClassOrderHomLex}$ applied to $x$ and $R$ is an order homomorphism of the set of finite archimedean classes of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and the set of finite archimedean classes of $R$.

HahnSeries.finiteArchimedeanClassOrderIsodefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

the finite archimedean class order isomorphism of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the finite archimedean class order isomorphism of $x$ and $R$ is an order isomorphism of the set of finite archimedean classes of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $x$ defined as the composition of $\operatorname{finiteArchimedeanClassOrderIsoLex}$ applied to $x$ and $R$ and $\operatorname{prodUnique}$ applied to $x$ and the set of finite archimedean classes of $R$.

HahnSeries.finiteArchimedeanClassOrderIsoLexdefMathlib.RingTheory.HahnSeries.Lex, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Then $\operatorname{finiteArchimedeanClassOrderIsoLex}$ applied to $x$ and $R$ is an order isomorphism of the set of finite archimedean classes of $\mathrm{Lex}$ applied to the set of Hahn series of $x$ and $R$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and the set of finite archimedean classes of $R$.

Mathlib.RingTheory.HahnSeries.Multiplication

HahnModuledefMathlib.RingTheory.HahnSeries.Multiplication, type

Wording

Hahn module of R and V (from the name)

English

Let $x$, $R$ and $V$ be sets. Then a Hahn module of $R$ and $V$ is an element of the function that maps $x$, $R$ and $V$ to the set of Hahn series of $x$ and $V$.

HahnModule.ofdefMathlib.RingTheory.HahnSeries.Multiplication, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{of}$ applied to $R$ is an equivalence from the set of Hahn series of $x$ and $V$ to the set of Hahn modules of $R$ and $V$ defined as the identity of the set of Hahn series of $x$ and $V$.

HahnSeries.CdefMathlib.RingTheory.HahnSeries.Multiplication, function or constant

Wording

no wording

English

$\operatorname{C}$ is a ring homomorphism of $R$ and the set of Hahn series of $x$ and $R$.

HahnSeries.embDomainAlgHomdefMathlib.RingTheory.HahnSeries.Multiplication, function or constant

Wording

the embedding domain algebra homomorphism of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{6}$ such that $\operatorname{coe}$ applied to $f$ is injective and for all elements $g$ of $x$, for all elements $\mathrm{g'}$ of $x$, $f (g)\leq f (\mathrm{g'})$, if and only if $g \leq \mathrm{g'}$. Then the embedding domain algebra homomorphism of $f$ is an algebra homomorphism of the set of Hahn series of $x$ and $A$ and the set of Hahn series of $x_{6}$ and $A$.

HahnSeries.embDomainRingHomdefMathlib.RingTheory.HahnSeries.Multiplication, function or constant

Wording

the embedding domain ring homomorphism of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{3}$ such that $\operatorname{coe}$ applied to $f$ is injective and for all elements $g$ of $x$, for all elements $\mathrm{g'}$ of $x$, $f (g)\leq f (\mathrm{g'})$, if and only if $g \leq \mathrm{g'}$. Then the embedding domain ring homomorphism of $f$ is a ring homomorphism of the set of Hahn series of $x$ and $R$ and the set of Hahn series of $x_{3}$ and $R$.

HahnSeries.orderTopSubOnePosdefMathlib.RingTheory.HahnSeries.Multiplication, function or constant

Wording

the order top difference one positive part of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the order top difference one positive part of $x$ and $R$ is a subgroup of the set of units of the set of Hahn series of $x$ and $R$.

Mathlib.RingTheory.HahnSeries.PowerSeries

HahnSeries.ofPowerSeriesdefMathlib.RingTheory.HahnSeries.PowerSeries, function or constant

Wording

the Hahn series of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the Hahn series of $x$ and $R$ is a ring homomorphism of the set of power series of $R$ and the set of Hahn series of $x$ and $R$.

HahnSeries.ofPowerSeriesAlgdefMathlib.RingTheory.HahnSeries.PowerSeries, function or constant

Wording

the Hahn series of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the Hahn series of $x$ and $R$ is an algebra homomorphism of the set of power series of $A$ and the set of Hahn series of $x$ and $A$.

HahnSeries.toMvPowerSeriesdefMathlib.RingTheory.HahnSeries.PowerSeries, function or constant

Wording

the multivariate power series (from the name)

English

The multivariate power series is a ring isomorphism of the set of Hahn series of $\FinsuppMACRoQ {x_{1}}{\Natural}$ and $R$ and the set of multivariate power series of $x_{1}$ and $R$.

HahnSeries.toPowerSeriesdefMathlib.RingTheory.HahnSeries.PowerSeries, function or constant

Wording

the power series (from the name)

English

The power series is a ring isomorphism of the set of Hahn series of $\Natural$ and $R$ and the set of power series of $R$.

HahnSeries.toPowerSeriesAlgdefMathlib.RingTheory.HahnSeries.PowerSeries, function or constant

Wording

the power series algebra of R (from the name)

English

Let $R$ be a set. Then the power series algebra of $R$ is an algebra isomorphism of the set of Hahn series of $\Natural$ and $A$ and the set of power series of $A$.

Mathlib.RingTheory.HahnSeries.Summable

HahnSeries.SummableFamilystructureMathlib.RingTheory.HahnSeries.Summable, type

Wording

summable family of R and x3 (from the name)

English

Let $x$, $R$ and $x_{3}$ be sets. Then the summable families of $R$ and $x_{3}$ are a basic type.

HahnSeries.SummableFamily.EquivdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the equivalence of e and s (from the name)

English

Let $e$ be an equivalence from $x_{1}$ to $x_{2}$. Let $s$ be a summable family of $R$ and $x_{1}$. Then the equivalence of $e$ and $s$ is a summable family of $R$ and $x_{2}$.

HahnSeries.SummableFamily.coeffdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the coefficient function of s and g (from the docstring)

English

Let $s$ be a summable family of $R$ and $x_{1}$. Let $g$ be an element of $x$. Then the coefficient function of $s$ and $g$ is an element of $\FinsuppMACRoQ {x_{1}}{R}$.

HahnSeries.SummableFamily.constdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the constant of x3 and x4 (from the name)

English

Let $x_{3}$ be a set. Let $x_{4}$ be a Hahn series of $x$ and $R$. Then the constant of $x_{3}$ and $x_{4}$ is a summable family of $R$ and $x_{3}$.

HahnSeries.SummableFamily.embDomaindefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the embedding domain of s and f (from the name)

English

Let $s$ be a summable family of $R$ and $x_{1}$. Let $f$ be an embedding of $x_{1}$ and $x_{2}$. Then the embedding domain of $s$ and $f$ is a summable family of $R$ and $x_{2}$.

HahnSeries.SummableFamily.hsumdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

no wording

English

Let $s$ be a summable family of $R$ and $x_{1}$. Then $\operatorname{hsum}$ applied to $s$ is a Hahn series of $x$ and $R$.

HahnSeries.SummableFamily.lsumdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

no wording

English

$\operatorname{lsum}$ is a linear map of the set of summable families of $R$ and $x_{1}$ and the set of Hahn series of $x$ and $R$.

HahnSeries.SummableFamily.muldefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a summable family of $R$ and $x_{1}$. Let $t$ be a summable family of $R$ and $x_{2}$. Then the product of $s$ and $t$ is a summable family of $R$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

HahnSeries.SummableFamily.ofFinsuppdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the summable family of f (from the name)

English

Let $f$ be a finitely supported function from $x_{1}$ to the set of Hahn series of $x$ and $R$. Then the summable family of $f$ is a summable family of $R$ and $x_{1}$.

HahnSeries.SummableFamily.powersdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the power of x4 (from the name)

English

Let $x_{4}$ be a Hahn series of $x$ and $R$. Then the power of $x_{4}$ is a summable family of $R$ and $\Natural$.

HahnSeries.SummableFamily.singledefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

no wording

English

Let $i$ be an element of $x_{3}$. Let $x_{5}$ be a Hahn series of $x$ and $R$. Then $\operatorname{single}$ applied to $i$ and $x_{5}$ is a summable family of $R$ and $x_{3}$.

HahnSeries.SummableFamily.smuldefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the scalar multiple of s and t (from the name)

English

Let $s$ be a summable family of $R$ and $x_{2}$. Let $t$ be a summable family of $V$ and $x_{3}$. Then the scalar multiple of $s$ and $t$ is a summable family of $V$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

HahnSeries.SummableFamily.smulFamilydefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the scalar multiple family of f and s (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $R$. Let $s$ be a summable family of $V$ and $x_{1}$. Then the scalar multiple family of $f$ and $s$ is a summable family of $V$ and $x_{1}$.

HahnSeries.SummableFamily.toFundefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the summable family of self and x4 (from the name)

English

Let $\mathrm{self}$ be a summable family of $R$ and $x_{3}$. Let $x_{4}$ be an element of $x_{3}$. Then the summable family of $\mathrm{self}$ and $x_{4}$ is a Hahn series of $x$ and $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

HahnSeries.toOrderTopSubOnePosdefMathlib.RingTheory.HahnSeries.Summable, function or constant

Wording

the order top difference one positive part of h1 (from the name)

English

Assume that $0 < \operatorname{orderTop} (x_{4} - 1)$. Then the order top difference one positive part of $h_{1}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{orderTopSubOnePos} (x , R)}{x_{5}})}$.

Mathlib.RingTheory.HahnSeries.Valuation

HahnSeries.addValdefMathlib.RingTheory.HahnSeries.Valuation, function or constant

Wording

the additive value of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the additive value of $x$ and $R$ is an additive valuation of the set of Hahn series of $x$ and $R$ and $\mathrm{WithTop}$ applied to $x$.

Mathlib.RingTheory.Henselian

HenselianLocalRingclassMathlib.RingTheory.Henselian, predicate

Wording

no wording

English

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

HenselianRingclassMathlib.RingTheory.Henselian, predicate

Wording

no wording

English

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

Mathlib.RingTheory.HopfAlgebra.Basic

HopfAlgebraclassMathlib.RingTheory.HopfAlgebra.Basic, predicate

Wording

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

English

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

HopfAlgebraStructclassMathlib.RingTheory.HopfAlgebra.Basic, predicate

Wording

no wording

English

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

HopfAlgebraStruct.antipodedefMathlib.RingTheory.HopfAlgebra.Basic, function or constant

Wording

the antipode of the Hopf algebra of R (from the docstring)

English

Let $R$ be a set. Then the antipode of the Hopf algebra of $R$ is a linear map of $A$ and $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.RingTheory.HopfAlgebra.Convolution

HopfAlgebra.antipodeAlgHomdefMathlib.RingTheory.HopfAlgebra.Convolution, function or constant

Wording

the antipode of R and A (from the docstring)

English

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

HopfAlgebra.antipodeAlgHomOpdefMathlib.RingTheory.HopfAlgebra.Convolution, function or constant

Wording

the antipode of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the antipode of $R$ and $A$ is an algebra homomorphism of $A$ and the set of multiplicative opposites of $A$.

Mathlib.RingTheory.HopfAlgebra.GroupLike

GroupLike.toUnitsdefMathlib.RingTheory.HopfAlgebra.GroupLike, function or constant

Wording

the unit of R (from the name)

English

Let $R$ be a set. Then the unit of $R$ is a monoid homomorphism of $\mathrm{GroupLike}$ applied to $R$ and $A$ and $\UnitsMACRoAO {A}$.

Mathlib.RingTheory.HopfAlgebra.Quotient

Ideal.IsHopfIdealclassMathlib.RingTheory.HopfAlgebra.Quotient, predicate

Wording

I is a Hopf ideal (from the name)

English

Let $R$ be a set. Let $I$ be an ideal of $A$. Then we can say that $I$ is a Hopf ideal.

Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

IsAssociatedPrimedefMathlib.RingTheory.Ideal.AssociatedPrime.Basic, predicate

Wording

no wording

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Then $\mathrm{IsAssociatedPrime}$ holds for $I$ and $M$, if $\operatorname{IsAssociatedPrime}$ holds for the bottom and $I$.

Submodule.IsAssociatedPrimestructureMathlib.RingTheory.Ideal.AssociatedPrime.Basic, predicate

Wording

no wording

English

Let $N$ be a submodule of $R$ and $M$. Let $I$ be an ideal of $R$. Then we can say that $\operatorname{IsAssociatedPrime}$ holds for $N$ and $I$.

Submodule.associatedPrimesdefMathlib.RingTheory.Ideal.AssociatedPrime.Basic, function or constant

Wording

no wording

English

Let $N$ be a submodule of $R$ and $M$. Then $\operatorname{associatedPrimes}$ applied to $N$ is an element of the power set of the set of ideals of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $I$ to $\operatorname{IsAssociatedPrime}$ applied to $N$ and $I$.

associatedPrimesdefMathlib.RingTheory.Ideal.AssociatedPrime.Basic, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\mathrm{associatedPrimes}$ applied to $R$ and $M$ is an element of the power set of the set of ideals of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $I$ to $\mathrm{IsAssociatedPrime}$ applied to $I$ and $M$.

Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Submodule.IsQuotientEquivQuotientPrimedefMathlib.RingTheory.Ideal.AssociatedPrime.Finiteness, predicate

Wording

no wording

English

Let $x_{3}$ and $x_{4}$ be submodules of $A$ and $M$. Then $\operatorname{IsQuotientEquivQuotientPrime}$ holds for $x_{3}$ and $x_{4}$, if $x_{3} \leq x_{4}$ and there exists a prime spectrum $p$ of $A$ such that $\mathrm{Nonempty}$ holds for the set of linear equivalences of the set of quotients of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {x_{4}}{x_{5}})}$ and the submodule of $x_{3}$ and $x_{4}$ and the set of quotients of $A$ and $\operatorname{asIdeal}$ applied to $p$.

Mathlib.RingTheory.Ideal.Basic

Ideal.equivFinTwodefMathlib.RingTheory.Ideal.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{equivFinTwo}$ applied to $K$ is an equivalence from the set of ideals of $K$ to $\mathrm{Fin}$ applied to $2$.

Ideal.pidefMathlib.RingTheory.Ideal.Basic, function or constant

Wording

the product of I (from the name)

English

Let $I$ be a function from elements $i_{1}$ of $x$ to ideals of $R$ applied to $i_{1}$. Then the product of $i_{1}$ is an ideal of the set of functions from elements $i$ of $x$ to elements of $R$ applied to $i$.

Mathlib.RingTheory.Ideal.Basis

Ideal.basisSpanSingletondefMathlib.RingTheory.Ideal.Basis, function or constant

Wording

the basis span singleton of b and hx (from the name)

English

Let $b$ be a basis of $R$ and $S$. Assume that $x_{4} \neq 0$. Then the basis span singleton of $b$ and $\mathrm{hx}$ is a basis of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{span} (\operatorname{singleton} (x_{4}))}{x_{5}})}$.

Mathlib.RingTheory.Ideal.Colon

Submodule.colondefMathlib.RingTheory.Ideal.Colon, function or constant

Wording

the colon of N and S (from the name)

English

Let $N$ be a submodule of $R$ and $M$. Let $S$ be an element of $\wp M$. Then the colon of $N$ and $S$ is an ideal of $R$.

Mathlib.RingTheory.Ideal.Cotangent

AlgHom.kerSquareLiftdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the lift of f (from the docstring)

English

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

Ideal.CotangentdefMathlib.RingTheory.Ideal.Cotangent, type

Wording

no wording

English

Let $I$ be an ideal of $R$. Then an element of $\operatorname{Cotangent}$ applied to $I$ is an element of the function that maps $I$ to the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$.

Ideal.Cotangent.equivOfEqdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the equivalence of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$ such that $\EqtMACRoH {I}{J}$. Then the equivalence of $I$ and $J$ is a linear equivalence of $\operatorname{Cotangent}$ applied to $I$ and $\operatorname{Cotangent}$ applied to $J$.

Ideal.Cotangent.liftdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the lift of f and hf (from the name)

English

Let $f$ be a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {I}{x_{8}})}$ and $M$ such that for all elements $x_{5}$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {I}{x_{7}})}$, for all elements $y$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {I}{x_{6}})}$, $\EqtMACRoH {f (x_{5} \times y)}{0}$. Then the lift of $f$ and $\mathrm{hf}$ is a linear map of $\operatorname{Cotangent}$ applied to $I$ and $M$.

Ideal.cotangentEquivIdealdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the cotangent equivalence ideal of I (from the name)

English

Let $I$ be an ideal of $R$. Then the cotangent equivalence ideal of $I$ is a linear equivalence of $\operatorname{Cotangent}$ applied to $I$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{cotangentIdeal} (I)}{x_{1}})}$.

Ideal.cotangentIdealdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the cotangent ideal of I (from the name)

English

Let $I$ be an ideal of $R$. Then the cotangent ideal of $I$ is an ideal of the set of quotients of $R$ and $I ^ {2}$ defined as the map of the semilinear map of $\operatorname{mk}$ applied to $I ^ {2}$ and $I$.

Ideal.cotangentToQuotientSquaredefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Then $\operatorname{cotangentToQuotientSquare}$ applied to $I$ is a linear map of $\operatorname{Cotangent}$ applied to $I$ and the set of quotients of $R$ and $I ^ {2}$.

Ideal.mapCotangentdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

no wording

English

Let $x_{5}$ be an ideal of $A$. Let $x_{6}$ be an ideal of $B$. Let $f$ be an algebra homomorphism of $A$ and $B$ such that $x_{5}$ is less than or equal to the preimage of $x_{6}$ under $f$. Then $\operatorname{mapCotangent}$ applied to $x_{5}$, $x_{6}$, $f$ and $h$ is a linear map of $\operatorname{Cotangent}$ applied to $x_{5}$ and $\operatorname{Cotangent}$ applied to $x_{6}$.

Ideal.quotCotangentdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the quotient ring of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the quotient ring of $I$ is a ring isomorphism of the set of quotients of the set of quotients of $R$ and $I ^ {2}$ and the cotangent ideal of $I$ and the set of quotients of $R$ and $I$.

Ideal.toCotangentdefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Then $\operatorname{toCotangent}$ applied to $I$ is a linear map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ and $\operatorname{Cotangent}$ applied to $I$ defined as $\operatorname{mkQ}$ applied to $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$.

IsLocalRing.CotangentSpacedefMathlib.RingTheory.Ideal.Cotangent, type

Wording

cotangent space of R (from the name)

English

Let $R$ be a set. Then a cotangent space of $R$ is an element of the function that maps $R$ to $\operatorname{Cotangent}$ applied to the maximal ideal of $R$.

IsLocalRing.toCotangentSpacedefMathlib.RingTheory.Ideal.Cotangent, function or constant

Wording

the cotangent space of R (from the name)

English

Let $R$ be a set. Then the cotangent space of $R$ is a linear map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{maximalIdeal} (R)}{x_{1}})}$ and the set of cotangent spaces of $R$.

Mathlib.RingTheory.Ideal.CotangentBaseChange

Ideal.tensorCotangentEquivdefMathlib.RingTheory.Ideal.CotangentBaseChange, function or constant

Wording

the tensor cotangent equivalence of I (from the name)

English

Let $R$ and $T$ be sets. Let $I$ be an ideal of $S$. Then the tensor cotangent equivalence of $I$ is a linear equivalence of the set of tensor products of $T$ and $\operatorname{Cotangent}$ applied to $I$ and $\operatorname{Cotangent}$ applied to the map of $\operatorname{toRingHom}$ applied to $\operatorname{includeRight}$ and $I$.

Ideal.tensorCotangentHomdefMathlib.RingTheory.Ideal.CotangentBaseChange, function or constant

Wording

the tensor cotangent homomorphism of I (from the name)

English

Let $R$ and $T$ be sets. Let $I$ be an ideal of $S$. Then the tensor cotangent homomorphism of $I$ is a linear map of the set of tensor products of $T$ and $\operatorname{Cotangent}$ applied to $I$ and $\operatorname{Cotangent}$ applied to the map of $\operatorname{toRingHom}$ applied to $\operatorname{includeRight}$ and $I$.

Mathlib.RingTheory.Ideal.Defs

IdealdefMathlib.RingTheory.Ideal.Defs, type

Wording

ideal of R (from the name)

English

Let $R$ be a set. Then an ideal of $R$ is an element of the function that maps $R$ to the set of submodules of $R$ and $R$.

Ideal.IsTwoSidedclassMathlib.RingTheory.Ideal.Defs, predicate

Wording

no wording

English

Let $I$ be an ideal of $x$. Then we can say that $\operatorname{IsTwoSided}$ holds for $I$.

Ideal.inertiadefMathlib.RingTheory.Ideal.Defs, function or constant

Wording

the inertia of G and I (from the name)

English

Let $G$ be a set. Let $I$ be an ideal of $x$. Then the inertia of $G$ and $I$ is a subgroup of $G$ defined as the inertia of the additive subgroup of $I$ and $G$.

Module.eqIdealdefMathlib.RingTheory.Ideal.Defs, function or constant

Wording

no wording

English

Let $R$ be a set. Let $m$ and $\mathrm{m'}$ be elements of $M$. Then $\operatorname{eqIdeal}$ applied to $R$, $m$ and $\mathrm{m'}$ is an ideal of $R$.

Mathlib.RingTheory.Ideal.GoingDown

Algebra.HasGoingDownclassMathlib.RingTheory.Ideal.GoingDown, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Ideal.HasGoingUp

Algebra.HasGoingUpclassMathlib.RingTheory.Ideal.HasGoingUp, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Ideal.Height

Ideal.FiniteHeightclassMathlib.RingTheory.Ideal.Height, predicate

Wording

I is a finite height (from the name)

English

Let $I$ be an ideal of $R$. Then we can say that $I$ is a finite height.

Ideal.heightdefMathlib.RingTheory.Ideal.Height, function or constant

Wording

the height of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the height of $I$ is a natural number.

Mathlib.RingTheory.Ideal.IsAugmentation

Ideal.IsAugmentationdefMathlib.RingTheory.Ideal.IsAugmentation, predicate

Wording

I is a augmentation (from the name)

English

Let $R$ be a set. Let $I$ be an ideal of $A$. Then $I$ is an augmentation, if $\mathrm{IsCompl}$ holds for $1$ and $\operatorname{restrictScalars}$ applied to $R$ and $I$.

Mathlib.RingTheory.Ideal.IsPrimary

Ideal.IsPrimarydefMathlib.RingTheory.Ideal.IsPrimary, predicate

Wording

I is primary (from the name)

English

Let $I$ be an ideal of $R$. Then $I$ is primary, if $I$ is primary.

Mathlib.RingTheory.Ideal.IsPrincipal

Ideal.associatesEquivIsPrincipaldefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{associatesEquivIsPrincipal}$ applied to $R$ is an element of $\EquivMACRoAE {\mathrm{Associates} (R)}{(\SubtypeSet {I}{\operatorname{IsPrincipal} (I)})}$.

Ideal.associatesMulEquivIsPrincipaldefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{associatesMulEquivIsPrincipal}$ applied to $R$ is a multiplicative equivalence of the set of associates of $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{isPrincipalSubmonoid} (R)}{x_{1}})}$.

Ideal.associatesNonZeroDivisorsEquivIsPrincipaldefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{associatesNonZeroDivisorsEquivIsPrincipal}$ applied to $R$ is an element of $\EquivMACRoAE {\mathrm{Associates} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (R)}{x_{1}})})}{(\SubtypeSet {I}{\operatorname{IsPrincipal} (I)})}$.

Ideal.associatesNonZeroDivisorsMulEquivIsPrincipaldefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{associatesNonZeroDivisorsMulEquivIsPrincipal}$ applied to $R$ is a multiplicative equivalence of the set of associates of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (R)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{isPrincipalNonZeroDivisorsSubmonoid} (R)}{x_{2}})}$.

Ideal.isPrincipalNonZeroDivisorsSubmonoiddefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{isPrincipalNonZeroDivisorsSubmonoid}$ applied to $R$ is a submonoid of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Ideal} (R))}{x_{1}})}$.

Ideal.isPrincipalSubmonoiddefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{isPrincipalSubmonoid}$ applied to $R$ is a submonoid of the set of ideals of $R$.

Ideal.isoBaseOfIsPrincipaldefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

the isomorphism base of hI (from the name)

English

Assume that $I$ is distinct from the bottom. Then the isomorphism base of $\mathrm{hI}$ is a linear equivalence of $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$.

Ideal.spanSubmonoiddefMathlib.RingTheory.Ideal.IsPrincipal, function or constant

Wording

the span submonoid of S (from the name)

English

Let $S$ be a submonoid of $R$. Then the span submonoid of $S$ is a submonoid of the set of ideals of $R$.

Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Ideal.quotEquivPowQuotPowSuccdefMathlib.RingTheory.Ideal.IsPrincipalPowQuotient, function or constant

Wording

the quotient equivalence power quotient power successor of #3 (from the name)

English

Assume that $I$ is principal. Assume that $I \neq \operatorname{bot}$. Let $n$ be an element of $\Natural$. Then the quotient equivalence power quotient power successor of $n$ is a linear equivalence of the set of quotients of $R$ and $I$ and the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {(I ^ {n})}{x_{1}})}$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$.

Ideal.quotEquivPowQuotPowSuccEquivdefMathlib.RingTheory.Ideal.IsPrincipalPowQuotient, function or constant

Wording

the quotient equivalence power quotient power successor equivalence of #3 (from the name)

English

Assume that $I$ is principal. Assume that $I \neq \operatorname{bot}$. Let $n$ be an element of $\Natural$. Then the quotient equivalence power quotient power successor equivalence of $n$ is an element of $\EquivMACRoAE {\operatorname{Quotient} (R , I)}{\operatorname{Quotient} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {(I ^ {n})}{x_{1}})}, \HSMulhSMulMACRoAL {I}{\operatorname{top}})}$ defined as the equivalence of the quotient equivalence power quotient power successor of $n$.

Mathlib.RingTheory.Ideal.Maps

Algebra.idealMapdefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the ideal map of S and I (from the name)

English

Let $S$ be a set. Let $I$ be an ideal of $R$. Then the ideal map of $S$ and $I$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {I}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{algebraMap} (R , S), I)}{x_{4}})}$.

Ideal.comapdefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the preimage of I under f (from the docstring)

English

Let $f$ be an element of $F$. Let $I$ be an ideal of $S$. Then the preimage of $I$ under $f$ is an ideal of $R$.

Ideal.giMapComapdefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

no wording

English

Let $f$ be an element of $F$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then $\operatorname{giMapComap}$ applied to $f$ and $\mathrm{hf}$ is a Galois insertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

Ideal.mapdefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the map of f and I (from the name)

English

Let $f$ be an element of $F$. Let $I$ be an ideal of $R$. Then the map of $f$ and $I$ is an ideal of $S$ defined as the span of the image of $\operatorname{coe}$ applied to $f$ and $I$.

Ideal.mapHomdefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the map homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the map homomorphism of $f$ is a ring homomorphism of the set of ideals of $R$ and the set of ideals of $S$.

Ideal.orderEmbeddingOfSurjectivedefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the order embedding of f and hf (from the name)

English

Let $f$ be an element of $F$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the order embedding of $f$ and $\mathrm{hf}$ is an order embedding of the set of ideals of $S$ and the set of ideals of $R$.

Ideal.piOrderIsodefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the product order isomorphism (from the name)

English

The product order isomorphism is an order isomorphism of the set of ideals of the set of functions from elements $i$ of $x$ to elements of $R$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to ideals of $R$ applied to $i_{1}$.

Ideal.relIsoOfBijectivedefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the relation isomorphism of f and hf (from the name)

English

Let $f$ be an element of $F$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the relation isomorphism of $f$ and $\mathrm{hf}$ is an order isomorphism of the set of ideals of $S$ and the set of ideals of $R$.

Ideal.relIsoOfSurjectivedefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the relation isomorphism of f and hf (from the name)

English

Let $f$ be an element of $F$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the relation isomorphism of $f$ and $\mathrm{hf}$ is an order isomorphism of the set of ideals of $S$ and $\SubtypeSet {p}{\mathrm{Leq} (\operatorname{comap} (\operatorname{bot} , f), p)}$.

Module.annihilatordefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the annihilator of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the annihilator of $R$ and $M$ is an ideal of $R$ defined as the kernel of the additive monoid end of $R$ and $M$.

RingEquiv.idealComapOrderIsodefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the ideal preimage order isomorphism of e (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then the ideal preimage order isomorphism of $e$ is an order isomorphism of the set of ideals of $S$ and the set of ideals of $R$.

RingHom.kerdefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the kernel of f (from the name)

English

Let $f$ be an element of $F$. Then the kernel of $f$ is an ideal of $R$ defined as the preimage of the bottom under $f$.

RingHom.liftOfRightInversedefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the lift of f and f_inv (from the name)

English

Let $f$ be a ring homomorphism of $A$ and $B$. Let $\mathrm{f\_inv}$ be a function from elements of $B$ to elements of $A$ such that $\operatorname{RightInverse}$ holds for $\mathrm{f\_inv}$ and $\operatorname{coe}$ applied to $f$. Then the lift of $f$ and $\mathrm{f\_inv}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{RingHom} (B , C)}$.

RingHom.liftOfSurjectivedefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the lift of f and hf (from the name)

English

Let $f$ be a ring homomorphism of $A$ and $B$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the lift of $f$ and $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{RingHom} (B , C)}$.

Submodule.annihilatordefMathlib.RingTheory.Ideal.Maps, function or constant

Wording

the annihilator of N (from the name)

English

Let $N$ be a submodule of $R$ and $M$. Then the annihilator of $N$ is an ideal of $R$ defined as the annihilator of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {N}{x_{3}})}$.

Mathlib.RingTheory.Ideal.Maximal

Ideal.IsMaximalclassMathlib.RingTheory.Ideal.Maximal, predicate

Wording

I is maximal (from the docstring)

English

Let $I$ be an ideal of $x$. Then we can say that $I$ is maximal.

Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Ideal.IsMinimalPrimedefMathlib.RingTheory.Ideal.MinimalPrime.Basic, predicate

Wording

p is a minimal prime with respect to I (from the name)

English

Let $I$ and $p$ be ideals of $R$. Then $p$ is a minimal prime with respect to $I$, if $p$ is minimal with respect to the function that maps $q$ to the proposition that $q$ is prime and $I \leq q$.

Ideal.minimalPrimesdefMathlib.RingTheory.Ideal.MinimalPrime.Basic, function or constant

Wording

the minimal prime of I (from the name)

English

Let $I$ be an ideal of $R$. Then the minimal prime of $I$ is an element of the power set of the set of ideals of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that $p$ is a minimal prime with respect to $I$.

IsMinimalPrimedefMathlib.RingTheory.Ideal.MinimalPrime.Basic, predicate

Wording

p is a minimal prime (from the name)

English

Let $p$ be an ideal of $R$. Then $p$ is a minimal prime, if $p$ is a minimal prime with respect to the bottom.

minimalPrimesdefMathlib.RingTheory.Ideal.MinimalPrime.Basic, function or constant

Wording

the minimal prime of R (from the name)

English

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

Mathlib.RingTheory.Ideal.Nonunits

nonunitsdefMathlib.RingTheory.Ideal.Nonunits, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\mathrm{nonunits}$ applied to $x$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is not a unit.

Mathlib.RingTheory.Ideal.Norm.AbsNorm

Ideal.absNormdefMathlib.RingTheory.Ideal.Norm.AbsNorm, function or constant

Wording

the absolute norm of the ideal (from the docstring)

English

The absolute norm of the ideal is a monoid with zero homomorphism of the set of ideals of $S$ and $\Natural$.

Submodule.cardQuotdefMathlib.RingTheory.Ideal.Norm.AbsNorm, function or constant

Wording

the cardinality of S (from the docstring)

English

Let $S$ be a submodule of $R$ and $M$. Then the cardinality of $S$ is a natural number defined as the index of the additive subgroup of $S$.

Mathlib.RingTheory.Ideal.Norm.RelNorm

Ideal.relNormdefMathlib.RingTheory.Ideal.Norm.RelNorm, function or constant

Wording

the relative norm of R (from the docstring)

English

Let $R$ be a set. Then the relative norm of $R$ is a monoid with zero homomorphism of the set of ideals of $S$ and the set of ideals of $R$.

Ideal.spanNormdefMathlib.RingTheory.Ideal.Norm.RelNorm, function or constant

Wording

the span norm of R and I (from the name)

English

Let $R$ be a set. Let $I$ be an ideal of $S$. Then the span norm of $R$ and $I$ is an ideal of $R$ defined as the map of the norm of $R$ and $S$ and $I$.

Mathlib.RingTheory.Ideal.Oka

Ideal.IsOkastructureMathlib.RingTheory.Ideal.Oka, predicate

Wording

no wording

English

Let $P$ be a function from ideals of $R$ to propositions. Then we can say that $\operatorname{IsOka}$ holds for $P$.

Mathlib.RingTheory.Ideal.Operations

Ideal.IsRadicaldefMathlib.RingTheory.Ideal.Operations, predicate

Wording

I is a radical (from the name)

English

Let $I$ be an ideal of $R$. Then $I$ is a radical, if the radical of $I$ is less than or equal to $I$.

Ideal.finsuppTotaldefMathlib.RingTheory.Ideal.Operations, function or constant

Wording

no wording

English

Let $x$ and $M$ be sets. Let $I$ be an ideal of $R$. Let $v$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{finsuppTotal}$ applied to $x$, $M$, $I$ and $v$ is a linear map of $\FinsuppMACRoQ {x}{(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {I}{x_{4}})})}$ and $M$ defined as the composition of the linear combination of $R$ and $v$ and the linear map of the subtype of $I$.

Ideal.radicaldefMathlib.RingTheory.Ideal.Operations, function or constant

Wording

the radical of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the radical of $I$ is an ideal of $R$.

Ideal.radicalInfTopHomdefMathlib.RingTheory.Ideal.Operations, function or constant

Wording

the radical infimum top homomorphism (from the name)

English

The radical infimum top homomorphism is an infimum top homomorphism of the set of ideals of $R$ and the set of ideals of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{radical}$ and $\mathrm{Ideal\_\_radical\_inf}$ and $\mathrm{Ideal\_\_radical\_top}$ applied to $R$.

Submodule.mapAlgEquivdefMathlib.RingTheory.Ideal.Operations, function or constant

Wording

the map algebra isomorphism of f (from the name)

English

Let $f$ be an algebra isomorphism of $A$ and $B$. Then the map algebra isomorphism of $f$ is an algebra isomorphism of the set of submodules of $R$ and $A$ and the set of submodules of $R$ and $B$.

Submodule.mapAlgHomdefMathlib.RingTheory.Ideal.Operations, function or constant

Wording

the map algebra homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the map algebra homomorphism of $f$ is an algebra homomorphism of the set of submodules of $R$ and $A$ and the set of submodules of $R$ and $B$.

Mathlib.RingTheory.Ideal.Over

Ideal.LiesOverclassMathlib.RingTheory.Ideal.Over, predicate

Wording

no wording

English

Let $P$ be an ideal of $B$. Let $p$ be an ideal of $A$. Then we can say that $\operatorname{LiesOver}$ holds for $P$ and $p$.

Ideal.Quotient.algEquivOfEqComapdefMathlib.RingTheory.Ideal.Over, function or constant

Wording

the algebra isomorphism of p and x6 (from the name)

English

Let $p$ be an ideal of $A$. Let $x_{6}$ be an element of $E$ such that $P$ is equal to the preimage of $Q$ under $x_{6}$. Then the algebra isomorphism of $p$ and $x_{6}$ is an algebra isomorphism of the set of quotients of $B$ and $P$ and the set of quotients of $C$ and $Q$.

Ideal.Quotient.algEquivOfEqMapdefMathlib.RingTheory.Ideal.Over, function or constant

Wording

the algebra isomorphism of p and x6 (from the name)

English

Let $p$ be an ideal of $A$. Let $x_{6}$ be an element of $E$ such that $Q$ is equal to the map of $x_{6}$ and $P$. Then the algebra isomorphism of $p$ and $x_{6}$ is an algebra isomorphism of the set of quotients of $B$ and $P$ and the set of quotients of $C$ and $Q$.

Ideal.Quotient.stabilizerHomdefMathlib.RingTheory.Ideal.Over, function or constant

Wording

the stabilizer homomorphism of P and p (from the name)

English

Let $P$ be an ideal of $B$. Let $p$ be an ideal of $A$. Let $G$ be a set. Then the stabilizer homomorphism of $P$ and $p$ is a monoid homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , P)}{x_{5}})}$ and the set of algebra isomorphisms of the set of quotients of $B$ and $P$ and the set of quotients of $B$ and $P$.

Ideal.primesOverdefMathlib.RingTheory.Ideal.Over, function or constant

Wording

no wording

English

Let $p$ be an ideal of $A$. Let $B$ be a set. Then $\operatorname{primesOver}$ applied to $p$ and $B$ is an element of the power set of the set of ideals of $B$ defined as $\operatorname{ofPred}$ applied to the function that maps $P$ to the proposition that $P$ is prime and $\operatorname{LiesOver}$ holds for $P$ and $p$.

Ideal.primesOver.mkdefMathlib.RingTheory.Ideal.Over, function or constant

Wording

no wording

English

Let $p$ be an ideal of $A$. Let $P$ be an ideal of $B$. Then $\operatorname{mk}$ applied to $p$ and $P$ is an element of $\operatorname{primesOver}$ applied to $p$ and $B$ defined as $P$.

Ideal.underdefMathlib.RingTheory.Ideal.Over, function or constant

Wording

no wording

English

Let $A$ be a set. Let $P$ be an ideal of $B$. Then $\operatorname{under}$ applied to $A$ and $P$ is an ideal of $A$ defined as the preimage of $P$ under the algebra map of $A$ and $B$.

Mathlib.RingTheory.Ideal.Pointwise

Ideal.inertiaEquivdefMathlib.RingTheory.Ideal.Pointwise, function or constant

Wording

the inertia equivalence of I and e (from the name)

English

Let $I$ be an ideal of $R$. Let $e$ be a multiplicative equivalence of $M$ and $N$ such that for all elements $m$ of $M$, for all elements $x_{7}$ of $R$, $\EqtMACRoH {\HSMulhSMulMACRoAL {e (m)}{x_{7}}}{\HSMulhSMulMACRoAL {m}{x_{7}}}$. Then the inertia equivalence of $I$ and $e$ is a multiplicative equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{inertia} (M , I)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{inertia} (N , I)}{x_{6}})}$.

Ideal.stabilizerEquivdefMathlib.RingTheory.Ideal.Pointwise, function or constant

Wording

the stabilizer equivalence of I and e (from the name)

English

Let $I$ be an ideal of $R$. Let $e$ be a multiplicative equivalence of $M$ and $N$ such that for all elements $m$ of $M$, for all elements $x_{7}$ of $R$, $\EqtMACRoH {\HSMulhSMulMACRoAL {e (m)}{x_{7}}}{\HSMulhSMulMACRoAL {m}{x_{7}}}$. Then the stabilizer equivalence of $I$ and $e$ is a multiplicative equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (M , I)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (N , I)}{x_{6}})}$.

Mathlib.RingTheory.Ideal.Prime

Ideal.IsPrimeclassMathlib.RingTheory.Ideal.Prime, predicate

Wording

I is prime (from the name)

English

Let $I$ be an ideal of $x$. Then we can say that $I$ is prime.

Ideal.primeCompldefMathlib.RingTheory.Ideal.Prime, function or constant

Wording

the complement of P (from the docstring)

English

Let $P$ be an ideal of $x$. Then the complement of $P$ is a submonoid of $x$.

Mathlib.RingTheory.Ideal.Prod

Ideal.idealProdEquivdefMathlib.RingTheory.Ideal.Prod, function or constant

Wording

the ideal product equivalence (from the name)

English

The ideal product equivalence is an order isomorphism of the set of ideals of $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Prod}$ applied to the set of ideals of $R$ and the set of ideals of $S$.

Ideal.proddefMathlib.RingTheory.Ideal.Prod, function or constant

Wording

the product of I and J (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $S$. Then the product of $I$ and $J$ is an ideal of $\mathrm{Prod}$ applied to $R$ and $S$ defined as the minimum of the preimage of $I$ under the first component of $R$ and $S$ and the preimage of $J$ under the second component of $R$ and $S$.

Mathlib.RingTheory.Ideal.Pure

Ideal.PuredefMathlib.RingTheory.Ideal.Pure, predicate

Wording

I is pure (from the name)

English

Let $I$ be an ideal of $R$. Then $I$ is pure, if the set of quotients of $R$ and $I$ is flat with respect to $R$.

Mathlib.RingTheory.Ideal.Quotient.Basic

Ideal.piQuotEquivdefMathlib.RingTheory.Ideal.Quotient.Basic, function or constant

Wording

the product quotient equivalence of x and I (from the name)

English

Let $x$ be a set. Let $I$ be an ideal of $R$. Then the product quotient equivalence of $x$ and $I$ is a linear equivalence of the set of quotients of the set of functions from elements of $x$ to elements of $R$ and the product of the function that maps $x_{3}$ to $I$ and the set of functions from elements of $x$ to quotients of $R$ and $I$.

Mathlib.RingTheory.Ideal.Quotient.Defs

Ideal.Quotient.factordefMathlib.RingTheory.Ideal.Quotient.Defs, function or constant

Wording

the factor of H (from the name)

English

Assume that $S \leq T$. Then the factor of $H$ is a ring homomorphism of the set of quotients of $R$ and $S$ and the set of quotients of $R$ and $T$.

Ideal.Quotient.liftdefMathlib.RingTheory.Ideal.Quotient.Defs, 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 ring homomorphism of $R$ and $S$ such that for all elements $a$ of $R$, if $a$ is an element of $I$, then $\EqtMACRoH {f (a)}{0}$. Then the lift of $I$ and $f$ is a ring homomorphism of the set of quotients of $R$ and $I$ and $S$.

Ideal.Quotient.mkdefMathlib.RingTheory.Ideal.Quotient.Defs, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Then $\operatorname{mk}$ applied to $I$ is a ring homomorphism of $R$ and the set of quotients of $R$ and $I$.

Ideal.Quotient.ringCondefMathlib.RingTheory.Ideal.Quotient.Defs, function or constant

Wording

the ring congruence relation of I (from the name)

English

Let $I$ be an ideal of $R$. Then the ring congruence relation of $I$ is a ring congruence relation of $R$.

Ideal.quotEquivOfEqdefMathlib.RingTheory.Ideal.Quotient.Defs, function or constant

Wording

the quotient equivalence of h2 (from the name)

English

Assume that $\EqtMACRoH {I}{J}$. Then the quotient equivalence of $h_{2}$ is a ring isomorphism of the set of quotients of $R$ and $I$ and the set of quotients of $R$ and $J$.

Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients.Basic

Ring.HasFiniteQuotientsclassMathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients.Basic, predicate

Wording

R has finite quotients (from the name)

English

Let $R$ be a set. Then we can say that $R$ has finite quotients.

Mathlib.RingTheory.Ideal.Quotient.Operations

AlgEquiv.quotientBotdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient bottom of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the quotient bottom of $R$ and $S$ is an algebra isomorphism of the set of quotients of $S$ and the bottom and $S$.

AlgHom.liftOfSurjectivedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the lift of f and g (from the name)

English

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

DoubleQuot.liftSupQuotQuotMkdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the lift supremum quotient quotient of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$. Then the lift supremum quotient quotient of $I$ and $J$ is a ring homomorphism of the set of quotients of $R$ and $\MaxmaxMACRoAF {I}{J}$ and the set of quotients of the set of quotients of $R$ and $I$ and the map of $\operatorname{mk}$ applied to $I$ and $J$.

DoubleQuot.liftSupQuotQuotMkₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the lift supremum quotient quotient of I and J (from the name)

English

Let $R$ be a set. Let $I$ and $J$ be ideals of $A$. Then the lift supremum quotient quotient of $I$ and $J$ is an algebra homomorphism of the set of quotients of $A$ and $\MaxmaxMACRoAF {I}{J}$ and the set of quotients of the set of quotients of $A$ and $I$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $J$.

DoubleQuot.quotLeftToQuotSupdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient left to quotient supremum of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$. Then the quotient left to quotient supremum of $I$ and $J$ is a ring homomorphism of the set of quotients of $R$ and $I$ and the set of quotients of $R$ and $\MaxmaxMACRoAF {I}{J}$.

DoubleQuot.quotLeftToQuotSupₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient left to quotient supremum of I and J (from the name)

English

Let $R$ be a set. Let $I$ and $J$ be ideals of $A$. Then the quotient left to quotient supremum of $I$ and $J$ is an algebra homomorphism of the set of quotients of $A$ and $I$ and the set of quotients of $A$ and $\MaxmaxMACRoAF {I}{J}$.

DoubleQuot.quotQuotEquivCommdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

no wording

English

Let $I$ and $J$ be ideals of $R$. Then $\operatorname{quotQuotEquivComm}$ applied to $I$ and $J$ is a ring isomorphism of the set of quotients of the set of quotients of $R$ and $I$ and the map of $\operatorname{mk}$ applied to $I$ and $J$ and the set of quotients of the set of quotients of $R$ and $J$ and the map of $\operatorname{mk}$ applied to $J$ and $I$.

DoubleQuot.quotQuotEquivCommₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

no wording

English

Let $R$ be a set. Let $I$ and $J$ be ideals of $A$. Then $\mathrm{DoubleQuot\_\_quotQuotEquivComm\_u2090\_}$ applied to $R$, $I$ and $J$ is an algebra isomorphism of the set of quotients of the set of quotients of $A$ and $I$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $J$ and the set of quotients of the set of quotients of $A$ and $J$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $J$ and $I$.

DoubleQuot.quotQuotEquivQuotOfLEdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

Assume that $I \leq J$. Then the quotient quotient equivalence quotient of $h$ is a ring isomorphism of the set of quotients of the set of quotients of $R$ and $I$ and the map of $\operatorname{mk}$ applied to $I$ and $J$ and the set of quotients of $R$ and $J$.

DoubleQuot.quotQuotEquivQuotOfLEₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

Let $R$ be a set. Assume that $I \leq J$. Then the quotient quotient equivalence quotient of $R$ and $h$ is an algebra isomorphism of the set of quotients of the set of quotients of $A$ and $I$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $J$ and the set of quotients of $A$ and $J$.

DoubleQuot.quotQuotEquivQuotSupdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient quotient equivalence quotient supremum of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$. Then the quotient quotient equivalence quotient supremum of $I$ and $J$ is a ring isomorphism of the set of quotients of the set of quotients of $R$ and $I$ and the map of $\operatorname{mk}$ applied to $I$ and $J$ and the set of quotients of $R$ and $\MaxmaxMACRoAF {I}{J}$.

DoubleQuot.quotQuotEquivQuotSupₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient quotient equivalence quotient supremum of I and J (from the name)

English

Let $R$ be a set. Let $I$ and $J$ be ideals of $A$. Then the quotient quotient equivalence quotient supremum of $I$ and $J$ is an algebra isomorphism of the set of quotients of the set of quotients of $A$ and $I$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $J$ and the set of quotients of $A$ and $\MaxmaxMACRoAF {I}{J}$.

DoubleQuot.quotQuotMkdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient quotient of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$. Then the quotient quotient of $I$ and $J$ is a ring homomorphism of $R$ and the set of quotients of the set of quotients of $R$ and $I$ and the map of $\operatorname{mk}$ applied to $I$ and $J$ defined as the composition of $\operatorname{mk}$ applied to the map of $\operatorname{mk}$ applied to $I$ and $J$ and $\operatorname{mk}$ applied to $I$.

DoubleQuot.quotQuotMkₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient quotient of I and J (from the name)

English

Let $R$ be a set. Let $I$ and $J$ be ideals of $A$. Then the quotient quotient of $I$ and $J$ is an algebra homomorphism of $A$ and the set of quotients of the set of quotients of $A$ and $I$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $J$.

DoubleQuot.quotQuotToQuotSupdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient quotient to quotient supremum of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$. Then the quotient quotient to quotient supremum of $I$ and $J$ is a ring homomorphism of the set of quotients of the set of quotients of $R$ and $I$ and the map of $\operatorname{mk}$ applied to $I$ and $J$ and the set of quotients of $R$ and $\MaxmaxMACRoAF {I}{J}$.

DoubleQuot.quotQuotToQuotSupₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient quotient to quotient supremum of I and J (from the name)

English

Let $R$ be a set. Let $I$ and $J$ be ideals of $A$. Then the quotient quotient to quotient supremum of $I$ and $J$ is an algebra homomorphism of the set of quotients of the set of quotients of $A$ and $I$ and the map of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and $I$ and $J$ and the set of quotients of $A$ and $\MaxmaxMACRoAF {I}{J}$.

Ideal.Quotient.factorₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the factor of x and hIJ (from the name)

English

Let $x$ be a set. Assume that $I \leq J$. Then the factor of $x$ and $\mathrm{hIJ}$ is an algebra homomorphism of the set of quotients of $A$ and $I$ and the set of quotients of $A$ and $J$.

Ideal.Quotient.liftₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the lift of I and f (from the name)

English

Let $I$ be an ideal of $A$. Let $f$ be an algebra homomorphism of $A$ and $B$ such that for all elements $a$ of $A$, if $a$ is an element of $I$, then $\EqtMACRoH {f (a)}{0}$. Then the lift of $I$ and $f$ is an algebra homomorphism of the set of quotients of $A$ and $I$ and $B$.

Ideal.Quotient.mkₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

no wording

English

Let $x$ be a set. Let $I$ be an ideal of $A$. Then $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $x$ and $I$ is an algebra homomorphism of $A$ and the set of quotients of $A$ and $I$.

Ideal.kerLiftAlgdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the kernel lift algebra of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the kernel lift algebra of $f$ is an algebra homomorphism of the set of quotients of $A$ and the kernel of $f$ and $B$ defined as $\operatorname{mk'}$ applied to the induced map from the quotient by the kernel to the codomain of the ring homomorphism of $f$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Ideal\_\_KerLift\_\_map\_smul}$ applied to $f$, $x_{6}$ and $x_{7}$.

Ideal.powQuotPowSuccEquivMapMkPowSuccPowdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the power quotient power successor equivalence map power successor power of I and n (from the name)

English

Let $I$ be an ideal of $R$. Let $n$ be an element of $\Natural$. Then the power quotient power successor equivalence map power successor power of $I$ and $n$ is an element of $\EquivMACRoAE {\operatorname{Quotient} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {(I ^ {n})}{x_{1}})}, \HSMulhSMulMACRoAL {I}{\operatorname{top}})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{mk} (I ^ {(n + 1)}), I ^ {n})}{x_{2}})})}$ defined as the equivalence of the power quotient power successor linear equivalence map power successor power of $I$ and $n$.

Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPowdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the power quotient power successor linear equivalence map power successor power of I and n (from the name)

English

Let $I$ be an ideal of $R$. Let $n$ be an element of $\Natural$. Then the power quotient power successor linear equivalence map power successor power of $I$ and $n$ is a linear equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {(I ^ {n})}{x_{1}})}$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{mk} (I ^ {(n + 1)}), I ^ {n})}{x_{2}})}$.

Ideal.quotientEquivdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient equivalence of J and f (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $S$. Let $f$ be a ring isomorphism of $R$ and $S$ such that $J$ is equal to the map of the ring homomorphism of $f$ and $I$. Then the quotient equivalence of $J$ and $f$ is a ring isomorphism of the set of quotients of $R$ and $I$ and the set of quotients of $S$ and $J$.

Ideal.quotientEquivAlgdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient equivalence algebra of J and f (from the name)

English

Let $I$ be an ideal of $A$. Let $J$ be an ideal of $B$. Let $f$ be an algebra isomorphism of $A$ and $B$ such that $J$ is equal to the map of the ring homomorphism of $f$ and $I$. Then the quotient equivalence algebra of $J$ and $f$ is an algebra isomorphism of the set of quotients of $A$ and $I$ and the set of quotients of $B$ and $J$.

Ideal.quotientEquivAlgOfEqdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient equivalence algebra of x and h2 (from the name)

English

Let $x$ be a set. Assume that $\EqtMACRoH {I}{J}$. Then the quotient equivalence algebra of $x$ and $h_{2}$ is an algebra isomorphism of the set of quotients of $A$ and $I$ and the set of quotients of $A$ and $J$.

Ideal.quotientInfEquivQuotientProddefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient infimum equivalence quotient product of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$ such that $I$ is coprime to $J$. Then the quotient infimum equivalence quotient product of $I$ and $J$ is a ring isomorphism of the set of quotients of $R$ and $\MinminMACRoAG {I}{J}$ and $\mathrm{Prod}$ applied to the set of quotients of $R$ and $I$ and the set of quotients of $R$ and $J$.

Ideal.quotientInfRingEquivPiQuotientdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient infimum ring isomorphism product quotient of f and hf (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to ideals of $R$ such that $\operatorname{onFun}$ applied to the proposition that $\mathrm{IsCoprime}$ and $f$ is pairwise. Then the quotient infimum ring isomorphism product quotient of $f$ and $\mathrm{hf}$ is a ring isomorphism of the set of quotients of $R$ and the infimum of the function that maps $i$ to $f$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to quotients of $R$ and $f$ applied to $i_{1}$.

Ideal.quotientInfToPiQuotientdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient infimum to product quotient of I (from the name)

English

Let $I$ be a function from elements of $x_{1}$ to ideals of $R$. Then the quotient infimum to product quotient of $I$ is a ring homomorphism of the set of quotients of $R$ and the infimum of the function that maps $i$ to $I$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to quotients of $R$ and $I$ applied to $i_{1}$.

Ideal.quotientKerAlgEquivOfRightInversedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient kernel algebra isomorphism of hf (from the name)

English

Assume that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the quotient kernel algebra isomorphism of $\mathrm{hf}$ is an algebra isomorphism of the set of quotients of $A$ and the kernel of $f$ and $B$.

Ideal.quotientKerAlgEquivOfSurjectivedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient kernel algebra isomorphism of hf (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the quotient kernel algebra isomorphism of $\mathrm{hf}$ is an algebra isomorphism of the set of quotients of $A$ and the kernel of $f$ and $B$.

Ideal.quotientKerEquivRangedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

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

Ideal.quotientMapdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

Let $J$ be an ideal of $S$. Let $f$ be a ring homomorphism of $R$ and $S$ such that $I$ is less than or equal to the preimage of $J$ under $f$. Then the quotient map of $J$ and $f$ is a ring homomorphism of the set of quotients of $R$ and $I$ and the set of quotients of $S$ and $J$.

Ideal.quotientMapₐdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

Let $J$ be an ideal of $B$. Let $f$ be an algebra homomorphism of $A$ and $B$ such that $I$ is less than or equal to the preimage of $J$ under $f$. Then the quotient map of $J$ and $f$ is an algebra homomorphism of the set of quotients of $A$ and $I$ and the set of quotients of $B$ and $J$.

Ideal.quotientMulEquivQuotientProddefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient multiplicative equivalence quotient product of I and J (from the name)

English

Let $I$ and $J$ be ideals of $R$ such that $I$ is coprime to $J$. Then the quotient multiplicative equivalence quotient product of $I$ and $J$ is a ring isomorphism of the set of quotients of $R$ and $I \times J$ and $\mathrm{Prod}$ applied to the set of quotients of $R$ and $I$ and the set of quotients of $R$ and $J$.

RingEquiv.quotientBotdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient of R (from the docstring)

English

Let $R$ be a set. Then the quotient of $R$ is a ring isomorphism of the set of quotients of $R$ and the bottom and $R$.

RingHom.kerLiftdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the induced map from the quotient by the kernel to the codomain of f (from the docstring)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the induced map from the quotient by the kernel to the codomain of $f$ is a ring homomorphism of the set of quotients of $R$ and the kernel of $f$ and $S$.

RingHom.quotientKerEquivOfRightInversedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient kernel equivalence of hf (from the name)

English

Assume that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $\mathrm{hf}$ is a ring isomorphism of the set of quotients of $R$ and the kernel of $f$ and $S$.

RingHom.quotientKerEquivOfSurjectivedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

the quotient kernel equivalence of hf (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $\mathrm{hf}$ is a ring isomorphism of the set of quotients of $R$ and the kernel of $f$ and $S$.

RingHom.quotientKerEquivRangedefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

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

RingHom.quotientKerEquivRangeSdefMathlib.RingTheory.Ideal.Quotient.Operations, function or constant

Wording

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

English

Mathlib.RingTheory.Ideal.Quotient.PowTransition

Ideal.Quotient.factorPowdefMathlib.RingTheory.Ideal.Quotient.PowTransition, function or constant

Wording

the factor power of I and le (from the name)

English

Let $I$ be an ideal of $R$. Assume that $n \leq m$. Then the factor power of $I$ and $\mathrm{le}$ is a ring homomorphism of the set of quotients of $R$ and $I ^ {m}$ and the set of quotients of $R$ and $I ^ {n}$.

Ideal.Quotient.factorPowSuccdefMathlib.RingTheory.Ideal.Quotient.PowTransition, function or constant

Wording

the factor power successor of I and n (from the name)

English

Let $I$ be an ideal of $R$. Let $n$ be a natural number. Then the factor power successor of $I$ and $n$ is a ring homomorphism of the set of quotients of $R$ and $I ^ {(n + 1)}$ and the set of quotients of $R$ and $I ^ {n}$ defined as the factor power of $I$ and $\mathrm{Nat\_\_le\_succ}$ applied to $n$.

Submodule.factorPowdefMathlib.RingTheory.Ideal.Quotient.PowTransition, function or constant

Wording

the factor power 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 factor power 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}}$.

Submodule.factorPowSuccdefMathlib.RingTheory.Ideal.Quotient.PowTransition, function or constant

Wording

the factor power successor of I and m (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Let $m$ be an element of $\Natural$. Then the factor power successor of $I$ and $m$ is a linear map of the set of quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {(m + 1)})}{\operatorname{top}}$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {m})}{\operatorname{top}}$ defined as the factor power of $I$.

Submodule.powSMulQuotInclusiondefMathlib.RingTheory.Ideal.Quotient.PowTransition, function or constant

Wording

the power multiplicative quotient inclusion of I and N (from the name)

English

Let $I$ be an ideal of $R$. Let $M$ be a set. Assume that $c = b + a$. Let $N$ be a submodule of $R$ and $M$. Then the power multiplicative quotient inclusion of $I$ and $N$ is a linear map of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {(\HSMulhSMulMACRoAL {(I ^ {a})}{N})}{x_{3}})}$ and $\HSMulhSMulMACRoAL {(I ^ {b})}{\operatorname{top}}$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {(I ^ {c})}{N}$.

Mathlib.RingTheory.Ideal.Span

Ideal.ofReldefMathlib.RingTheory.Ideal.Span, function or constant

Wording

the ideal generated by an arbitrary binary relation of r (from the docstring)

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the ideal generated by an arbitrary binary relation of $r$ is an ideal of $x$ defined as the span of $x$ and $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exist elements $a$ and $b$ of $x$, such that $r$ holds for $a$ and $b$ and $\EqtMACRoH {x_{2} + b}{a}$.

Ideal.spandefMathlib.RingTheory.Ideal.Span, function or constant

Wording

the span of s (from the name)

English

Let $s$ be an element of $\wp x$. Then the span of $s$ is an ideal of $x$ defined as the span of $x$ and $s$.

IsPrincipalIdealRingclassMathlib.RingTheory.Ideal.Span, predicate

Wording

R is a principal ideal ring (from the docstring)

English

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

Mathlib.RingTheory.IdealFilter.Basic

IdealFilterdefMathlib.RingTheory.IdealFilter.Basic, type

Wording

ideal filter of A (from the name)

English

Let $A$ be a set. Then an ideal filter of $A$ is an element of the function that maps $A$ to the set of filters of the set of ideals of $A$.

IdealFilter.IsGabrielclassMathlib.RingTheory.IdealFilter.Basic, predicate

Wording

no wording

English

Let $F$ be an ideal filter of $A$. Then we can say that $\operatorname{IsGabriel}$ holds for $F$.

IdealFilter.IsTorsiondefMathlib.RingTheory.IdealFilter.Basic, predicate

Wording

F is a torsion (from the name)

English

Let $F$ be an ideal filter of $A$. Let $M$ be a set. Then $F$ is a torsion, if for all elements $m$ of $M$, $\operatorname{IsTorsionElem}$ holds for $F$ and $m$.

IdealFilter.IsTorsionElemdefMathlib.RingTheory.IdealFilter.Basic, predicate

Wording

no wording

English

Let $F$ be an ideal filter of $A$. Let $m$ be an element of $M$. Then $\operatorname{IsTorsionElem}$ holds for $F$ and $m$, if there exists an ideal $L$ of $A$, such that $L$ is an element of $F$ and for all elements $a$ of $A$, if $a$ is an element of $L$, then $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{m}}{0}$.

IdealFilter.IsTorsionQuotdefMathlib.RingTheory.IdealFilter.Basic, predicate

Wording

no wording

English

Let $F$ be an ideal filter of $A$. Let $L$ and $K$ be ideals of $A$. Then $\operatorname{IsTorsionQuot}$ holds for $F$, $L$ and $K$, if for all elements $k$ of $A$, if $k$ is an element of $K$, then there exists an ideal $I$ of $A$, such that $I$ is an element of $F$ and $I$ is less than or equal to the colon of $L$ and $\operatorname{singleton}$ applied to $k$.

IdealFilter.IsUniformclassMathlib.RingTheory.IdealFilter.Basic, predicate

Wording

F is uniform (from the docstring)

English

Let $F$ be an ideal filter of $A$. Then we can say that $F$ is uniform.

IdealFilter.gabrielCompositiondefMathlib.RingTheory.IdealFilter.Basic, function or constant

Wording

no wording

English

Let $F$ and $G$ be ideal filters of $A$. Then $\operatorname{gabrielComposition}$ applied to $F$ and $G$ is an ideal filter of $A$ defined as the filter of $\mathrm{IdealFilter\_\_isPFilter\_gabrielComposition}$ applied to $F$ and $G$.

Mathlib.RingTheory.IdealFilter.Topology

WithIdealFilterdefMathlib.RingTheory.IdealFilter.Topology, type

Wording

no wording

English

Let $x_{1}$ be an ideal filter of $A$. Then an element of $\mathrm{WithIdealFilter}$ applied to $x_{1}$ is an element of the function that maps $x_{1}$ to $A$.

WithIdealFilter.idealSetdefMathlib.RingTheory.IdealFilter.Topology, function or constant

Wording

the ideal set of I (from the name)

English

Let $I$ be an ideal of $A$. Then the ideal set of $I$ is an element of $\wp \mathrm{WithIdealFilter} (F)$ defined as $I$.

Mathlib.RingTheory.Idempotents

AlgEquiv.prodQuotientOfIsIdempotentElemdefMathlib.RingTheory.Idempotents, function or constant

Wording

the product quotient of h and h1 (from the name)

English

Let $R$ be a set. Assume that $e$ is an idempotent element. Assume that $f$ is an idempotent element. Assume that $\EqtMACRoH {e + f}{1}$. Assume that $\EqtMACRoH {e \times f}{0}$. Then the product quotient of $h$ and $h_{1}$ is an algebra isomorphism of $S$ and $\mathrm{Prod}$ applied to the set of quotients of $S$ and the span of $\operatorname{singleton}$ applied to $e$ and the set of quotients of $S$ and the span of $\operatorname{singleton}$ applied to $f$ defined as the algebra isomorphism of the product of $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and the span of $\operatorname{singleton}$ applied to $e$ and $\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_}$ applied to $R$ and the span of $\operatorname{singleton}$ applied to $f$ and $\mathrm{RingHom\_\_prod\_bijective\_of\_isIdempotentElem}$ applied to $\mathrm{he}$, $\mathrm{hf}$, $h$ and $h_{1}$.

CompleteOrthogonalIdempotentsstructureMathlib.RingTheory.Idempotents, predicate

Wording

no wording

English

Let $e$ be a function from elements of $I$ to elements of $R$. Then we can say that $\mathrm{CompleteOrthogonalIdempotents}$ holds for $e$.

CompleteOrthogonalIdempotents.ringEquivOfCommdefMathlib.RingTheory.Idempotents, function or constant

Wording

the ring isomorphism of he (from the name)

English

Assume that $\mathrm{CompleteOrthogonalIdempotents}$ holds for $e$. Then the ring isomorphism of $\mathrm{he}$ is a ring isomorphism of $R$ and the set of functions from elements $i$ of $I$ to corners of $\operatorname{idem}$ applied to $\operatorname{toOrthogonalIdempotents}$ applied to $\mathrm{he}$ and $i$.

CompleteOrthogonalIdempotents.ringEquivOfIsMulCentraldefMathlib.RingTheory.Idempotents, function or constant

Wording

the ring isomorphism of he and hc (from the name)

English

Assume that $\mathrm{CompleteOrthogonalIdempotents}$ holds for $e$. Assume that for all elements $i_{1}$ of $I$, $\mathrm{IsMulCentral}$ holds for $e$ applied to $i_{1}$. Then the ring isomorphism of $\mathrm{he}$ and $\mathrm{hc}$ is a ring isomorphism of $R$ and the set of functions from elements $i$ of $I$ to corners of $\operatorname{idem}$ applied to $\operatorname{toOrthogonalIdempotents}$ applied to $\mathrm{he}$ and $i$.

IsIdempotentElem.CornerdefMathlib.RingTheory.Idempotents, type

Wording

corner of h (from the name)

English

Assume that $e$ is an idempotent element. Then a corner of $h$ is an element of the function that maps $h$ to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{corner} (e)}{x_{1}})}$.

NonUnitalRing.cornerdefMathlib.RingTheory.Idempotents, function or constant

Wording

the corner of e (from the name)

English

Let $e$ be an element of $R$. Then the corner of $e$ is a non unital subring of $R$.

NonUnitalSubsemiring.cornerdefMathlib.RingTheory.Idempotents, function or constant

Wording

the corner of e (from the name)

English

Let $e$ be an element of $R$. Then the corner of $e$ is a non unital subsemiring of $R$.

OrthogonalIdempotentsstructureMathlib.RingTheory.Idempotents, predicate

Wording

no wording

English

Let $e$ be a function from elements of $I$ to elements of $R$. Then we can say that $\mathrm{OrthogonalIdempotents}$ holds for $e$.

Subsemigroup.cornerdefMathlib.RingTheory.Idempotents, function or constant

Wording

the corner of e (from the name)

English

Let $e$ be an element of $R$. Then the corner of $e$ is a subsemigroup of $R$.

Mathlib.RingTheory.IntegralClosure.Algebra.Basic

integralClosuredefMathlib.RingTheory.IntegralClosure.Algebra.Basic, function or constant

Wording

the integral closure of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the integral closure of $R$ and $A$ is a subalgebra of $R$ and $A$.

Mathlib.RingTheory.IntegralClosure.Algebra.Defs

Algebra.IsIntegralclassMathlib.RingTheory.IntegralClosure.Algebra.Defs, predicate

Wording

R is integral (from the docstring)

English

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

Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Algebra.intNormdefMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

the norm of A and B (from the docstring)

English

Let $A$ and $B$ be sets. Then the norm of $A$ and $B$ is a monoid homomorphism of $B$ and $A$ defined as $\operatorname{intNormAux}$ applied to $A$, the set of fraction rings of $A$, the set of fraction rings of $B$ and $B$.

Algebra.intTracedefMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

the trace of A and B (from the docstring)

English

Let $A$ and $B$ be sets. Then the trace of $A$ and $B$ is a linear map of $B$ and $A$ defined as $\operatorname{intTraceAux}$ applied to $A$, the set of fraction rings of $A$, the set of fraction rings of $B$ and $B$.

galLiftdefMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

no wording

English

Let $K$, $L$ and $x$ be sets. Let $x_{17}$ be an algebra homomorphism of $B$ and $x_{1}$. Then $\mathrm{galLift}$ applied to $K$, $L$, $x$ and $x_{17}$ is an algebra homomorphism of $L$ and $x$.

galLiftEquivdefMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

no wording

English

Let $K$, $L$ and $x$ be sets. Let $x_{17}$ be an algebra isomorphism of $B$ and $x_{1}$. Then $\mathrm{galLiftEquiv}$ applied to $K$, $L$, $x$ and $x_{17}$ is an algebra isomorphism of $L$ and $x$.

galRestrictdefMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

no wording

English

Let $A$, $K$, $L$ and $B$ be sets. Then $\mathrm{galRestrict}$ applied to $A$, $K$, $L$ and $B$ is a multiplicative equivalence of the set of algebra isomorphisms of $L$ and $L$ and the set of algebra isomorphisms of $B$ and $B$ defined as the composition of the inverse of the algebra homomorphism unit equivalence of $K$ and $L$ and the composition of the map equivalence of $\mathrm{galRestrictHom}$ applied to $A$, $K$, $L$ and $B$ and the algebra homomorphism unit equivalence of $A$ and $B$.

galRestrict'defMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

no wording

English

Let $A$, $B$ and $x_{1}$ be sets. Let $f$ be an algebra homomorphism of $L$ and $x$. Then $\mathrm{galRestrict'}$ applied to $A$, $B$, $x_{1}$ and $f$ is an algebra homomorphism of $B$ and $x_{1}$.

galRestrictHomdefMathlib.RingTheory.IntegralClosure.IntegralRestrict, function or constant

Wording

no wording

English

Let $A$, $K$, $L$ and $B$ be sets. Then $\mathrm{galRestrictHom}$ applied to $A$, $K$, $L$ and $B$ is a multiplicative equivalence of the set of algebra homomorphisms of $L$ and $L$ and the set of algebra homomorphisms of $B$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $f$ to $\mathrm{galRestrict'}$ applied to $A$, $B$, $B$ and $f$, $\mathrm{galLift}$ applied to $K$, $L$ and $L$, the function that maps $x_{9}$ to $\mathrm{galLift\_galRestrict'}$ applied to $K$, $L$, $L$ and $x_{9}$ and the function that maps $x_{10}$ to $\mathrm{galRestrict'\_galLift}$ applied to $K$, $L$, $L$ and $x_{10}$ and the function that maps $x_{11}$ and $x_{12}$ to $\mathrm{galRestrict'\_comp}$ applied to $A$, $B$, $B$, $B$, $x_{12}$ and $x_{11}$.

Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

IsIntegrallyCloseddefMathlib.RingTheory.IntegralClosure.IntegrallyClosed, predicate

Wording

R is integrally closed (from the docstring)

English

generation took over the time limit

IsIntegrallyClosedIndefMathlib.RingTheory.IntegralClosure.IntegrallyClosed, predicate

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\mathrm{IsIntegrallyClosedIn}$ holds for $R$ and $A$, if $A$ is an integral closure with respect to $R$.

Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

IsAlmostIntegraldefMathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral, predicate

Wording

no wording

English

Let $R$ be a set. Let $s$ be an element of $S$. Then $\mathrm{IsAlmostIntegral}$ holds for $R$ and $s$, if there exists an element $r$ of $R$, such that $r$ is an element of the non zero divisor of $R$ and for all natural numbers $n$, $\HSMulhSMulMACRoAL {r}{(s ^ {n})}$ is an element of the range of the algebra map of $R$ and $S$.

completeIntegralClosuredefMathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral, function or constant

Wording

the complete integral closure of R and S (from the docstring)

English

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

Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

IsIntegraldefMathlib.RingTheory.IntegralClosure.IsIntegral.Defs, predicate

Wording

x3 is integral (from the name)

English

Let $R$ be a set. Let $x_{3}$ be an element of $A$. Then $x_{3}$ is integral, if $x_{3}$ is an integral element with respect to the algebra map of $R$ and $A$.

RingHom.IsIntegraldefMathlib.RingTheory.IntegralClosure.IsIntegral.Defs, predicate

Wording

f is integral (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $A$. Then $f$ is integral, if for all elements $x_{2}$ of $A$, $x_{2}$ is an integral element with respect to $f$.

RingHom.IsIntegralElemdefMathlib.RingTheory.IntegralClosure.IsIntegral.Defs, predicate

Wording

x2 is a integral element with respect to f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $A$. Let $x_{2}$ be an element of $A$. Then $x_{2}$ is an integral element with respect to $f$, if there exists a polynomial $p$ of $R$, such that $p$ is monic and the evaluation of $x_{2}$ and $p$ is equal to $0$.

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

AlgEquiv.mapIntegralClosuredefMathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic, function or constant

Wording

the map integral closure of f (from the name)

English

Let $f$ be an algebra isomorphism of $A$ and $S$. Then the map integral closure of $f$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (R , A)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (R , S)}{x_{6}})}$.

AlgHom.mapIntegralClosuredefMathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic, function or constant

Wording

the map integral closure of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $S$. Then the map integral closure of $f$ is an algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (R , A)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (R , S)}{x_{6}})}$.

IsIntegralClosure.equivdefMathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic, function or constant

Wording

the equivalence of B and #4 (from the name)

English

Let $R$, $A$, $B$ and $\mathrm{A'}$ be sets. Then the equivalence of $B$ and $\mathrm{A'}$ is an algebra isomorphism of $A$ and $\mathrm{A'}$.

IsIntegralClosure.liftdefMathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic, function or constant

Wording

the lift of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the lift of $A$ and $B$ is an algebra homomorphism of $S$ and $A$.

IsIntegralClosure.mk'defMathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic, function or constant

Wording

no wording

English

Let $A$ be a set. Let $x_{5}$ be an integral element of $B$. Then $\operatorname{mk'}$ applied to $A$, $x_{5}$ and $\mathrm{hx}$ is an element of $A$.

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs

IsIntegralClosureclassMathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs, predicate

Wording

B is a integral closure with respect to R (from the name)

English

Let $A$, $R$ and $B$ be sets. Then we can say that $B$ is an integral closure with respect to $R$.

Mathlib.RingTheory.Invariant.Basic

Ideal.Quotient.stabilizerQuotientInertiaEquivdefMathlib.RingTheory.Invariant.Basic, function or constant

Wording

the stabilizer quotient inertia equivalence of P and Q (from the name)

English

Let $G$ be a set. Let $P$ be an ideal of $A$. Let $Q$ be an ideal of $B$. Then the stabilizer quotient inertia equivalence of $P$ and $Q$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , Q)}{x_{5}})}$ and the inertia of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , Q)}{x_{6}})}$ and $Q$ and the set of algebra isomorphisms of the set of quotients of $B$ and $Q$ and the set of quotients of $B$ and $Q$.

IsFractionRing.stabilizerHomdefMathlib.RingTheory.Invariant.Basic, function or constant

Wording

the stabilizer homomorphism of P and Q (from the name)

English

Let $G$, $K$ and $L$ be sets. Let $P$ be an ideal of $A$. Let $Q$ be an ideal of $B$. Then the stabilizer homomorphism of $P$ and $Q$ is a monoid homomorphism of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , Q)}{x_{11}})}$ and the set of algebra isomorphisms of $L$ and $L$ defined as the composition of the field equivalence of $K$ and $L$ and the stabilizer homomorphism of $Q$ and $P$.

IsFractionRing.stabilizerQuotientInertiaEquivdefMathlib.RingTheory.Invariant.Basic, function or constant

Wording

the stabilizer quotient inertia equivalence of P and Q (from the name)

English

Let $G$, $K$ and $L$ be sets. Let $P$ be an ideal of $A$. Let $Q$ be an ideal of $B$. Then the stabilizer quotient inertia equivalence of $P$ and $Q$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , Q)}{x_{11}})}$ and the inertia of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , Q)}{x_{12}})}$ and $Q$ and the set of algebra isomorphisms of $L$ and $L$.

MulSemiringAction.charpolydefMathlib.RingTheory.Invariant.Basic, function or constant

Wording

the characteristic polynomial of G and b (from the name)

English

Let $G$ be a set. Let $b$ be an element of $B$. Then the characteristic polynomial of $G$ and $b$ is a polynomial of $B$ defined as $\FinsetProd {\FinsetunivMACRoAC}{g}{(\operatorname{X} - \operatorname{C} (\HSMulhSMulMACRoAL {g}{b}))}$.

Mathlib.RingTheory.Invariant.Defs

Algebra.IsInvariantclassMathlib.RingTheory.Invariant.Defs, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Invariant.Profinite

Ideal.Quotient.stabilizerHomSurjectiveAuxFunctordefMathlib.RingTheory.Invariant.Profinite, function or constant

Wording

the stabilizer homomorphism surjective functor of Q and x6 (from the name)

English

Let $P$ be an ideal of $A$. Let $Q$ be an ideal of $B$. Let $x_{6}$ be an algebra isomorphism of the set of quotients of $B$ and $Q$ and the set of quotients of $B$ and $Q$. Then the stabilizer homomorphism surjective functor of $Q$ and $x_{6}$ is a functor of the set of open normal subgroups of $G$ and the set of sets.

Mathlib.RingTheory.IsAdjoinRoot

AdjoinRoot.isAdjoinRootdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then $\operatorname{isAdjoinRoot}$ applied to $f$ is an element of $\mathrm{IsAdjoinRoot}$ applied to $\mathrm{AdjoinRoot}$ applied to $f$ and $f$.

AdjoinRoot.isAdjoinRootMonicdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Let $f$ be a monic polynomial of $R$. Then $\operatorname{isAdjoinRootMonic}$ applied to $f$ and $\mathrm{hf}$ is an element of $\mathrm{IsAdjoinRootMonic}$ applied to $\mathrm{AdjoinRoot}$ applied to $f$ and $f$ defined as $\operatorname{mk}$ applied to $\operatorname{isAdjoinRoot}$ applied to $f$ and $\mathrm{hf}$.

IsAdjoinRootstructureMathlib.RingTheory.IsAdjoinRoot, type

Wording

no wording

English

Let $S$ be a set. Let $f$ be a polynomial of $R$. Then the elements of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$ are a basic type.

IsAdjoinRoot.adjoinRootAlgEquivdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Let $h$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Then $\operatorname{adjoinRootAlgEquiv}$ applied to $h$ is an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $f$ and $S$.

IsAdjoinRoot.algEquivdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the algebra isomorphism of h and #2 (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Let $\mathrm{h'}$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $T$ and $f$. Then the algebra isomorphism of $h$ and $\mathrm{h'}$ is an algebra isomorphism of $S$ and $T$ defined as the composition of the inverse of $\operatorname{adjoinRootAlgEquiv}$ applied to $h$ and $\operatorname{adjoinRootAlgEquiv}$ applied to $\mathrm{h'}$.

IsAdjoinRoot.liftdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the lift of i and x4 (from the name)

English

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

IsAdjoinRoot.liftHomdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the lift homomorphism of h and x4 (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Let $x_{4}$ be an element of $T$ such that $\EqtMACRoH {\operatorname{aeval} (x_{4} , f)}{0}$. Then the lift homomorphism of $h$ and $x_{4}$ is an algebra homomorphism of $S$ and $T$.

IsAdjoinRoot.mapdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the map of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Then the map of $\mathrm{self}$ is an algebra homomorphism of the set of polynomials of $R$ and $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

IsAdjoinRoot.mkOfAdjoinEqTopdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then $\operatorname{mkOfAdjoinEqTop}$ applied to $h_{4}$ and $h_{5}$ is an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and the minimal polynomial of $R$ and $x_{3}$.

IsAdjoinRoot.mkOfPrimitiveElementdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $F$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then $\operatorname{mkOfPrimitiveElement}$ applied to $h$ and $h_{1}$ is an element of $\mathrm{IsAdjoinRoot}$ applied to $E$ and the minimal polynomial of $F$ and $x_{3}$.

IsAdjoinRoot.ofAdjoinRootEquivdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Let $e$ be an algebra isomorphism of $\mathrm{AdjoinRoot}$ applied to $f$ and $S$. Then $\operatorname{ofAdjoinRootEquiv}$ applied to $e$ is an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$ defined as $\operatorname{ofAlgEquiv}$ applied to $\operatorname{isAdjoinRoot}$ applied to $f$ and $e$.

IsAdjoinRoot.ofAlgEquivdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Let $h$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Let $e$ be an algebra isomorphism of $S$ and $T$. Then $\operatorname{ofAlgEquiv}$ applied to $h$ and $e$ is an element of $\mathrm{IsAdjoinRoot}$ applied to $T$ and $f$.

IsAdjoinRoot.reprdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the representation of h and x3 (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Let $x_{3}$ be an element of $S$. Then the representation of $h$ and $x_{3}$ is a polynomial of $R$.

IsAdjoinRoot.rootdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the root of h (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRoot}$ applied to $S$ and $f$. Then the root of $h$ is an element of $S$ defined as $\operatorname{map}$ applied to $h$ and $\operatorname{X}$.

IsAdjoinRootMonicstructureMathlib.RingTheory.IsAdjoinRoot, type

Wording

no wording

English

Let $S$ be a set. Let $f$ be a polynomial of $R$. Then the elements of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and $f$ are a basic type.

IsAdjoinRootMonic.basisdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the basis of h (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and $f$. Then the basis of $h$ is a basis of $R$ and $S$.

IsAdjoinRootMonic.coeffdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the coefficient of h (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and $f$. Then the coefficient of $h$ is a linear map of $S$ and the set of functions from natural numbers to elements of $R$.

IsAdjoinRootMonic.liftPolyₗdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the lift polynomial of h and g (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and $f$. Let $g$ be a linear map of the set of polynomials of $R$ and $T$. Then the lift polynomial of $h$ and $g$ is a linear map of $S$ and $T$ defined as the composition of $g$ and $\operatorname{modByMonicHom}$ applied to $h$.

IsAdjoinRootMonic.mkOfAdjoinEqTopdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then $\operatorname{mkOfAdjoinEqTop}$ applied to $h_{4}$ and $h_{5}$ is an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and the minimal polynomial of $R$ and $x_{3}$.

IsAdjoinRootMonic.mkOfAdjoinEqTop'defMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Assume that $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then $\operatorname{mkOfAdjoinEqTop'}$ applied to $h_{2}$ is an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and the minimal polynomial of $R$ and $x_{3}$.

IsAdjoinRootMonic.mkOfPrimitiveElementdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Assume that $x_{3}$ is integral. Assume that $\operatorname{adjoin}$ applied to $F$ and $\operatorname{singleton}$ applied to $x_{3}$ is equal to the top. Then $\operatorname{mkOfPrimitiveElement}$ applied to $h$ and $h_{1}$ is an element of $\mathrm{IsAdjoinRootMonic}$ applied to $E$ and the minimal polynomial of $F$ and $x_{3}$.

IsAdjoinRootMonic.modByMonicHomdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

no wording

English

Let $h$ be an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and $f$. Then $\operatorname{modByMonicHom}$ applied to $h$ is a linear map of $S$ and the set of polynomials of $R$.

IsAdjoinRootMonic.powerBasisdefMathlib.RingTheory.IsAdjoinRoot, function or constant

Wording

the power basis of h (from the name)

English

Let $h$ be an element of $\mathrm{IsAdjoinRootMonic}$ applied to $S$ and $f$. Then the power basis of $h$ is a power basis of $R$ and $S$ defined as $\operatorname{mk}$ applied to the root of $\operatorname{toIsAdjoinRoot}$ applied to $h$, the natural degree of $f$, the basis of $h$ and $\mathrm{IsAdjoinRootMonic\_\_basis\_apply}$ applied to $h$.

Mathlib.RingTheory.IsGaloisGroup.Basic

IsGaloisGroup.mulEquivAlgEquivdefMathlib.RingTheory.IsGaloisGroup.Basic, function or constant

Wording

the multiplicative equivalence algebra isomorphism of A and B (from the name)

English

Let $G$, $A$ and $B$ be sets. Then the multiplicative equivalence algebra isomorphism of $A$ and $B$ is a multiplicative equivalence of $G$ and the set of algebra isomorphisms of $B$ and $B$.

Mathlib.RingTheory.IsGaloisGroup.Defs

IsGaloisGroupclassMathlib.RingTheory.IsGaloisGroup.Defs, predicate

Wording

no wording

English

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

IsGaloisGroup.ringEquivdefMathlib.RingTheory.IsGaloisGroup.Defs, function or constant

Wording

the ring isomorphism of B and #4 (from the name)

English

Let $G$, $A$, $\mathrm{A'}$ and $B$ be sets. Then the ring isomorphism of $\mathrm{A'}$ and $B$ is a ring isomorphism of $A$ and $\mathrm{A'}$ defined as the composition of the ring isomorphism fixed point of $A$ and $B$ and the inverse of the ring isomorphism fixed point of $\mathrm{A'}$ and $B$.

IsGaloisGroup.ringEquivFixedPointsdefMathlib.RingTheory.IsGaloisGroup.Defs, function or constant

Wording

the ring isomorphism fixed point of A and B (from the name)

English

Let $G$, $A$ and $B$ be sets. Then the ring isomorphism fixed point of $A$ and $B$ is a ring isomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{subsemiring} (B , G)}{x_{5}})}$.

Mathlib.RingTheory.IsPrimary

Submodule.IsPrimarydefMathlib.RingTheory.IsPrimary, predicate

Wording

S is primary (from the name)

English

Let $S$ be a submodule of $R$ and $M$. Then $S$ is primary, if $S \neq \operatorname{top}$ and for all elements $r$ of $R$, for all elements $x_{3}$ of $M$, if $\MembershipmemMACRoT {S}{\HSMulhSMulMACRoAL {r}{x_{3}}}$, then $\MembershipmemMACRoT {S}{x_{3}}$ or there exists an element $n$ of $\Natural$ such that $\HSMulhSMulMACRoAL {(r ^ {n})}{\operatorname{top}}\leq S$.

Mathlib.RingTheory.IsTensorProduct

Algebra.IsPushoutclassMathlib.RingTheory.IsTensorProduct, predicate

Wording

no wording

English

Let $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$ be sets. Then we can say that $\operatorname{IsPushout}$ holds for $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$.

Algebra.IsPushout.cancelBaseChangedefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

no wording

English

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

Algebra.IsPushout.cancelBaseChangeAlgdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

no wording

English

Let $R$, $S$, $A$, $B$ and $C$ be sets. Then $\operatorname{cancelBaseChangeAlg}$ applied to $R$, $S$, $A$, $B$ and $C$ is an algebra isomorphism of the set of tensor products of $B$ and $C$ and the set of tensor products of $S$ and $C$.

Algebra.IsPushout.equivdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the equivalence of #3 and #4 (from the name)

English

Let $R$, $S$, $\mathrm{R'}$ and $\mathrm{S'}$ be sets. Then the equivalence of $\mathrm{R'}$ and $\mathrm{S'}$ is an algebra isomorphism of the set of tensor products of $S$ and $\mathrm{R'}$ and $\mathrm{S'}$.

Algebra.pushoutDescdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

no wording

English

Let $\mathrm{S'}$ be a set. Let $f$ be an algebra homomorphism of $S$ and $A$. Let $g$ be an algebra homomorphism of $\mathrm{R'}$ and $A$ such that for all elements $x_{11}$ of $S$, for all elements $y$ of $\mathrm{R'}$, $\EqtMACRoH {f (x_{11})\times g (y)}{g (y)\times f (x_{11})}$. Then $\operatorname{pushoutDesc}$ applied to $\mathrm{S'}$, $f$, $g$ and $\mathrm{hf}$ is an algebra homomorphism of $\mathrm{S'}$ and $A$ defined as the composition of the lift of $f$ and $g$ and $\operatorname{restrictScalars}$ applied to $R$ and the algebra homomorphism of the inverse of the equivalence of $\mathrm{R'}$ and $\mathrm{S'}$.

IsBaseChangedefMathlib.RingTheory.IsTensorProduct, predicate

Wording

f is a base change (from the name)

English

Let $S$ be a set. Let $f$ be a linear map of $M$ and $N$. Then $f$ is a base change, if $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{flip}$ applied to the linear map of $S$ and the set of ends of $S$ and the set of linear maps of $M$ and $N$ and $f$ is a tensor product.

IsBaseChange.equivdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the equivalence of h1 (from the name)

English

Assume that $f$ is a base change. Then the equivalence of $h_{1}$ is a linear equivalence of the set of tensor products of $S$ and $M$ and $N$.

IsBaseChange.liftdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the lift of h1 and g (from the name)

English

Assume that $f$ is a base change. Let $g$ be a linear map of $M$ and $Q$. Then the lift of $h_{1}$ and $g$ is a linear map of $N$ and $Q$.

IsBaseChange.tensorEquivdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the tensor equivalence of hf and P (from the name)

English

Assume that $f$ is a base change. Let $P$ be a set. Then the tensor equivalence of $\mathrm{hf}$ and $P$ is a linear equivalence of the set of tensor products of $P$ and $N$ and the set of tensor products of $P$ and $M$ defined as the composition of the tensor of $P$ and the inverse of the equivalence of $\mathrm{hf}$ and $\operatorname{cancelBaseChange}$ applied to $R$, $S$, $S$, $P$ and $M$.

IsTensorProductdefMathlib.RingTheory.IsTensorProduct, predicate

Wording

f is a tensor product (from the name)

English

Let $f$ be a linear map of $x_{1}$ and the set of linear maps of $x_{2}$ and $M$. Then $f$ is a tensor product, if $\operatorname{coe}$ applied to the lift of $f$ is bijective.

IsTensorProduct.assocdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the associator of f and g (from the name)

English

Let $f$ be a linear map of $x_{3}$ and the set of linear maps of $x_{4}$ and $x_{6}$ such that $\mathrm{LinearMap\_\_restrictScalars\_u2081\_\_u2082\_}$ applied to $R$, $R$ and $f$ is a tensor product. Let $g$ be a linear map of $x_{4}$ and the set of linear maps of $x_{5}$ and $x_{7}$ such that $g$ is a tensor product. Then the associator of $f$ and $g$ is a linear equivalence of the set of tensor products of $x_{6}$ and $x_{5}$ and the set of tensor products of $x_{3}$ and $x_{7}$.

IsTensorProduct.assocOfMapSMuldefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the associator of f and g (from the name)

English

Let $f$ be a linear map of $x_{3}$ and the set of linear maps of $x_{4}$ and $x_{6}$ such that $f$ is a tensor product. Let $g$ be a linear map of $x_{4}$ and the set of linear maps of $x_{5}$ and $x_{7}$ such that $g$ is a tensor product. Assume that for all elements $t$ of $T$, for all elements $x_{27}$ of $x_{3}$, for all elements $y_{1}$ of $x_{4}$, $\EqtMACRoH {\operatorname{coe} (f , \HSMulhSMulMACRoAL {t}{x_{27}}, y_{1})}{\HSMulhSMulMACRoAL {t}{\operatorname{coe} (f , x_{27} , y_{1})}}$. Assume that for all elements $s$ of $S$, for all elements $x_{26}$ of $x_{3}$, for all elements $y$ of $x_{4}$, $\EqtMACRoH {\operatorname{coe} (f , x_{26} , \HSMulhSMulMACRoAL {s}{y})}{\HSMulhSMulMACRoAL {s}{\operatorname{coe} (f , x_{26} , y)}}$. Then the associator of $f$ and $g$ is a linear equivalence of the set of tensor products of $x_{6}$ and $x_{5}$ and the set of tensor products of $x_{3}$ and $x_{7}$.

IsTensorProduct.equivdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the equivalence of h (from the name)

English

Assume that $f$ is a tensor product. Then the equivalence of $h$ is a linear equivalence of the set of tensor products of $x_{1}$ and $x_{2}$ and $M$ defined as the linear equivalence of the lift of $f$ and $h$.

IsTensorProduct.liftdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the lift of h and #2 (from the name)

English

Assume that $f$ is a tensor product. Let $\mathrm{f'}$ be a linear map of $x_{1}$ and the set of linear maps of $x_{2}$ and $\mathrm{M'}$. Then the lift of $h$ and $\mathrm{f'}$ is a linear map of $M$ and $\mathrm{M'}$ defined as the composition of the lift of $\mathrm{f'}$ and $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of $h$.

IsTensorProduct.mapdefMathlib.RingTheory.IsTensorProduct, function or constant

Wording

the map of x17 and x18 (from the name)

English

Assume that $f$ is a tensor product. Assume that $g$ is a tensor product. Let $x_{17}$ be a linear map of $x_{1}$ and $x_{9}$. Let $x_{18}$ be a linear map of $x_{2}$ and $x_{10}$. Then the map of $x_{17}$ and $x_{18}$ is a linear map of $M$ and $N$ defined as the composition of $\operatorname{toLinearMap}$ applied to the equivalence of $\mathrm{hg}$ and the composition of the tensor product of $x_{17}$ and $x_{18}$ and $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of $\mathrm{hf}$.

Mathlib.RingTheory.Jacobson.Ideal

Ideal.IsLocalclassMathlib.RingTheory.Jacobson.Ideal, predicate

Wording

I is local (from the name)

English

Let $I$ be an ideal of $R$. Then we can say that $I$ is local.

Ideal.jacobsondefMathlib.RingTheory.Jacobson.Ideal, function or constant

Wording

the Jacobson radical of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the Jacobson radical of $I$ is an ideal of $R$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $J$ to the proposition that $I \leq J$ and $J$ is maximal.

TwoSidedIdeal.jacobsondefMathlib.RingTheory.Jacobson.Ideal, function or constant

Wording

the Jacobson radical of I (from the docstring)

English

Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then the Jacobson radical of $I$ is an element of $\mathrm{TwoSidedIdeal}$ applied to $R$ defined as $\operatorname{toTwoSided}$ applied to the Jacobson radical of $\operatorname{asIdeal}$ applied to $I$.

Mathlib.RingTheory.Jacobson.Radical

Module.jacobsondefMathlib.RingTheory.Jacobson.Radical, function or constant

Wording

the Jacobson radical of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the Jacobson radical of $R$ and $M$ is a submodule of $R$ and $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $m$ to $\mathrm{IsCoatom}$ applied to $m$.

Ring.jacobsondefMathlib.RingTheory.Jacobson.Radical, function or constant

Wording

the Jacobson radical of R (from the docstring)

English

Let $R$ be a set. Then the Jacobson radical of $R$ is an ideal of $R$ defined as the Jacobson radical of $R$ and $R$.

Mathlib.RingTheory.Jacobson.Ring

IsJacobsonRingclassMathlib.RingTheory.Jacobson.Ring, predicate

Wording

R is a Jacobson ring (from the name)

English

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

IsLocalization.orderIsoOfMaximaldefMathlib.RingTheory.Jacobson.Ring, function or constant

Wording

the order isomorphism of y (from the name)

English

Let $y$ be an element of $R$. Then the order isomorphism of $y$ is an order isomorphism of $\SubtypeSet {p}{\operatorname{IsMaximal} (p)}$ and $\SubtypeSet {p_{1}}{\mathrm{and} (\operatorname{IsMaximal} (p_{1}), \mathrm{not} (\MembershipmemMACRoT {p_{1}}{y}))}$.

Mathlib.RingTheory.Jacobson.Semiprimary

IsSemiprimaryRingclassMathlib.RingTheory.Jacobson.Semiprimary, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Kaehler.Basic

Derivation.liftKaehlerDifferentialdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

no wording

English

Let $D$ be a derivation of $S$ and $M$. Then $\operatorname{liftKaehlerDifferential}$ applied to $D$ is a linear map of $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ and $M$.

Derivation.tensorProductTodefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

no wording

English

Let $D$ be a derivation of $S$ and $M$. Then $\operatorname{tensorProductTo}$ applied to $D$ is a linear map of the set of tensor products of $S$ and $S$ and $M$ defined as the lift of $\operatorname{flip}$ applied to $\operatorname{lsmul}$ applied to $S$ and the set of linear maps of $S$ and $M$ and $\operatorname{toLinearMap}$ applied to $D$.

KaehlerDifferentialdefMathlib.RingTheory.Kaehler.Basic, type

Wording

no wording

English

Let $R$ and $S$ be sets. Then an element of $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ is an element of the function that maps $R$ and $S$ to $\operatorname{Cotangent}$ applied to the ideal of $R$ and $S$.

KaehlerDifferential.DdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{D}$ applied to $R$ and $S$ is a derivation of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

KaehlerDifferential.DLinearMapdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the linear map of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the linear map of $R$ and $S$ is a linear map of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ defined as the composition of $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{fromIdeal}$ applied to $R$ and $S$ and $\operatorname{codRestrict}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and the ideal of $R$ and $S$, the difference between the linear map of $\operatorname{includeRight}$ and the linear map of $\operatorname{includeLeft}$ and $\mathrm{KaehlerDifferential\_\_one\_smul\_sub\_smul\_one\_mem\_ideal}$ applied to $R$.

KaehlerDifferential.derivationQuotKerTotaldefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{derivationQuotKerTotal}$ applied to $R$ and $S$ is a derivation of $S$ and the set of quotients of $\FinsuppMACRoQ {S}{S}$ and $\operatorname{kerTotal}$ applied to $R$ and $S$.

KaehlerDifferential.endEquivdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the end equivalence of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the end equivalence of $R$ and $S$ is an element of $\EquivMACRoAE {\operatorname{End} (S , \mathrm{KaehlerDifferential} (R , S))}{(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (\operatorname{kerSquareLift} (\operatorname{lmul'} (R)), f)}{\operatorname{id} (R , S)})})}$.

KaehlerDifferential.endEquivAuxEquivdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the end equivalence equivalence of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the end equivalence equivalence of $R$ and $S$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (\mathrm{Ideal\_\_Quotient\_\_mk\_u2090\_} (R , \operatorname{cotangentIdeal} (\operatorname{ideal} (R , S))), f)}{\operatorname{toAlgHom} (S , \operatorname{Quotient} (\operatorname{Quotient} (\mathrm{TensorProduct} (S , S), \operatorname{ideal} (R , S)^ {2}), \operatorname{cotangentIdeal} (\operatorname{ideal} (R , S))))})})}{(\SubtypeSet {f_{1}}{(\EqtMACRoH {\operatorname{comp} (\operatorname{kerSquareLift} (\operatorname{lmul'} (R)), f_{1})}{\operatorname{id} (R , S)})})}$ defined as the subtype equivalence of the identity of the set of algebra homomorphisms of $S$ and the set of quotients of the set of tensor products of $S$ and $S$ and $\operatorname{ideal} (R , S)^ {2}$ and $\mathrm{KaehlerDifferential\_\_End\_equiv\_aux}$ applied to $R$ and $S$.

KaehlerDifferential.endEquivDerivation'defMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the end equivalence derivation of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the end equivalence derivation of $R$ and $S$ is a linear equivalence of the set of derivations of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ and the set of derivations of $S$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{cotangentIdeal} (\operatorname{ideal} (R , S))}{x_{3}})}$ defined as $\operatorname{compDer}$ applied to $\operatorname{restrictScalars}$ applied to $S$ and the cotangent equivalence ideal of the ideal of $R$ and $S$.

KaehlerDifferential.fromIdealdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{fromIdeal}$ applied to $R$ and $S$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ideal} (R , S)}{x_{3}})}$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ defined as $\operatorname{toCotangent}$ applied to the ideal of $R$ and $S$.

KaehlerDifferential.idealdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the ideal of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the ideal of $R$ and $S$ is an ideal of the set of tensor products of $S$ and $S$ defined as the kernel of $\operatorname{lmul'}$ applied to $R$.

KaehlerDifferential.kerCotangentToTensordefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the kernel cotangent to tensor of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the kernel cotangent to tensor of $A$ and $B$ is a linear map of $\operatorname{Cotangent}$ applied to the kernel of the algebra map of $A$ and $B$ and the set of tensor products of $B$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$.

KaehlerDifferential.kerToTensordefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the kernel to tensor of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the kernel to tensor of $A$ and $B$ is a linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{algebraMap} (A , B))}{x_{5}})}$ and the set of tensor products of $B$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$.

KaehlerDifferential.kerTotaldefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{kerTotal}$ applied to $R$ and $S$ is a submodule of $S$ and $\FinsuppMACRoQ {S}{S}$ defined as the span of $S$ and the union of the union of the range of the function that maps $x_{3}$ to $\FinsuppsingleMACRoS {\ProdfstMACRoZ {x_{3}}}{1}+ \FinsuppsingleMACRoS {\ProdsndMACRoAA {x_{3}}}{1}- \FinsuppsingleMACRoS {(\ProdfstMACRoZ {x_{3}}+ \ProdsndMACRoAA {x_{3}})}{1}$ and the range of the function that maps $x_{4}$ to $\FinsuppsingleMACRoS {\ProdsndMACRoAA {x_{4}}}{\ProdfstMACRoZ {x_{4}}}+ \FinsuppsingleMACRoS {\ProdfstMACRoZ {x_{4}}}{\ProdsndMACRoAA {x_{4}}}- \FinsuppsingleMACRoS {(\ProdfstMACRoZ {x_{4}}\times \ProdsndMACRoAA {x_{4}})}{1}$ and the range of the function that maps $x_{5}$ to $\FinsuppsingleMACRoS {\operatorname{algebraMap} (R , S , x_{5})}{1}$.

KaehlerDifferential.linearMapEquivDerivationdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the linear map equivalence derivation of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the linear map equivalence derivation of $R$ and $S$ is a linear equivalence of the set of linear maps of $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ and $M$ and the set of derivations of $S$ and $M$.

KaehlerDifferential.mapdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the map of A and B (from the name)

English

Let $R$, $S$, $A$ and $B$ be sets. Then the map of $A$ and $B$ is a linear map of $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$ and $\mathrm{KaehlerDifferential}$ applied to $S$ and $B$ defined as $\operatorname{liftKaehlerDifferential}$ applied to the composition algebra map of $A$ and $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{D}$ applied to $S$ and $B$.

KaehlerDifferential.mapBaseChangedefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the map base change of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the map base change of $A$ and $B$ is a linear map of the set of tensor products of $B$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $B$.

KaehlerDifferential.quotKerTotalEquivdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the quotient kernel total equivalence of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the quotient kernel total equivalence of $R$ and $S$ is a linear equivalence of the set of quotients of $\FinsuppMACRoQ {S}{S}$ and $\operatorname{kerTotal}$ applied to $R$ and $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

KaehlerDifferential.quotientCotangentIdealdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the quotient cotangent ideal of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the quotient cotangent ideal of $R$ and $S$ is an algebra isomorphism of the set of quotients of the set of quotients of the set of tensor products of $S$ and $S$ and the exponentiation of the ideal of $R$ and $S$ to $2$ and the cotangent ideal of the ideal of $R$ and $S$ and $S$.

KaehlerDifferential.quotientCotangentIdealRingEquivdefMathlib.RingTheory.Kaehler.Basic, function or constant

Wording

the quotient cotangent ideal ring isomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the quotient cotangent ideal ring isomorphism of $R$ and $S$ is a ring isomorphism of the set of quotients of the set of quotients of the set of tensor products of $S$ and $S$ and the exponentiation of the ideal of $R$ and $S$ to $2$ and the cotangent ideal of the ideal of $R$ and $S$ and $S$.

Mathlib.RingTheory.Kaehler.JacobiZariski

Algebra.Generators.CotangentSpace.compEquivdefMathlib.RingTheory.Kaehler.JacobiZariski, function or constant

Wording

the composition equivalence of Q and P (from the name)

English

Let $Q$ be a generator of $T$ and $x_{6}$. Let $P$ be a generator of $S$ and $x_{7}$. Then the composition equivalence of $Q$ and $P$ is a linear equivalence of the set of cotangent spaces of the extension of the composition of $Q$ and $P$ and $\mathrm{Prod}$ applied to the set of cotangent spaces of the extension of $Q$ and the set of tensor products of $T$ and the set of cotangent spaces of the extension of $P$ defined as the composition of the representation of the cotangent space basis of the composition of $Q$ and $P$ and the inverse of the representation of the product of the cotangent space basis of $Q$ and the base change of $T$ and the cotangent space basis of $P$.

Algebra.Generators.H1Cotangent.δdefMathlib.RingTheory.Kaehler.JacobiZariski, function or constant

Wording

no wording

English

Let $Q$ be a generator of $T$ and $x_{6}$. Let $P$ be a generator of $S$ and $x_{7}$. Then $\mathrm{Algebra\_\_Generators\_\_H1Cotangent\_\_\_u3b4\_}$ applied to $Q$ and $P$ is a linear map of $\operatorname{H1Cotangent}$ applied to the extension of $Q$ and the set of tensor products of $T$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

Algebra.H1Cotangent.δdefMathlib.RingTheory.Kaehler.JacobiZariski, function or constant

Wording

no wording

English

Let $R$, $S$ and $T$ be sets. Then $\mathrm{Algebra\_\_H1Cotangent\_\_\_u3b4\_}$ applied to $R$, $S$ and $T$ is a linear map of $\operatorname{H1Cotangent}$ applied to $S$ and $T$ and the set of tensor products of $T$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$ defined as $\mathrm{Algebra\_\_Generators\_\_H1Cotangent\_\_\_u3b4\_}$ applied to the self of $S$ and $T$ and the self of $R$ and $S$.

Mathlib.RingTheory.Kaehler.Polynomial

KaehlerDifferential.mvPolynomialBasisdefMathlib.RingTheory.Kaehler.Polynomial, function or constant

Wording

the multivariate polynomial basis of R and x1 (from the name)

English

Let $R$ and $x_{1}$ be sets. Then the multivariate polynomial basis of $R$ and $x_{1}$ is a basis of the set of multivariate polynomials of $x_{1}$ and $R$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and the set of multivariate polynomials of $x_{1}$ and $R$ defined as $\operatorname{ofRepr}$ applied to the relative differential module of $R$ and $x_{1}$.

KaehlerDifferential.mvPolynomialEquivdefMathlib.RingTheory.Kaehler.Polynomial, function or constant

Wording

the relative differential module of R and x1 (from the docstring)

English

Let $R$ and $x_{1}$ be sets. Then the relative differential module of $R$ and $x_{1}$ is a linear equivalence of $\mathrm{KaehlerDifferential}$ applied to $R$ and the set of multivariate polynomials of $x_{1}$ and $R$ and the set of finitely supported functions from $x_{1}$ to the set of multivariate polynomials of $x_{1}$ and $R$.

KaehlerDifferential.polynomialEquivdefMathlib.RingTheory.Kaehler.Polynomial, function or constant

Wording

the relative differential module of the univariate polynomial algebra of R (from the docstring)

English

Let $R$ be a set. Then the relative differential module of the univariate polynomial algebra of $R$ is a linear equivalence of $\mathrm{KaehlerDifferential}$ applied to $R$ and the set of polynomials of $R$ and the set of polynomials of $R$.

Mathlib.RingTheory.Kaehler.TensorProduct

KaehlerDifferential.derivationTensorProductdefMathlib.RingTheory.Kaehler.TensorProduct, function or constant

Wording

the derivation tensor product of A and B (from the name)

English

Let $R$, $S$, $A$ and $B$ be sets. Then the derivation tensor product of $A$ and $B$ is a derivation of $B$ and the set of tensor products of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$.

KaehlerDifferential.tensorKaehlerEquivdefMathlib.RingTheory.Kaehler.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $S$, $A$ and $B$ be sets. Then $\operatorname{tensorKaehlerEquiv}$ applied to $R$, $S$, $A$ and $B$ is a linear equivalence of the set of tensor products of $B$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$ and $\mathrm{KaehlerDifferential}$ applied to $S$ and $B$.

KaehlerDifferential.tensorKaehlerEquivBasedefMathlib.RingTheory.Kaehler.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $S$, $A$ and $B$ be sets. Then $\operatorname{tensorKaehlerEquivBase}$ applied to $R$, $S$, $A$ and $B$ is a linear equivalence of the set of tensor products of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $A$ and $\mathrm{KaehlerDifferential}$ applied to $S$ and $B$.

Mathlib.RingTheory.KrullDimension.Basic

FiniteRingKrullDimdefMathlib.RingTheory.KrullDimension.Basic, predicate

Wording

R is a finite ring Krull dimension (from the name)

English

Let $R$ be a set. Then $R$ is a finite ring Krull dimension, if the set of prime spectra of $R$ is a finite dimensional order.

Ring.KrullDimLEdefMathlib.RingTheory.KrullDimension.Basic, predicate

Wording

no wording

English

Let $n$ be a natural number. Let $R$ be a set. Then $\operatorname{KrullDimLE}$ holds for $n$ and $R$, if $\operatorname{KrullDimLE}$ holds for $n$ and the set of prime spectra of $R$.

ringKrullDimdefMathlib.RingTheory.KrullDimension.Basic, function or constant

Wording

the ring Krull dimension of R (from the name)

English

Let $R$ be a set. Then the ring Krull dimension of $R$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the Krull dimension of the set of prime spectra of $R$.

Mathlib.RingTheory.KrullDimension.Module

Module.supportDimdefMathlib.RingTheory.KrullDimension.Module, function or constant

Wording

the support dimension of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the support dimension of $R$ and $M$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the Krull dimension of the set of elements of the support of $R$ and $M$.

Mathlib.RingTheory.Lasker

IsLaskerdefMathlib.RingTheory.Lasker, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\mathrm{IsLasker}$ holds for $R$ and $M$, if for all submodules $N$ of $R$ and $M$, there exists a finite set $s$ of the set of submodules of $R$ and $M$, such that the infimum of $s$ and $\mathrm{id}$ is equal to $N$ and for all submodules $J$ of $R$ and $M$, if $J$ is an element of $s$, then $J$ is primary.

Submodule.IsMinimalPrimaryDecompositionstructureMathlib.RingTheory.Lasker, predicate

Wording

no wording

English

Let $N$ be a submodule of $R$ and $M$. Let $t$ be a finite set of the set of submodules of $R$ and $M$. Then we can say that $\operatorname{IsMinimalPrimaryDecomposition}$ holds for $N$ and $t$.