Definitions: Mathlib.RingTheory, part 4 of 6

LaurentSeriesdefMathlib.RingTheory.LaurentSeries, type

Wording

type of formal Laurent series with coefficients in R (from the docstring)

English

Let $R$ be a set. Then a type of formal Laurent series with coefficients in $R$ is an element of the function that maps $R$ to the set of Hahn series of $\Integer$ and $R$.

LaurentSeries.Cauchy.coeffdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the coefficient of h and x2 (from the name)

English

Assume that $\mathrm{Cauchy}$ holds for $x_{1}$. Let $x_{2}$ be an integer. Then the coefficient of $h$ and $x_{2}$ is an element of $K$.

LaurentSeries.Cauchy.limitdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the limit of h (from the name)

English

Assume that $\mathrm{Cauchy}$ holds for $x_{1}$. Then the limit of $h$ is a type of formal Laurent series with coefficients in $K$.

LaurentSeries.LaurentSeriesAlgEquivdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the Laurent series algebra isomorphism of K (from the name)

English

Let $K$ be a set. Then the Laurent series algebra isomorphism of $K$ is an algebra isomorphism of the set of types of formal Laurent series with coefficients in $K$ and the set of rational number function adic complements of $K$.

LaurentSeries.LaurentSeriesPkgdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{LaurentSeriesPkg}$ applied to $K$ is an abstract completion of $\mathrm{WithVal}$ applied to the polynomial valuation of $K$.

LaurentSeries.LaurentSeriesRingEquivdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the Laurent series ring isomorphism of K (from the name)

English

Let $K$ be a set. Then the Laurent series ring isomorphism of $K$ is a ring isomorphism of the set of types of formal Laurent series with coefficients in $K$ and the set of rational number function adic complements of $K$ defined as the inverse of $\operatorname{ratfuncAdicComplRingEquiv}$ applied to $K$.

LaurentSeries.RatFuncAdicCompldefMathlib.RingTheory.LaurentSeries, type

Wording

rational number function adic complement of K (from the name)

English

Let $K$ be a set. Then a rational number function adic complement of $K$ is an element of the function that maps $K$ to the set of adic completions of the set of rational number functions of $K$ and the ideal of $K$.

LaurentSeries.comparePkgdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{comparePkg}$ applied to $K$ is a uniform equivalence of the set of rational number function adic complements of $K$ and the set of types of formal Laurent series with coefficients in $K$ defined as the composition of the uniform equivalence of the set of rational number functions of $K$ and the ideal of $K$ and $\operatorname{compareEquiv}$ applied to $\operatorname{ratfuncAdicComplPkg}$ and $\operatorname{LaurentSeriesPkg}$ applied to $K$.

LaurentSeries.derivativedefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the derivative of R (from the docstring)

English

Let $R$ be a set. Then the derivative of $R$ is a linear map of the set of types of formal Laurent series with coefficients in $V$ and the set of types of formal Laurent series with coefficients in $V$ defined as the Hasse derivative of $R$ and $1$.

LaurentSeries.extensionAsRingHomdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the extension as ring homomorphism of K and hf (from the name)

English

Let $K$ be a set such that $\operatorname{coe}$ applied to the composition of the algebra map of the set of rational number functions of $K$ and the set of types of formal Laurent series with coefficients in $K$ and the ring homomorphism of the equivalence of the polynomial valuation of $K$ is continuous. Then the extension as ring homomorphism of $K$ and $\mathrm{hf}$ is a ring homomorphism of the set of completions of $\mathrm{WithVal}$ applied to the polynomial valuation of $K$ and the set of types of formal Laurent series with coefficients in $K$ defined as the completion extension of the composition of the algebra map of the set of rational number functions of $K$ and the set of types of formal Laurent series with coefficients in $K$ and the ring homomorphism of the equivalence of the polynomial valuation of $K$ and $\mathrm{hf}$.

LaurentSeries.hasseDerivdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the Hasse derivative of R and k (from the name)

English

Let $R$ be a set. Let $k$ be a natural number. Then the Hasse derivative of $R$ and $k$ is a linear map of the set of types of formal Laurent series with coefficients in $V$ and the set of types of formal Laurent series with coefficients in $V$.

LaurentSeries.powerSeriesAlgEquivdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the power series algebra isomorphism of K (from the name)

English

Let $K$ be a set. Then the power series algebra isomorphism of $K$ is an algebra isomorphism of the set of power series of $K$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{adicCompletionIntegers} (\mathrm{RatFunc} (K), \operatorname{idealX} (K))}{x_{1}})}$.

LaurentSeries.powerSeriesEquivSubringdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the power series equivalence subring of K (from the name)

English

Let $K$ be a set. Then the power series equivalence subring of $K$ is a ring isomorphism of the set of power series of $K$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{LaurentSeries\_\_powerSeries\_as\_subring} (K)}{x_{1}})}$.

LaurentSeries.powerSeriesPartdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the power series part of x1 (from the name)

English

Let $x_{1}$ be a type of formal Laurent series with coefficients in $R$. Then the power series part of $x_{1}$ is a power series of $R$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to the coefficient function of $x_{1}$ and the sum of the order of $x_{1}$ and $n$.

LaurentSeries.powerSeriesRingEquivdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the power series ring isomorphism of K (from the name)

English

Let $K$ be a set. Then the power series ring isomorphism of $K$ is a ring isomorphism of the set of power series of $K$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{adicCompletionIntegers} (\mathrm{RatFunc} (K), \operatorname{idealX} (K))}{x_{1}})}$ defined as the composition of the composition of the power series equivalence subring of $K$ and the subring map of the Laurent series ring isomorphism of $K$ and the subring congruence of $\mathrm{LaurentSeries\_\_powerSeries\_ext\_subring}$ applied to $K$.

LaurentSeries.powerSeries_as_subringdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the power series as subring of K (from the name)

English

Let $K$ be a set. Then the power series as subring of $K$ is a subring of the set of types of formal Laurent series with coefficients in $K$ defined as the map of the Hahn series of $\Integer$ and $K$ and the top.

LaurentSeries.ratfuncAdicComplPkgdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

no wording

English

$\operatorname{ratfuncAdicComplPkg}$ is an abstract completion of $\mathrm{WithVal}$ applied to the polynomial valuation of $K$ defined as $\operatorname{cPkg}$.

LaurentSeries.ratfuncAdicComplRingEquivdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{ratfuncAdicComplRingEquiv}$ applied to $K$ is a ring isomorphism of the set of rational number function adic complements of $K$ and the set of types of formal Laurent series with coefficients in $K$.

PowerSeries.idealXdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the prime ideal of K (from the docstring)

English

Let $K$ be a set. Then the prime ideal of $K$ is a height one spectrum of the set of power series of $K$.

RatFunc.polynomialValuationXdefMathlib.RingTheory.LaurentSeries, function or constant

Wording

the polynomial valuation of K (from the name)

English

Let $K$ be a set. Then the polynomial valuation of $K$ is a valuation of the set of rational number functions of $K$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as the valuation of the set of rational number functions of $K$ and the ideal of $K$.

Mathlib.RingTheory.Length

Module.lengthdefMathlib.RingTheory.Length, function or constant

Wording

the length of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the length of $R$ and $M$ is a natural number.

Mathlib.RingTheory.LinearDisjoint

Subalgebra.LinearDisjointdefMathlib.RingTheory.LinearDisjoint, predicate

Wording

no wording

English

Let $A$ and $B$ be subalgebras of $R$ and $S$. Then $\operatorname{LinearDisjoint}$ holds for $A$ and $B$, if $\operatorname{LinearDisjoint}$ holds for $\operatorname{toSubmodule}$ applied to $A$ and $\operatorname{toSubmodule}$ applied to $B$.

Subalgebra.LinearDisjoint.basisOfBasisLeftdefMathlib.RingTheory.LinearDisjoint, function or constant

Wording

the basis of #3 (from the name)

English

Subalgebra.LinearDisjoint.basisOfBasisRightdefMathlib.RingTheory.LinearDisjoint, function or constant

Wording

the basis of #3 (from the name)

English

Assume that $\operatorname{LinearDisjoint}$ holds for $A$ and $B$. Assume that $\MaxmaxMACRoAF {A}{B}$ is equal to the top. Let $b$ be a basis of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {B}{x_{5}})}$. Then the basis of $b$ is a basis of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$ and $S$ defined as the map of the base change of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$ and $b$ and the linear equivalence of the left multiplicative map of $H$ and $\mathrm{H'}$.

Subalgebra.LinearDisjoint.mulMapdefMathlib.RingTheory.LinearDisjoint, function or constant

Wording

the multiplicative map of H (from the name)

English

Assume that $\operatorname{LinearDisjoint}$ holds for $A$ and $B$. Then the multiplicative map of $H$ is an algebra isomorphism of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {B}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {A}{B})}{x_{5}})}$.

Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTopdefMathlib.RingTheory.LinearDisjoint, function or constant

Wording

the left multiplicative map of H and #2 (from the name)

English

Assume that $\operatorname{LinearDisjoint}$ holds for $A$ and $B$. Assume that $\MaxmaxMACRoAF {A}{B}$ is equal to the top. Then the left multiplicative map of $H$ and $\mathrm{H'}$ is an algebra isomorphism of the set of tensor products of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {B}{x_{5}})}$ and $S$.

Mathlib.RingTheory.LocalIso

Algebra.IsLocalIsoclassMathlib.RingTheory.LocalIso, predicate

Wording

no wording

English

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

Mathlib.RingTheory.LocalProperties.Basic

LocalizationPreservesdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

Let $P$ be a function from sets $R$ and elements of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring to propositions. Then $\mathrm{LocalizationPreserves}$ holds for $R$ and $P$, if for all sets $R$, for all elements $\mathrm{hR}$ of $\mathrm{CommRing}$ applied to $R$, for all submonoids $M$ of $R$, for all sets $S$, for all elements $\mathrm{hS}$ of $\mathrm{CommRing}$ applied to $S$, for all elements $x$ of $\mathrm{Algebra}$ applied to $R$ and $S$, if $M$ is a localization, then if $R$ holds for $R$ and $\mathrm{hR}$, then $R$ holds for $S$ and $\mathrm{hS}$.

OfLocalizationMaximaldefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

Let $P$ be a function from sets $R$ and elements of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring to propositions. Then $\mathrm{OfLocalizationMaximal}$ holds for $R$ and $P$, if for all sets $R$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, if for all ideals $J$ of $R$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that $J$ is maximal, $R$ holds for $\operatorname{AtPrime}$ applied to $J$ and $\operatorname{instCommRing}$, then $R$ holds for $R$ and $x$.

RingHom.ContainsIdentitiesdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

RingHom.HoldsForLocalizationdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

RingHom.HoldsForLocalizationAwaydefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

RingHom.LocalizationAwayPreservesdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then $\operatorname{LocalizationAwayPreserves}$ holds for $R$, $S$, $x$, $x_{1}$ and $P$, if for all sets $R$ and $S$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all elements $x_{1}$ of $\mathrm{CommRing}$ applied to $S$, for all ring homomorphisms $f$ of $R$ and $S$, for all elements $r$ of $R$, for all sets $\mathrm{R'}$ and $\mathrm{S'}$, for all elements $x_{2}$ of $\mathrm{CommRing}$ applied to $\mathrm{R'}$, for all elements $x_{3}$ of $\mathrm{CommRing}$ applied to $\mathrm{S'}$, for all elements $x_{4}$ of $\mathrm{Algebra}$ applied to $R$ and $\mathrm{R'}$, for all elements $x_{5}$ of $\mathrm{Algebra}$ applied to $S$ and $\mathrm{S'}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{Away}$ applied to $r$ and $\mathrm{R'}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\operatorname{Away}$ applied to $f$ applied to $r$ and $\mathrm{S'}$, if $R$ holds for $R$, $S$, $x$, $x_{1}$ and $f$, then $R$ holds for $\mathrm{R'}$, $\mathrm{S'}$, $x_{2}$, $x_{3}$ and the map of $f$ and $r$.

RingHom.LocalizationPreservesdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

RingHom.OfLocalizationFiniteSpandefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

P is a localization finite span (from the name)

English

Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then $R$ is a localization finite span, if for all sets $R$ and $S$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all elements $x_{1}$ of $\mathrm{CommRing}$ applied to $S$, for all ring homomorphisms $f$ of $R$ and $S$, for all finite sets $s$ of $R$, if the span of $s$ is equal to the top, then if for all elements $r$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$, $R$ holds for $\operatorname{Away}$ applied to $r$, $\operatorname{Away}$ applied to $f$ applied to $r$, $\operatorname{instCommRing}$, $\operatorname{instCommRing}$ and $\operatorname{awayMap}$ applied to $f$ and $r$, then $R$ holds for $R$, $S$, $x$, $x_{1}$ and $f$.

RingHom.OfLocalizationFiniteSpanTargetdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

P is a localization finite span target (from the name)

English

Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then $R$ is a localization finite span target, if for all sets $R$ and $S$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all elements $x_{1}$ of $\mathrm{CommRing}$ applied to $S$, for all ring homomorphisms $f$ of $R$ and $S$, for all finite sets $s$ of $S$, if the span of $s$ is equal to the top, then if for all elements $r$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$, $R$ holds for $R$, $\operatorname{Away}$ applied to $r$, $x$, $\operatorname{instCommRing}$ and the composition of the algebra map of $S$ and $\operatorname{Away}$ applied to $r$ and $f$, then $R$ holds for $R$, $S$, $x$, $x_{1}$ and $f$.

RingHom.OfLocalizationPrimedefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

P is a localization prime (from the name)

English

RingHom.OfLocalizationSpandefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

P is a localization span (from the name)

English

RingHom.OfLocalizationSpanTargetdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

P is a localization span target (from the name)

English

RingHom.PropertyIsLocalstructureMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

P is local (from the docstring)

English

RingHom.StableUnderCompositionWithLocalizationAwaydefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

RingHom.StableUnderCompositionWithLocalizationAwaySourcedefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then $\operatorname{StableUnderCompositionWithLocalizationAwaySource}$ holds for $R$, $S$, $x$, $x_{1}$ and $P$, if for all sets $R$, $S$ and $T$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all elements $x_{1}$ of $\mathrm{CommRing}$ applied to $S$, for all elements $x_{2}$ of $\mathrm{CommRing}$ applied to $T$, for all elements $x_{3}$ of $\mathrm{Algebra}$ applied to $R$ and $S$, for all elements $r$ of $R$, if $\operatorname{Away}$ holds for $r$ and $S$, then for all ring homomorphisms $f$ of $S$ and $T$, if $R$ holds for $S$, $T$, $x_{1}$, $x_{2}$ and $f$, then $R$ holds for $R$, $T$, $x$, $x_{2}$ and the composition of $f$ and the algebra map of $R$ and $S$.

RingHom.StableUnderCompositionWithLocalizationAwayTargetdefMathlib.RingTheory.LocalProperties.Basic, predicate

Wording

no wording

English

Let $P$ be a function from sets $R$ and sets $S$ and elements $x$ of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $S$ is a commutative ring and ring homomorphisms of $R$ and $S$ to propositions. Then $\operatorname{StableUnderCompositionWithLocalizationAwayTarget}$ holds for $R$, $S$, $x$, $x_{1}$ and $P$, if for all sets $R$, $S$ and $T$, for all elements $x$ of $\mathrm{CommRing}$ applied to $R$, for all elements $x_{1}$ of $\mathrm{CommRing}$ applied to $S$, for all elements $x_{2}$ of $\mathrm{CommRing}$ applied to $T$, for all elements $x_{3}$ of $\mathrm{Algebra}$ applied to $S$ and $T$, for all elements $s$ of $S$, if $\operatorname{Away}$ holds for $s$ and $T$, then for all ring homomorphisms $f$ of $R$ and $S$, if $R$ holds for $R$, $S$, $x$, $x_{1}$ and $f$, then $R$ holds for $R$, $T$, $x$, $x_{2}$ and the composition of the algebra map of $S$ and $T$ and $f$.

Mathlib.RingTheory.LocalRing.Basic

IsLocalRing.nonunitsAddSubmonoiddefMathlib.RingTheory.LocalRing.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{nonunitsAddSubmonoid}$ applied to $R$ is an additive submonoid of $R$.

Mathlib.RingTheory.LocalRing.Defs

IsLocalRingclassMathlib.RingTheory.LocalRing.Defs, predicate

Wording

R is local (from the docstring)

English

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

Mathlib.RingTheory.LocalRing.LocalSubring

LocalSubringstructureMathlib.RingTheory.LocalRing.LocalSubring, type

Wording

local subring of R (from the name)

English

Let $R$ be a set. Then the local subrings of $R$ are a basic type.

LocalSubring.copydefMathlib.RingTheory.LocalRing.LocalSubring, function or constant

Wording

the copy of S and s (from the name)

English

Let $S$ be a local subring of $R$. Let $s$ be an element of $\wp R$ such that $s$ is equal to the underlying subring of $S$. Then the copy of $S$ and $s$ is a local subring of $R$ defined as $\operatorname{mk}$ applied to the copy of the underlying subring of $S$ and $s$.

LocalSubring.mapdefMathlib.RingTheory.LocalRing.LocalSubring, function or constant

Wording

the map of f and s (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $s$ be a local subring of $R$. Then the map of $f$ and $s$ is a local subring of $S$ defined as $\operatorname{mk}$ applied to the map of $f$ and the underlying subring of $s$.

LocalSubring.ofPrimedefMathlib.RingTheory.LocalRing.LocalSubring, function or constant

Wording

the localization of A and P (from the docstring)

English

Let $A$ be a subring of $K$. Let $P$ be an ideal of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$. Then the localization of $A$ and $P$ is a local subring of $K$.

LocalSubring.ofPrimeEquivdefMathlib.RingTheory.LocalRing.LocalSubring, function or constant

Wording

the localization of A and P (from the docstring)

English

Let $A$ be a subring of $K$. Let $P$ be an ideal of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$. Then the localization of $A$ and $P$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to $P$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toSubring} (\operatorname{ofPrime} (A , P))}{x_{2}})}$.

LocalSubring.rangedefMathlib.RingTheory.LocalRing.LocalSubring, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the range of $f$ is a local subring of $S$.

LocalSubring.toSubringdefMathlib.RingTheory.LocalRing.LocalSubring, function or constant

Wording

the underlying subring of self (from the docstring)

English

Let $\mathrm{self}$ be a local subring of $R$. Then the underlying subring of $\mathrm{self}$ is a subring of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs

IsLocalRing.maximalIdealdefMathlib.RingTheory.LocalRing.MaximalIdeal.Defs, function or constant

Wording

the maximal ideal of R (from the name)

English

Let $R$ be a set. Then the maximal ideal of $R$ is an ideal of $R$.

Mathlib.RingTheory.LocalRing.Pullback

AlgHom.pullbackdefMathlib.RingTheory.LocalRing.Pullback, function or constant

Wording

the pullback of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $C$. Let $g$ be an algebra homomorphism of $B$ and $C$. Then the pullback of $f$ and $g$ is a subalgebra of $R$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the equalizer of the composition of $f$ and the first component of $A$ and $B$ and the composition of $g$ and the second component of $A$ and $B$.

AlgHom.pullbackFstdefMathlib.RingTheory.LocalRing.Pullback, function or constant

Wording

the pullback first component of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $C$. Let $g$ be an algebra homomorphism of $B$ and $C$. Then the pullback first component of $f$ and $g$ is an algebra homomorphism of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{pullback} (f , g)}{x_{7}})}$ and $A$ defined as the composition of the first component of $A$ and $B$ and the value of the pullback of $f$ and $g$.

AlgHom.pullbackSnddefMathlib.RingTheory.LocalRing.Pullback, function or constant

Wording

the pullback second component of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $C$. Let $g$ be an algebra homomorphism of $B$ and $C$. Then the pullback second component of $f$ and $g$ is an algebra homomorphism of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{pullback} (f , g)}{x_{7}})}$ and $B$ defined as the composition of the second component of $A$ and $B$ and the value of the pullback of $f$ and $g$.

RingHom.pullbackdefMathlib.RingTheory.LocalRing.Pullback, function or constant

Wording

the pullback of f and g (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $T$. Let $g$ be a ring homomorphism of $S$ and $T$. Then the pullback of $f$ and $g$ is a subring of $\mathrm{Prod}$ applied to $R$ and $S$ defined as $\operatorname{eqLocus}$ applied to the composition of $f$ and the first component of $R$ and $S$ and the composition of $g$ and the second component of $R$ and $S$.

RingHom.pullbackFstdefMathlib.RingTheory.LocalRing.Pullback, function or constant

Wording

the pullback first component of f and g (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $T$. Let $g$ be a ring homomorphism of $S$ and $T$. Then the pullback first component of $f$ and $g$ is a ring homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{pullback} (f , g)}{x_{3}})}$ and $R$ defined as the composition of the first component of $R$ and $S$ and the subtype of the pullback of $f$ and $g$.

RingHom.pullbackSnddefMathlib.RingTheory.LocalRing.Pullback, function or constant

Wording

the pullback second component of f and g (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $T$. Let $g$ be a ring homomorphism of $S$ and $T$. Then the pullback second component of $f$ and $g$ is a ring homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{pullback} (f , g)}{x_{3}})}$ and $S$ defined as the composition of the second component of $R$ and $S$ and the subtype of the pullback of $f$ and $g$.

Mathlib.RingTheory.LocalRing.Quotient

IsLocalRing.basisQuotientdefMathlib.RingTheory.LocalRing.Quotient, function or constant

Wording

the basis quotient of b (from the name)

English

Let $b$ be a basis of $R$ and $S$. Then the basis quotient of $b$ is a basis of the set of quotients of $R$ and the maximal ideal of $R$ and the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and the maximal ideal of $R$.

Mathlib.RingTheory.LocalRing.ResidueField.Basic

IsLocalRing.ResidueField.liftdefMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the lift of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the lift of $f$ is a ring homomorphism of the set of residue fields of $R$ and $S$.

IsLocalRing.ResidueField.mapdefMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a ring homomorphism of the set of residue fields of $R$ and the set of residue fields of $S$.

IsLocalRing.ResidueField.mapAlgEquivdefMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map algebra isomorphism of e (from the name)

English

Let $e$ be an algebra isomorphism of $S$ and $T$. Then the map algebra isomorphism of $e$ is an algebra isomorphism of the set of residue fields of $S$ and the set of residue fields of $T$.

IsLocalRing.ResidueField.mapAlgEquiv'defMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map algebra isomorphism of e (from the name)

English

Let $e$ be an algebra isomorphism of $S$ and $T$. Then the map algebra isomorphism of $e$ is an algebra isomorphism of the set of residue fields of $S$ and the set of residue fields of $T$ defined as $\operatorname{extendScalarsOfSurjective}$ applied to $\mathrm{IsLocalRing\_\_residue\_surjective}$ and the map algebra isomorphism of $e$.

IsLocalRing.ResidueField.mapAlgHomdefMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map algebra homomorphism of e (from the name)

English

Let $e$ be an algebra homomorphism of $S$ and $T$. Then the map algebra homomorphism of $e$ is an algebra homomorphism of the set of residue fields of $S$ and the set of residue fields of $T$.

IsLocalRing.ResidueField.mapAlgHom'defMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map algebra homomorphism of e (from the name)

English

Let $e$ be an algebra homomorphism of $S$ and $T$. Then the map algebra homomorphism of $e$ is an algebra homomorphism of the set of residue fields of $S$ and the set of residue fields of $T$ defined as $\operatorname{extendScalarsOfSurjective}$ applied to $\mathrm{IsLocalRing\_\_residue\_surjective}$ and the map algebra homomorphism of $e$.

IsLocalRing.ResidueField.mapAutdefMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map automorphism (from the name)

English

The map automorphism is a monoid homomorphism of the set of ring automorphisms of $R$ and the set of ring automorphisms of the set of residue fields of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mapEquiv}$ and $\mathrm{IsLocalRing\_\_ResidueField\_\_mapEquiv\_refl}$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{IsLocalRing\_\_ResidueField\_\_mapEquiv\_trans}$ applied to $x_{2}$ and $x_{1}$.

IsLocalRing.ResidueField.mapEquivdefMathlib.RingTheory.LocalRing.ResidueField.Basic, function or constant

Wording

the map equivalence of f (from the name)

English

Let $f$ be a ring isomorphism of $R$ and $S$. Then the map equivalence of $f$ is a ring isomorphism of the set of residue fields of $R$ and the set of residue fields of $S$.

Mathlib.RingTheory.LocalRing.ResidueField.Defs

IsLocalRing.ResidueFielddefMathlib.RingTheory.LocalRing.ResidueField.Defs, type

Wording

residue field of R (from the name)

English

Let $R$ be a set. Then a residue field of $R$ is an element of the function that maps $R$ to the set of quotients of $R$ and the maximal ideal of $R$.

IsLocalRing.residuedefMathlib.RingTheory.LocalRing.ResidueField.Defs, function or constant

Wording

the quotient map of R (from the docstring)

English

Let $R$ be a set. Then the quotient map of $R$ is a ring homomorphism of $R$ and the set of residue fields of $R$ defined as $\operatorname{mk}$ applied to the maximal ideal of $R$.

Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Ideal.FiberdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, type

Wording

fiber of p and S (from the name)

English

Let $p$ be an ideal of $R$. Let $S$ be a set. Then a fiber of $p$ and $S$ is an element of the function that maps $p$ and $S$ to the set of tensor products of the set of residue fields of $p$ and $S$.

Ideal.Fiber.algEquivAux₁defMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the algebra isomorphism of p (from the name)

English

Let $p$ be an ideal of $R$. Then the algebra isomorphism of $p$ is an algebra isomorphism of the set of fibers of $p$ and $S$ and the set of quotients of the set of localizations of the algebra map submonoid of $S$ and the complement of $p$ and the map of the algebra map of $S$ and the set of localizations of the algebra map submonoid of $S$ and the complement of $p$ and the map of the algebra map of $R$ and $S$ and $p$.

Ideal.Fiber.algEquivAux₂defMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

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

English

Let $p$ be an ideal of $R$. Let $q$ be an ideal of the set of fibers of $p$ and $S$. Then the algebra isomorphism of $p$ and $q$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to $q$ and the set of quotients of $\operatorname{AtPrime}$ applied to the preimage of $q$ under $\operatorname{includeRight}$ and the map of the algebra map of $S$ and $\operatorname{AtPrime}$ applied to the preimage of $q$ under $\operatorname{includeRight}$ and the map of the algebra map of $R$ and $S$ and $p$.

Ideal.Fiber.algEquivQuotientdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the algebra isomorphism quotient of p (from the name)

English

Let $p$ be an ideal of $R$. Then the algebra isomorphism quotient of $p$ is an algebra isomorphism of the set of fibers of $p$ and $S$ and the set of quotients of the set of localizations of the algebra map submonoid of $S$ and the complement of $p$ and the map of the algebra map of the set of localizations of the complement of $p$ and the set of localizations of the algebra map submonoid of $S$ and the complement of $p$ and the maximal ideal of the set of localizations of the complement of $p$.

Ideal.Fiber.localizationAlgEquivQuotientdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the localization of the fiber of p and q (from the docstring)

English

Let $p$ be an ideal of $R$. Let $q$ be an ideal of the set of fibers of $p$ and $S$. Then the localization of the fiber of $p$ and $q$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to $q$ and the set of quotients of $\operatorname{AtPrime}$ applied to the preimage of $q$ under $\operatorname{includeRight}$ and the map of the algebra map of $R$ and $\operatorname{AtPrime}$ applied to the preimage of $q$ under $\operatorname{includeRight}$ and $p$.

PrimeSpectrum.preimageEquivFiberdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the preimage equivalence fiber of p (from the name)

English

Let $R$ and $S$ be sets. Let $p$ be a prime spectrum of $R$. Then the preimage equivalence fiber of $p$ is an equivalence from the set of elements of the preimage of $\operatorname{comap}$ applied to the algebra map of $R$ and $S$ and $\operatorname{singleton}$ applied to $p$ to the set of prime spectra of the set of fibers of $\operatorname{asIdeal}$ applied to $p$ and $S$.

PrimeSpectrum.preimageHomeomorphFiberdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the preimage homeomorphism fiber of p (from the name)

English

Let $R$ and $S$ be sets. Let $p$ be a prime spectrum of $R$. Then the preimage homeomorphism fiber of $p$ is a homeomorphism of the set of elements of the preimage of $\operatorname{comap}$ applied to the algebra map of $R$ and $S$ and $\operatorname{singleton}$ applied to $p$ and the set of prime spectra of the set of fibers of $\operatorname{asIdeal}$ applied to $p$ and $S$.

PrimeSpectrum.preimageOrderIsoFiberdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the preimage order isomorphism fiber of p (from the name)

English

Let $R$ and $S$ be sets. Let $p$ be a prime spectrum of $R$. Then the preimage order isomorphism fiber of $p$ is an order isomorphism of the set of elements of the preimage of $\operatorname{comap}$ applied to the algebra map of $R$ and $S$ and $\operatorname{singleton}$ applied to $p$ and the set of prime spectra of the set of fibers of $\operatorname{asIdeal}$ applied to $p$ and $S$.

PrimeSpectrum.primesOverOrderIsoFiberdefMathlib.RingTheory.LocalRing.ResidueField.Fiber, function or constant

Wording

the prime over order isomorphism fiber of p (from the name)

English

Let $R$ and $S$ be sets. Let $p$ be an ideal of $R$. Then the prime over order isomorphism fiber of $p$ is an order isomorphism of the set of elements of $\operatorname{primesOver}$ applied to $p$ and $S$ and the set of prime spectra of the set of fibers of $p$ and $S$.

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Ideal.ResidueFielddefMathlib.RingTheory.LocalRing.ResidueField.Ideal, type

Wording

residue field of I (from the name)

English

Let $I$ be an ideal of $R$. Then a residue field of $I$ is an element of the function that maps $I$ to the set of residue fields of $\operatorname{AtPrime}$ applied to $I$.

Ideal.ResidueField.liftdefMathlib.RingTheory.LocalRing.ResidueField.Ideal, 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 $I$ is less than or equal to the kernel of $f$ and the complement of $I$ is less than or equal to the preimage of $f$ and the submonoid consisting of the units of $S$. Then the lift of $I$ and $f$ is a ring homomorphism of the set of residue fields of $I$ and $S$.

Ideal.ResidueField.liftₐdefMathlib.RingTheory.LocalRing.ResidueField.Ideal, 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 $I$ is less than or equal to the kernel of $f$ and the complement of $I$ is less than or equal to the preimage of $f$ and the submonoid consisting of the units of $B$. Then the lift of $I$ and $f$ is an algebra homomorphism of the set of residue fields of $I$ and $B$.

Ideal.ResidueField.mapdefMathlib.RingTheory.LocalRing.ResidueField.Ideal, function or constant

Wording

the map 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 homomorphism of $R$ and $S$ such that $I$ is equal to the preimage of $J$ under $f$. Then the map of $J$ and $f$ is a ring homomorphism of the set of residue fields of $I$ and the set of residue fields of $J$ defined as the map of the local ring homomorphism of $J$ and $f$.

Ideal.ResidueField.mapₐdefMathlib.RingTheory.LocalRing.ResidueField.Ideal, function or constant

Wording

the map 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 homomorphism of $A$ and $B$ such that $I$ is equal to the preimage of $J$ under $\operatorname{toRingHom}$ applied to $f$. Then the map of $J$ and $f$ is an algebra homomorphism of the set of residue fields of $I$ and the set of residue fields of $J$.

Ideal.algEquivResidueFieldOfFielddefMathlib.RingTheory.LocalRing.ResidueField.Ideal, function or constant

Wording

the algebra isomorphism residue field of p (from the name)

English

Let $p$ be an ideal of $k$. Then the algebra isomorphism residue field of $p$ is an algebra isomorphism of $k$ and the set of residue fields of $p$.

Ideal.residueFieldAlgEquivdefMathlib.RingTheory.LocalRing.ResidueField.Ideal, function or constant

Wording

the residue field algebra isomorphism of K and f (from the name)

English

Let $J$ be an ideal of $A$. Let $K$ be an ideal of $B$. Let $f$ be an algebra isomorphism of $A$ and $B$ such that $J$ is equal to the preimage of $K$ under $f$. Then the residue field algebra isomorphism of $K$ and $f$ is an algebra isomorphism of the set of residue fields of $J$ and the set of residue fields of $K$ defined as the map algebra isomorphism of the local algebra isomorphism of $K$ and $f$.

Ideal.residueFieldAlgEquiv'defMathlib.RingTheory.LocalRing.ResidueField.Ideal, function or constant

Wording

the residue field algebra isomorphism of K and f (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $A$. Let $K$ be an ideal of $B$. Let $f$ be an algebra isomorphism of $A$ and $B$ such that $J$ is equal to the preimage of $K$ under $f$. Then the residue field algebra isomorphism of $K$ and $f$ is an algebra isomorphism of the set of residue fields of $J$ and the set of residue fields of $K$ defined as the map algebra isomorphism of the local algebra isomorphism of $K$ and $f$.

Ideal.residueFieldRingEquivdefMathlib.RingTheory.LocalRing.ResidueField.Ideal, function or constant

Wording

the residue field ring isomorphism of K and f (from the name)

English

Let $J$ be an ideal of $A$. Let $K$ be an ideal of $B$. Let $f$ be a ring isomorphism of $A$ and $B$ such that $J$ is equal to the preimage of $K$ under $f$. Then the residue field ring isomorphism of $K$ and $f$ is a ring isomorphism of the set of residue fields of $J$ and the set of residue fields of $K$ defined as the map equivalence of the local ring isomorphism of $K$ and $f$.

Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Polynomial.fiberEquivQuotientdefMathlib.RingTheory.LocalRing.ResidueField.Polynomial, function or constant

Wording

the fiber equivalence quotient of f and p (from the name)

English

Let $f$ be an algebra homomorphism of the set of polynomials of $R$ and $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $p$ be an ideal of $R$. Then the fiber equivalence quotient of $f$ and $p$ is an algebra isomorphism of the set of fibers of $p$ and $S$ and the set of quotients of the set of polynomials of the set of residue fields of $p$ and the map of the map ring homomorphism of the algebra map of $R$ and the set of residue fields of $p$ and the kernel of the ring homomorphism of $f$.

Polynomial.residueFieldMapCAlgEquivdefMathlib.RingTheory.LocalRing.ResidueField.Polynomial, function or constant

Wording

the residue field map algebra isomorphism of I and J (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of the set of polynomials of $R$ such that $J$ is equal to the map of $\operatorname{C}$ and $I$. Then the residue field map algebra isomorphism of $I$ and $J$ is an algebra isomorphism of the set of residue fields of $J$ and the set of rational number functions of the set of residue fields of $I$.

Mathlib.RingTheory.LocalRing.ResidueField.Separable

Algebra.HasSeparableResidueFieldsAtclassMathlib.RingTheory.LocalRing.ResidueField.Separable, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Localization.Algebra

AlgHom.toKerIsLocalizationdefMathlib.RingTheory.Localization.Algebra, function or constant

Wording

no wording

English

Let $M$ be a submonoid of $R$. Let $x_{5}$, $x_{8}$ and $x_{12}$ be sets. Let $f$ be an algebra homomorphism of $A$ and $B$. Then $\operatorname{toKerIsLocalization}$ applied to $M$, $x_{5}$, $x_{8}$, $x_{12}$ and $f$ is a linear map of $\SubtypeSet {x_{18}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{18}})}$ and $\SubtypeSet {x_{19}}{(\MembershipmemMACRoT {\operatorname{ker} (\mathrm{IsLocalization\_\_map\_u2090\_} (M , f))}{x_{19}})}$.

IsLocalization.mapₐdefMathlib.RingTheory.Localization.Algebra, function or constant

Wording

the map of M and f (from the name)

English

Let $M$ be a submonoid of $R$. Let $x_{5}$, $x_{8}$ and $x_{12}$ be sets. Let $f$ be an algebra homomorphism of $A$ and $B$. Then the map of $M$ and $f$ is an algebra homomorphism of $x_{8}$ and $x_{12}$.

RingHom.toKerIsLocalizationdefMathlib.RingTheory.Localization.Algebra, function or constant

Wording

no wording

English

Let $S$ and $Q$ be sets. Let $g$ be a ring homomorphism of $R$ and $P$ such that $M \leq \operatorname{comap} (g , T)$. Then $\operatorname{toKerIsLocalization}$ applied to $S$, $Q$, $g$ and $\mathrm{hy}$ is a linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{ker} (g)}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{map} (g))}{x_{7}})}$.

Mathlib.RingTheory.Localization.AsSubring

Localization.mapToFractionRingdefMathlib.RingTheory.Localization.AsSubring, function or constant

Wording

the canonical map of K (from the docstring)

English

Let $K$ and $B$ be sets. Let $S$ be a submonoid of $A$ such that $S$ is less than or equal to the non zero divisor of $A$. Then the canonical map of $K$ is an algebra homomorphism of $B$ and $K$.

Localization.subalgebradefMathlib.RingTheory.Localization.AsSubring, function or constant

Wording

the subalgebra of S (from the name)

English

Let $K$ be a set. Let $S$ be a submonoid of $A$ such that $S$ is less than or equal to the non zero divisor of $A$. Then the subalgebra of $S$ is a subalgebra of $A$ and $K$.

Localization.subalgebra.ofFielddefMathlib.RingTheory.Localization.AsSubring, function or constant

Wording

the subalgebra of S (from the name)

English

Let $K$ be a set. Let $S$ be a submonoid of $A$ such that $S$ is less than or equal to the non zero divisor of $A$. Then the subalgebra of $S$ is a subalgebra of $A$ and $K$.

Mathlib.RingTheory.Localization.AtPrime.Basic

IsLocalization.AtPrimedefMathlib.RingTheory.Localization.AtPrime.Basic, predicate

Wording

no wording

English

Let $S$ be a set. Let $P$ be an ideal of $R$. Then $\operatorname{AtPrime}$ holds for $S$ and $P$, if the complement of $P$ is a localization.

IsLocalization.AtPrime.equivQuotMaximalIdealdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the equivalence quotient maximal ideal of p and x1 (from the name)

English

Let $p$ be an ideal of $R$. Let $x_{1}$ be a set. Then the equivalence quotient maximal ideal of $p$ and $x_{1}$ is an algebra isomorphism of the set of quotients of $R$ and $p$ and the set of quotients of $x_{1}$ and the maximal ideal of $x_{1}$.

IsLocalization.AtPrime.equivQuotMaximalIdealPowdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the equivalence quotient maximal ideal power of p and n (from the name)

English

Let $p$ be an ideal of $R$. Let $x_{1}$ be a set. Let $n$ be a natural number. Then the equivalence quotient maximal ideal power of $p$ and $n$ is an algebra isomorphism of the set of quotients of $R$ and $p ^ {n}$ and the set of quotients of $x_{1}$ and the exponentiation of the maximal ideal of $x_{1}$ to $n$.

IsLocalization.AtPrime.equivQuotientMapMaximalIdealdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the equivalence quotient map maximal ideal of p (from the name)

English

Let $S$, $x_{1}$ and $x_{4}$ be sets. Let $p$ be an ideal of $R$. Then the equivalence quotient map maximal ideal of $p$ is a ring isomorphism of the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $p$ and the set of quotients of $x_{4}$ and the map of the algebra map of $x_{1}$ and $x_{4}$ and the maximal ideal of $x_{1}$.

IsLocalization.AtPrime.orderIsoOfPrimedefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the order isomorphism of S and I (from the name)

English

Let $S$ be a set. Let $I$ be an ideal of $R$. Then the order isomorphism of $S$ and $I$ is an order isomorphism of $\SubtypeSet {p}{\operatorname{IsPrime} (p)}$ and $\SubtypeSet {p_{1}}{\mathrm{and} (\operatorname{IsPrime} (p_{1}), \mathrm{Leq} (p_{1} , I))}$.

IsLocalization.AtPrime.primeSpectrumOrderIsodefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the prime spectrum of the localization of S and I (from the docstring)

English

Let $S$ be a set. Let $I$ be an ideal of $R$. Then the prime spectrum of the localization of $S$ and $I$ is an order isomorphism of the set of prime spectra of $S$ and the set of elements of $\operatorname{Iic}$ applied to $\operatorname{mk}$ applied to $I$ and $\mathrm{hI}$.

Localization.AtPrimedefMathlib.RingTheory.Localization.AtPrime.Basic, type

Wording

no wording

English

Let $P$ be an ideal of $R$. Then an element of $\operatorname{AtPrime}$ applied to $P$ is an element of the function that maps $P$ to the set of localizations of the complement of $P$.

Localization.AtPrime.mapPiEvalRingHomdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the map product evaluation ring homomorphism of I (from the name)

English

Let $I$ be an ideal of $R$ applied to $i$. Then the map product evaluation ring homomorphism of $I$ is a ring homomorphism of $\operatorname{AtPrime}$ applied to the preimage of $I$ under the evaluation ring homomorphism of $R$ and $i$ and $\operatorname{AtPrime}$ applied to $I$.

Localization.localAlgEquivdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the local algebra isomorphism of J and f (from the name)

English

Let $I$ be an ideal of $S$. Let $J$ be an ideal of $P$. Let $f$ be an algebra isomorphism of $S$ and $P$ such that $I$ is equal to the preimage of $J$ under $f$. Then the local algebra isomorphism of $J$ and $f$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to $I$ and $\operatorname{AtPrime}$ applied to $J$.

Localization.localAlgEquiv'defMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the local algebra isomorphism of K and f (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $S$. Let $K$ be an ideal of $P$. Let $f$ be an algebra isomorphism of $S$ and $P$ such that $J$ is equal to the preimage of $K$ under $f$. Then the local algebra isomorphism of $K$ and $f$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to $J$ and $\operatorname{AtPrime}$ applied to $K$ defined as $\operatorname{extendScalarsOfIsLocalization}$ applied to $\operatorname{AtPrime}$ applied to $I$, the complement of $I$ and the local algebra isomorphism of $K$ and $f$.

Localization.localAlgHomdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the local algebra homomorphism of J and f (from the name)

English

Let $I$ be an ideal of $S$. Let $J$ be an ideal of $P$. Let $f$ be an algebra homomorphism of $S$ and $P$ such that $I$ is equal to the preimage of $J$ under $f$. Then the local algebra homomorphism of $J$ and $f$ is an algebra homomorphism of $\operatorname{AtPrime}$ applied to $I$ and $\operatorname{AtPrime}$ applied to $J$.

Localization.localAlgHom'defMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the local algebra homomorphism of K and f (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $S$. Let $K$ be an ideal of $P$. Let $f$ be an algebra homomorphism of $S$ and $P$ such that $J$ is equal to the preimage of $K$ under $f$. Then the local algebra homomorphism of $K$ and $f$ is an algebra homomorphism of $\operatorname{AtPrime}$ applied to $J$ and $\operatorname{AtPrime}$ applied to $K$ defined as $\operatorname{extendScalarsOfIsLocalization}$ applied to $\operatorname{AtPrime}$ applied to $I$, the complement of $I$ and the local algebra homomorphism of $K$ and $f$.

Localization.localRingEquivdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

the local ring isomorphism of J and f (from the name)

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $P$. Let $f$ be a ring isomorphism of $R$ and $P$ such that $I$ is equal to the preimage of $J$ under $f$. Then the local ring isomorphism of $J$ and $f$ is a ring isomorphism of $\operatorname{AtPrime}$ applied to $I$ and $\operatorname{AtPrime}$ applied to $J$.

Localization.localRingHomdefMathlib.RingTheory.Localization.AtPrime.Basic, function or constant

Wording

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

English

Let $I$ be an ideal of $R$. Let $J$ be an ideal of $P$. Let $f$ be a ring homomorphism of $R$ and $P$ such that $I$ is equal to the preimage of $J$ under $f$. Then the local ring homomorphism of $J$ and $f$ is a ring homomorphism of $\operatorname{AtPrime}$ applied to $I$ and $\operatorname{AtPrime}$ applied to $J$.

Mathlib.RingTheory.Localization.AtPrime.Extension

IsDedekindDomain.primesOverEquivPrimesOverdefMathlib.RingTheory.Localization.AtPrime.Extension, function or constant

Wording

no wording

English

Let $p$ be an ideal of $R$. Let $x_{3}$ and $x_{6}$ be sets. Assume that $p$ is distinct from the bottom. Then $\operatorname{primesOverEquivPrimesOver}$ applied to $p$, $x_{3}$, $x_{6}$ and $\mathrm{hp}$ is an order isomorphism of the set of elements of $\operatorname{primesOver}$ applied to $p$ and $S$ and the set of elements of $\operatorname{primesOver}$ applied to the maximal ideal of $x_{3}$ and $x_{6}$.

IsLocalization.AtPrime.equivQuotientMapOfIsMaximaldefMathlib.RingTheory.Localization.AtPrime.Extension, function or constant

Wording

the equivalence quotient map of p and P (from the name)

English

Let $p$ be an ideal of $R$. Let $x_{3}$ be a set. Let $P$ be an ideal of $S$. Then the equivalence quotient map of $p$ and $P$ is a ring isomorphism of the set of quotients of $S$ and $P$ and the set of quotients of $x_{3}$ and the map of the algebra map of $S$ and $x_{3}$ and $P$.

Mathlib.RingTheory.Localization.Away.AdjoinRoot

Localization.awayEquivAdjoindefMathlib.RingTheory.Localization.Away.AdjoinRoot, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Then $\operatorname{awayEquivAdjoin}$ applied to $r$ is an algebra isomorphism of $\operatorname{Away}$ applied to $r$ and $\mathrm{AdjoinRoot}$ applied to $\operatorname{C} (r)\times \operatorname{X} - 1$.

Mathlib.RingTheory.Localization.Away.Basic

IsLocalization.AwaydefMathlib.RingTheory.Localization.Away.Basic, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $S$ be a set. Then $\operatorname{Away}$ holds for $x_{1}$ and $S$, if the power of $x_{1}$ is a localization.

IsLocalization.Away.awayToAwayLeftdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ and $y$ be elements of $R$. Then $\operatorname{awayToAwayLeft}$ applied to $x_{4}$ and $y$ is a ring homomorphism of $S$ and $P$.

IsLocalization.Away.awayToAwayRightdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ and $y$ be elements of $R$. Then $\operatorname{awayToAwayRight}$ applied to $x_{4}$ and $y$ is a ring homomorphism of $S$ and $P$.

IsLocalization.Away.invSelfdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the inverse self of x3 (from the name)

English

Let $x_{3}$ be an element of $R$. Then the inverse self of $x_{3}$ is an element of $S$ defined as $\operatorname{mk'}$ applied to $S$, $1$ and $x_{3}$.

IsLocalization.Away.liftdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the lift of x4 and hg (from the name)

English

Let $x_{4}$ be an element of $R$ such that $g$ applied to $x_{4}$ is a unit. Then the lift of $x_{4}$ and $\mathrm{hg}$ is a ring homomorphism of $S$ and $P$.

IsLocalization.Away.liftAlgHomdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the lift algebra homomorphism of x4 and hf (from the name)

English

Let $x_{4}$ be an element of $R$ such that $f$ applied to $x_{4}$ is a unit. Then the lift algebra homomorphism of $x_{4}$ and $\mathrm{hf}$ is an algebra homomorphism of $S$ and $P$.

IsLocalization.Away.mapdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the map of f and r (from the name)

English

Let $S$ and $Q$ be sets. Let $f$ be a ring homomorphism of $R$ and $P$. Let $r$ be an element of $R$. Then the map of $f$ and $r$ is a ring homomorphism of $S$ and $Q$.

IsLocalization.Away.mapₐdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the map of f and a (from the name)

English

Let $x_{5}$ and $x_{9}$ be sets. Let $f$ be an algebra homomorphism of $A$ and $B$. Let $a$ be an element of $A$. Then the map of $f$ and $a$ is an algebra homomorphism of $x_{5}$ and $x_{9}$.

IsLocalization.Away.secdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be an element of $R$. Let $s$ be an element of $S$. Then $\operatorname{sec}$ applied to $x_{3}$ and $s$ is an element of $\mathrm{Prod}$ applied to $R$ and $\Natural$.

IsLocalization.atOnedefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the localization at one of R and S (from the docstring)

English

Let $R$ and $S$ be sets. Then the localization at one of $R$ and $S$ is an algebra isomorphism of $R$ and $S$.

IsLocalization.atUnitdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Let $x_{3}$ be an element of $R$ such that $x_{3}$ is a unit. Then $\operatorname{atUnit}$ applied to $R$, $S$, $x_{3}$ and $e$ is an algebra isomorphism of $R$ and $S$.

Localization.awayLiftdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $P$. Let $r$ be an element of $R$ such that $f$ applied to $r$ is a unit. Then $\operatorname{awayLift}$ applied to $f$, $r$ and $\mathrm{hr}$ is a ring homomorphism of $\operatorname{Away}$ applied to $r$ and $P$ defined as the lift of $r$ and $\mathrm{hr}$.

Localization.awayMapdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $P$. Let $r$ be an element of $R$. Then $\operatorname{awayMap}$ applied to $f$ and $r$ is a ring homomorphism of $\operatorname{Away}$ applied to $r$ and $\operatorname{Away}$ applied to $f$ applied to $r$ defined as the map of $f$ and $r$.

Localization.awayMapₐdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

no wording

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $a$ be an element of $A$. Then $\mathrm{Localization\_\_awayMap\_u2090\_}$ applied to $f$ and $a$ is an algebra homomorphism of $\operatorname{Away}$ applied to $a$ and $\operatorname{Away}$ applied to $f$ applied to $a$ defined as the map of $f$ and $a$.

selfZPowdefMathlib.RingTheory.Localization.Away.Basic, function or constant

Wording

the self power of x1 and m (from the name)

English

Let $x_{1}$ be an element of $R$. Let $B$ be a set. Let $m$ be an integer. Then the self power of $x_{1}$ and $m$ is an element of $B$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (0 , m)$, the function that maps $h_{1}$ to $\operatorname{algebraMap} (R , B , x_{1})^ {\IntnatAbsMACRoY {m}}$ and the function that maps $h_{2}$ to $\operatorname{mk'}$ applied to $B$, $1$ and the power of $x_{1}$ and $\IntnatAbsMACRoY {m}$.

Mathlib.RingTheory.Localization.Away.Lemmas

IsLocalization.Away.mulNumeratordefMathlib.RingTheory.Localization.Away.Lemmas, function or constant

Wording

the multiplicative numerator of p and t1 (from the name)

English

Let $s$ be an element of $\wp R$. Let $p$ be a function from elements $t_{1}$ of $s$ to elements of $\wp x_{1} (t_{1})$. Let $x_{4}$ be an element of $\Sigma$ applied to the function that maps $t$ to the set of elements of $p$ applied to $t$. Then the multiplicative numerator of $t_{1}$ and $p$ is an element of $R$ defined as the function that maps $x_{4}$ to $\mathrm{times} (\operatorname{fst} (p), \ProdfstMACRoZ {\operatorname{sec} (\operatorname{fst} (p), \operatorname{snd} (p))}, x_{4})$.

Mathlib.RingTheory.Localization.BaseChange

IsLocalization.Away.tensorEquivdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the tensor equivalence of r (from the name)

English

Let $S$ and $A$ be sets. Let $r$ be an element of $R$. Then the tensor equivalence of $r$ is an algebra isomorphism of the set of tensor products of $S$ and $A$ and $\operatorname{Away}$ applied to $\operatorname{algebraMap}$ applied to $R$, $S$ and $r$ defined as the algebra isomorphism of the power of $\operatorname{algebraMap}$ applied to $R$, $S$ and $r$.

IsLocalization.Away.tensorProductEquivTMulRightdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the right tensor product equivalence multiplicative of g (from the name)

English

Let $R$, $S$ and $B$ be sets. Let $g$ be an element of $A$. Then the right tensor product equivalence multiplicative of $g$ is an algebra isomorphism of the set of tensor products of $S$ and $B$ and $\operatorname{Away}$ applied to $\operatorname{tmul}$ applied to $R$, $1$ and $g$ defined as the tensor product equivalence of the power of $g$.

IsLocalization.Away.tensorRightEquivdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the tensor right equivalence of r (from the name)

English

Let $S$ and $A$ be sets. Let $r$ be an element of $R$. Then the tensor right equivalence of $r$ is an algebra isomorphism of the set of tensor products of $A$ and $S$ and $\operatorname{Away}$ applied to $\operatorname{algebraMap}$ applied to $R$, $S$ and $r$ defined as the algebra isomorphism of the power of $\operatorname{algebraMap}$ applied to $R$, $S$ and $r$.

IsLocalization.algebraLiddefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $A$ and $B$ be sets. Then $\operatorname{algebraLid}$ applied to $S$, $A$ and $B$ is an algebra isomorphism of the set of tensor products of $A$ and $B$ and $B$ defined as $\operatorname{lidOfCompatibleSMul}$ applied to $R$, $A$ and $B$.

IsLocalization.algebraTensorEquivdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the algebra tensor equivalence of S (from the name)

English

Let $S$ be a submonoid of $R$. Let $A$, $B$ and $C$ be sets. Then the algebra tensor equivalence of $S$ is an algebra isomorphism of the set of tensor products of $B$ and $C$ and the set of tensor products of $B$ and $C$ defined as the equivalence of $B$ and $C$.

IsLocalization.moduleLiddefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $A$ and $x_{3}$ be sets. Then $\operatorname{moduleLid}$ applied to $S$, $A$ and $x_{3}$ is a linear equivalence of the set of tensor products of $A$ and $x_{3}$ and $x_{3}$ defined as the composition of the inverse of the equivalence of $A$ and $x_{3}$ and $\operatorname{lid}$ applied to $A$ and $x_{3}$.

IsLocalization.moduleTensorEquivdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the module tensor equivalence of S (from the name)

English

Let $S$ be a submonoid of $R$. Let $A$, $x_{3}$ and $x_{4}$ be sets. Then the module tensor equivalence of $S$ is a linear equivalence of the set of tensor products of $x_{3}$ and $x_{4}$ and the set of tensor products of $x_{3}$ and $x_{4}$ defined as the equivalence of $x_{3}$ and $x_{4}$.

IsLocalization.tensorProductEquivOfMapIncludeRightdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the tensor product equivalence of M (from the name)

English

Let $R$, $S$, $B$ and $C$ be sets. Let $M$ be a submonoid of $A$. Then the tensor product equivalence of $M$ is an algebra isomorphism of the set of tensor products of $S$ and $B$ and $C$ defined as $\operatorname{restrictScalars}$ applied to $S$ and the algebra isomorphism of the map of $\operatorname{includeRight}$ and $M$.

Localization.tensorLeftAlgEquivdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the isomorphism of M and S (from the docstring)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the isomorphism of $M$ and $S$ is an algebra isomorphism of the set of tensor products of $S$ and the set of localizations of $M$ and the set of localizations of the algebra map submonoid of $S$ and $M$ defined as the inverse of the algebra isomorphism of the algebra map submonoid of $S$ and $M$ and the set of tensor products of $S$ and the set of localizations of $M$.

Localization.tensorRightAlgEquivdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the isomorphism of M and S (from the docstring)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the isomorphism of $M$ and $S$ is an algebra isomorphism of the set of tensor products of the set of localizations of $M$ and $S$ and the set of localizations of the algebra map submonoid of $S$ and $M$.

LocalizedModule.equivTensorProductdefMathlib.RingTheory.Localization.BaseChange, function or constant

Wording

the equivalence tensor product of S and M (from the name)

English

Let $S$ be a submonoid of $R$. Let $M$ be a set. Then the equivalence tensor product of $S$ and $M$ is a linear equivalence of the set of localized modules of $S$ and $M$ and the set of tensor products of the set of localizations of $S$ and $M$ defined as the inverse of the equivalence of $\operatorname{isBaseChange}$ applied to $S$ and $M$.

Mathlib.RingTheory.Localization.Basic

AlgEquiv.extendScalarsOfIsLocalizationdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

no wording

English

Let $S$ be a set. Let $M$ be a submonoid of $R$. Let $f$ be an algebra isomorphism of $A$ and $B$. Then $\operatorname{extendScalarsOfIsLocalization}$ applied to $S$, $M$ and $f$ is an algebra isomorphism of $A$ and $B$.

AlgHom.extendScalarsOfIsLocalizationdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

no wording

English

Let $S$ be a set. Let $M$ be a submonoid of $R$. Let $f$ be an algebra homomorphism of $A$ and $B$. Then $\operatorname{extendScalarsOfIsLocalization}$ applied to $S$, $M$ and $f$ is an algebra homomorphism of $A$ and $B$.

IsLocalization.algEquivdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

the algebra isomorphism of M (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ and $Q$ be sets. Then the algebra isomorphism of $M$ is an algebra isomorphism of $S$ and $Q$.

IsLocalization.algEquivOfAlgEquivdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

the algebra isomorphism of h4 (from the name)

English

Let $S$ and $Q$ be sets. Let $h_{4}$ be an algebra isomorphism of $R$ and $P$ such that the map of $h_{4}$ and $M$ is equal to $T$. Then the algebra isomorphism of $h_{4}$ is an algebra isomorphism of $S$ and $Q$.

IsLocalization.atUnitsdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $M$ be a submonoid of $R$ such that $M$ is less than or equal to the submonoid consisting of the units of $R$. Then $\operatorname{atUnits}$ applied to $R$, $M$ and $H$ is an algebra isomorphism of $R$ and $S$.

IsLocalization.liftAlgHomdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

the lift algebra homomorphism of hf (from the name)

English

Assume that for all elements $y$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {M}{x_{8}})}$, $f$ applied to $y$ is a unit. Then the lift algebra homomorphism of $\mathrm{hf}$ is an algebra homomorphism of $S$ and $P$.

Localization.algEquivdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

the algebra isomorphism of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the algebra isomorphism of $M$ and $S$ is an algebra isomorphism of the set of localizations of $M$ and $S$ defined as the algebra isomorphism of $M$.

Localization.mapPiEvalRingHomdefMathlib.RingTheory.Localization.Basic, function or constant

Wording

the map product evaluation ring homomorphism of S (from the name)

English

Let $S$ be a submonoid of $R$ applied to $i$. Then the map product evaluation ring homomorphism of $S$ is a ring homomorphism of the set of localizations of the preimage of the evaluation ring homomorphism of $R$ and $i$ and $S$ and the set of localizations of $S$.

Mathlib.RingTheory.Localization.Defs

IsLocalizationdefMathlib.RingTheory.Localization.Defs, predicate

Wording

M is a localization (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then $M$ is a localization, if $\mathrm{IsLocalization'}$ holds for $M$ and $S$.

IsLocalization.liftdefMathlib.RingTheory.Localization.Defs, function or constant

Wording

the lift of hg (from the name)

English

Assume that for all elements $y$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {M}{x_{4}})}$, $g$ applied to $y$ is a unit. Then the lift of $\mathrm{hg}$ is a ring homomorphism of $S$ and $P$.

IsLocalization.mapdefMathlib.RingTheory.Localization.Defs, function or constant

Wording

the map of g (from the name)

English

Let $Q$ be a set. Let $g$ be a ring homomorphism of $R$ and $P$ such that $M$ is less than or equal to the preimage of $g$ and $T$. Then the map of $g$ is a ring homomorphism of $S$ and $Q$.

IsLocalization.mk'defMathlib.RingTheory.Localization.Defs, function or constant

Wording

no wording

English

Let $S$ be a set. Let $x_{3}$ be an element of $R$. Let $y$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {M}{x_{4}})}$. Then $\operatorname{mk'}$ applied to $S$, $x_{3}$ and $y$ is an element of $S$ defined as $\operatorname{mk'}$ applied to the localization map of $M$ and $S$, $x_{3}$ and $y$.

IsLocalization.ringEquivOfRingEquivdefMathlib.RingTheory.Localization.Defs, function or constant

Wording

the ring isomorphism of h2 (from the name)

English

Let $S$ and $Q$ be sets. Let $h_{2}$ be a ring isomorphism of $R$ and $P$ such that the map of the monoid homomorphism of $h_{2}$ and $M$ is equal to $T$. Then the ring isomorphism of $h_{2}$ is a ring isomorphism of $S$ and $Q$.

IsLocalization.secdefMathlib.RingTheory.Localization.Defs, function or constant

Wording

no wording

English

Let $M$ be a submonoid of $R$. Let $z$ be an element of $S$. Then $\operatorname{sec}$ applied to $M$ and $z$ is an element of $\mathrm{Prod}$ applied to $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ defined as $\operatorname{choose}$ applied to $\operatorname{surj}$ applied to $M$ and $z$.

IsLocalization.toLocalizationMapdefMathlib.RingTheory.Localization.Defs, function or constant

Wording

the localization map of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the localization map of $M$ and $S$ is a localization map of $M$ and $S$.

Localization.mkAddMonoidHomdefMathlib.RingTheory.Localization.Defs, function or constant

Wording

the additive monoid homomorphism of b (from the name)

English

Let $b$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {M}{x_{1}})}$. Then the additive monoid homomorphism of $b$ is an additive monoid homomorphism of $R$ and the set of localizations of $M$.

Mathlib.RingTheory.Localization.FractionRing

FractionRingdefMathlib.RingTheory.Localization.FractionRing, type

Wording

fraction ring of R (from the name)

English

Let $R$ be a set. Then a fraction ring of $R$ is an element of the function that maps $R$ to the set of localizations of the non zero divisor of $R$.

FractionRing.algEquivdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

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

English

Let $A$ and $K$ be sets. Then the algebra isomorphism of $A$ and $K$ is an algebra isomorphism of the set of fraction rings of $A$ and $K$ defined as the algebra isomorphism of the non zero divisor of $A$ and $K$.

IsFractionRingdefMathlib.RingTheory.Localization.FractionRing, predicate

Wording

no wording

English

Let $R$ and $K$ be sets. Then $\mathrm{IsFractionRing}$ holds for $R$ and $K$, if the non zero divisor of $R$ is a localization.

IsFractionRing.algEquivdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

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

English

Let $R$, $K$ and $L$ be sets. Then the algebra isomorphism of $K$ and $L$ is an algebra isomorphism of $K$ and $L$.

IsFractionRing.algEquivOfAlgEquivdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the algebra isomorphism of h4 (from the name)

English

Let $h_{4}$ be an algebra isomorphism of $A$ and $B$. Then the algebra isomorphism of $h_{4}$ is an algebra isomorphism of $K$ and $L$.

IsFractionRing.fieldEquivOfAlgEquivdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the field equivalence of f (from the name)

English

Let $\mathrm{FA}$, $\mathrm{FB}$ and $\mathrm{FC}$ be sets. Let $f$ be an algebra isomorphism of $B$ and $C$. Then the field equivalence of $f$ is an algebra isomorphism of $\mathrm{FB}$ and $\mathrm{FC}$.

IsFractionRing.fieldEquivOfAlgEquivHomdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the field equivalence of K and L (from the name)

English

Let $K$ and $L$ be sets. Then the field equivalence of $K$ and $L$ is a monoid homomorphism of the set of algebra isomorphisms of $B$ and $B$ and the set of algebra isomorphisms of $L$ and $L$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{fieldEquivOfAlgEquiv}$ and $\mathrm{IsFractionRing\_\_fieldEquivOfAlgEquiv\_refl}$ applied to $A$, $B$, $K$ and $L$ and the function that maps $f$ and $g$ to $\mathrm{IsFractionRing\_\_fieldEquivOfAlgEquiv\_trans}$ applied to $K$, $L$, $L$, $L$, $g$ and $f$.

IsFractionRing.invdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the inverse of A and z (from the docstring)

English

Let $A$ be a set. Let $z$ be an element of $K$. Then the inverse of $A$ and $z$ is an element of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{IsFractionRing\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_RingTheory\_\_Localization\_\_FractionRing\_\_1935392398\_\_\_hygCtx\_\_\_hyg\_\_2}$, $A$ and $z$.

IsFractionRing.liftdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the lift of hg (from the name)

English

Assume that $\operatorname{coe}$ applied to $g$ is injective. Then the lift of $\mathrm{hg}$ is a ring homomorphism of $K$ and $L$ defined as the lift of the function that maps $y$ to $\mathrm{IsFractionRing\_\_isUnit\_map\_of\_injective}$ applied to $\mathrm{hg}$ and $y$.

IsFractionRing.liftAlgHomdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the lift algebra homomorphism of hg (from the name)

English

Assume that $\operatorname{coe}$ applied to $g$ is injective. Then the lift algebra homomorphism of $\mathrm{hg}$ is an algebra homomorphism of $K$ and $L$.

IsFractionRing.mapdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the map of hj (from the name)

English

Assume that $\operatorname{coe}$ applied to $j$ is injective. Then the map of $\mathrm{hj}$ is a ring homomorphism of $K$ and $L$.

IsFractionRing.ringEquivOfRingEquivdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the ring isomorphism of h2 (from the name)

English

Let $h_{2}$ be a ring isomorphism of $A$ and $B$. Then the ring isomorphism of $h_{2}$ is a ring isomorphism of $K$ and $L$.

IsFractionRing.ringEquivOfRingEquivHomdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the ring isomorphism of A and K (from the name)

English

Let $A$ and $K$ be sets. Then the ring isomorphism of $A$ and $K$ is a monoid homomorphism of the set of ring isomorphisms of $A$ and $A$ and the set of ring isomorphisms of $K$ and $K$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ringEquivOfRingEquiv}$ and $\mathrm{IsFractionRing\_\_ringEquivOfRingEquiv\_refl}$ and the function that maps $f$ and $g$ to $\mathrm{IsFractionRing\_\_ringEquivOfRingEquiv\_comp}$ applied to $K$, $K$, $K$, $g$ and $f$.

IsFractionRing.semilinearEquivOfRingEquivdefMathlib.RingTheory.Localization.FractionRing, function or constant

Wording

the semilinear equivalence of f (from the name)

English

Let $K$ and $L$ be sets. Let $f$ be a ring isomorphism of $A$ and $B$. Then the semilinear equivalence of $f$ is a linear equivalence of $K$ and $L$.

Mathlib.RingTheory.Localization.Ideal

IsLocalization.mapFrameHomdefMathlib.RingTheory.Localization.Ideal, function or constant

Wording

the map frame homomorphism of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the map frame homomorphism of $M$ and $S$ is a frame homomorphism of the set of ideals of $R$ and the set of ideals of $S$.

IsLocalization.orderEmbeddingdefMathlib.RingTheory.Localization.Ideal, function or constant

Wording

the order embedding of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the order embedding of $M$ and $S$ is an order embedding of the set of ideals of $S$ and the set of ideals of $R$.

IsLocalization.orderIsoOfPrimedefMathlib.RingTheory.Localization.Ideal, function or constant

Wording

the order isomorphism of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the order isomorphism of $M$ and $S$ is an order isomorphism of $\SubtypeSet {p}{\operatorname{IsPrime} (p)}$ and $\SubtypeSet {p_{1}}{\mathrm{and} (\operatorname{IsPrime} (p_{1}), \mathrm{Disjoint} (M , p_{1}))}$.

IsLocalization.primeSpectrumOrderIsodefMathlib.RingTheory.Localization.Ideal, function or constant

Wording

the prime spectrum of the localization of M and S (from the docstring)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the prime spectrum of the localization of $M$ and $S$ is an order isomorphism of the set of prime spectra of $S$ and $\SubtypeSet {p}{\mathrm{Disjoint} (M , \operatorname{asIdeal} (p))}$.

Mathlib.RingTheory.Localization.Integer

IsLocalization.IsIntegerdefMathlib.RingTheory.Localization.Integer, predicate

Wording

a is a integer (from the name)

English

Let $R$ be a set. Let $a$ be an element of $S$. Then $a$ is an integer, if $a$ is an element of the range of the algebra map of $R$ and $S$.

IsLocalization.commonDenomdefMathlib.RingTheory.Localization.Integer, function or constant

Wording

no wording

English

Let $M$ be a submonoid of $R$. Let $s$ be a finite set of $x_{3}$. Let $f$ be a function from elements of $x_{3}$ to elements of $S$. Then $\operatorname{commonDenom}$ applied to $M$, $s$ and $f$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {M}{x_{4}})}$ defined as $\operatorname{choose}$ applied to $\mathrm{IsLocalization\_\_exist\_integer\_multiples}$ applied to $M$, $s$ and $f$.

IsLocalization.commonDenomOfFinsetdefMathlib.RingTheory.Localization.Integer, function or constant

Wording

no wording

English

Let $M$ be a submonoid of $R$. Let $s$ be a finite set of $S$. Then $\operatorname{commonDenomOfFinset}$ applied to $M$ and $s$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ defined as $\operatorname{commonDenom}$ applied to $M$, $s$ and $\mathrm{id}$.

IsLocalization.finsetIntegerMultipledefMathlib.RingTheory.Localization.Integer, function or constant

Wording

the finite set integer multiple of M and s (from the name)

English

Let $M$ be a submonoid of $R$. Let $s$ be a finite set of $S$. Then the finite set integer multiple of $M$ and $s$ is a finite set of $R$ defined as the forward image of $\operatorname{attach}$ applied to $s$ under the function that maps $t$ to the integer multiple of $\mathrm{id}$ and $t$.

IsLocalization.integerMultipledefMathlib.RingTheory.Localization.Integer, function or constant

Wording

the integer multiple of f and i (from the name)

English

Let $M$ be a submonoid of $R$. Let $s$ be a finite set of $x_{3}$. Let $f$ be a function from elements of $x_{3}$ to elements of $S$. Let $i$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$. Then the integer multiple of $f$ and $i$ is an element of $R$.

Mathlib.RingTheory.Localization.Integral

IsLocalization.integerNormalizationdefMathlib.RingTheory.Localization.Integral, function or constant

Wording

the integer normalization of M and p (from the name)

English

Let $M$ be a submonoid of $R$. Let $p$ be a polynomial of $S$. Then the integer normalization of $M$ and $p$ is a polynomial of $R$.

Mathlib.RingTheory.Localization.InvSubmonoid

IsLocalization.equivInvSubmonoiddefMathlib.RingTheory.Localization.InvSubmonoid, function or constant

Wording

the equivalence inverse submonoid of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the equivalence inverse submonoid of $M$ and $S$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{algebraMap} (R , S), M)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{invSubmonoid} (M , S)}{x_{4}})}$ defined as the inverse of the left inverse equivalence of the map of the algebra map of $R$ and $S$ and $M$ and $\mathrm{IsLocalization\_\_submonoid\_map\_le\_is\_unit}$ applied to $M$ and $S$.

IsLocalization.invSubmonoiddefMathlib.RingTheory.Localization.InvSubmonoid, function or constant

Wording

the inverse submonoid of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the inverse submonoid of $M$ and $S$ is a submonoid of $S$ defined as the left inverse of the map of the algebra map of $R$ and $S$ and $M$.

IsLocalization.toInvSubmonoiddefMathlib.RingTheory.Localization.InvSubmonoid, function or constant

Wording

the inverse submonoid of M and S (from the name)

English

Let $M$ be a submonoid of $R$. Let $S$ be a set. Then the inverse submonoid of $M$ and $S$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{invSubmonoid} (M , S)}{x_{4}})}$ defined as the composition of the monoid homomorphism of the equivalence inverse submonoid of $M$ and $S$ and the submonoid map of the monoid homomorphism of the algebra map of $R$ and $S$ and $M$.

Mathlib.RingTheory.Localization.LocalizationLocalization

IsLocalization.localizationLocalizationAtPrimeIsoLocalizationdefMathlib.RingTheory.Localization.LocalizationLocalization, function or constant

Wording

the localization localization at prime isomorphism localization of M and p (from the name)

English

Let $M$ be a submonoid of $R$. Let $p$ be an ideal of the set of localizations of $M$. Then the localization localization at prime isomorphism localization of $M$ and $p$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to the preimage of $p$ under the algebra map of $R$ and the set of localizations of $M$ and $\operatorname{AtPrime}$ applied to $p$ defined as the algebra isomorphism of the complement of the preimage of $p$ under the algebra map of $R$ and the set of localizations of $M$.

IsLocalization.localizationLocalizationSubmoduledefMathlib.RingTheory.Localization.LocalizationLocalization, function or constant

Wording

the localization localization submodule of M and N (from the name)

English

Let $M$ be a submonoid of $R$. Let $N$ be a submonoid of $S$. Then the localization localization submodule of $M$ and $N$ is a submonoid of $R$ defined as the preimage of the algebra map of $R$ and $S$ and the maximum of $N$ and the map of the algebra map of $R$ and $S$ and $M$.

Mathlib.RingTheory.Localization.Module

IsLocalizedModule.mapEquivdefMathlib.RingTheory.Localization.Module, function or constant

Wording

the map equivalence of g and e (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $g$ be a linear map of $N$ and $\mathrm{N'}$. Let $x_{9}$ be a set. Let $e$ be a linear equivalence of $M$ and $N$. Then the map equivalence of $g$ and $e$ is a linear equivalence of $\mathrm{M'}$ and $\mathrm{N'}$.

IsLocalizedModule.mapExtendScalarsdefMathlib.RingTheory.Localization.Module, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $g$ be a linear map of $N$ and $\mathrm{N'}$. Let $x_{9}$ be a set. Then $\operatorname{mapExtendScalars}$ applied to $S$, $f$, $g$ and $x_{9}$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of $\mathrm{M'}$ and $\mathrm{N'}$ defined as the composition of $\operatorname{toLinearMap}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{extendScalarsOfIsLocalizationEquiv}$ applied to $S$ and $x_{9}$ and the map of $f$ and $g$.

LinearEquiv.extendScalarsOfIsLocalizationdefMathlib.RingTheory.Localization.Module, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $A$ be a set. Let $f$ be a linear equivalence of $M$ and $N$. Then $\operatorname{extendScalarsOfIsLocalization}$ applied to $S$, $A$ and $f$ is a linear equivalence of $M$ and $N$.

LinearEquiv.extendScalarsOfIsLocalizationEquivdefMathlib.RingTheory.Localization.Module, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $A$ be a set. Then $\operatorname{extendScalarsOfIsLocalizationEquiv}$ applied to $S$ and $A$ is an equivalence from the set of linear equivalences of $M$ and $N$ to the set of linear equivalences of $M$ and $N$.

LinearMap.extendScalarsOfIsLocalizationdefMathlib.RingTheory.Localization.Module, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $A$ be a set. Let $f$ be a linear map of $M$ and $N$. Then $\operatorname{extendScalarsOfIsLocalization}$ applied to $S$, $A$ and $f$ is a linear map of $M$ and $N$.

LinearMap.extendScalarsOfIsLocalizationEquivdefMathlib.RingTheory.Localization.Module, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $A$ be a set. Then $\operatorname{extendScalarsOfIsLocalizationEquiv}$ applied to $S$ and $A$ is a linear equivalence of the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $N$.

LocalizedModule.mapdefMathlib.RingTheory.Localization.Module, function or constant

Wording

the map of S (from the name)

English

Let $S$ be a submonoid of $R$. Then the map of $S$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of the set of localized modules of $S$ and $M$ and the set of localized modules of $S$ and $N$ defined as $\operatorname{mapExtendScalars}$ applied to $S$, the linear map of $S$ and $M$, the linear map of $S$ and $N$ and the set of localizations of $S$.

Module.Basis.localizationLocalizationdefMathlib.RingTheory.Localization.Module, function or constant

Wording

the localization localization of S and b (from the name)

English

Let $x$ and $x_{6}$ be sets. Let $S$ be a submonoid of $R$. Let $b$ be a basis of $R$ and $A$. Then the localization localization of $S$ and $b$ is a basis of $x$ and $x_{6}$ defined as the basis of the linear map of the algebra homomorphism of $A$ and $x_{6}$ and $b$.

Module.Basis.ofIsLocalizedModuledefMathlib.RingTheory.Localization.Module, function or constant

Wording

the basis of f and b (from the name)

English

Let $x$ be a set. Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $x_{4}$. Let $b$ be a basis of $R$ and $M$. Then the basis of $f$ and $b$ is a basis of $x$ and $x_{4}$.

Mathlib.RingTheory.Localization.NumDen

IsFractionRing.dendefMathlib.RingTheory.Localization.NumDen, function or constant

Wording

the denominator of A and x3 (from the name)

English

Let $A$ be a set. Let $x_{3}$ be an element of $K$. Then the denominator of $A$ and $x_{3}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (A)}{x_{4}})}$.

IsFractionRing.numdefMathlib.RingTheory.Localization.NumDen, function or constant

Wording

the numerator of A and x3 (from the name)

English

Let $A$ be a set. Let $x_{3}$ be an element of $K$. Then the numerator of $A$ and $x_{3}$ is an element of $A$ defined as $\operatorname{choose}$ applied to $\mathrm{IsFractionRing\_\_exists\_reduced\_fraction}$ applied to $A$ and $x_{3}$.

Mathlib.RingTheory.Localization.Submodule

IsLocalization.coeSubmoduledefMathlib.RingTheory.Localization.Submodule, function or constant

Wording

the coercion submodule of S and I (from the name)

English

Let $S$ be a set. Let $I$ be an ideal of $R$. Then the coercion submodule of $S$ and $I$ is a submodule of $R$ and $S$ defined as the map of the linear map of $R$ and $S$ and $I$.

Mathlib.RingTheory.MatrixAlgebra

Matrix.kroneckerAlgEquivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

Let $m$, $n$ and $R$ be sets. Then $\operatorname{kroneckerAlgEquiv}$ applied to $m$, $n$ and $R$ is an algebra isomorphism of the set of tensor products of the set of matrixes of $m$ and $R$ and the set of matrixes of $n$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $n$ and $R$ defined as the composition of $\operatorname{kroneckerTMulAlgEquiv}$ applied to $m$, $n$, $R$, $R$, $R$ and $R$ and the map matrix of $\operatorname{lid}$ applied to $R$ and $R$.

Matrix.kroneckerStarAlgEquivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

Let $m$, $n$ and $R$ be sets. Then $\operatorname{kroneckerStarAlgEquiv}$ applied to $m$, $n$ and $R$ is a star algebra isomorphism of the set of tensor products of the set of matrixes of $m$ and $R$ and the set of matrixes of $n$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $n$ and $R$.

Matrix.kroneckerTMulAlgEquivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

Let $m$, $n$, $R$, $S$, $A$ and $B$ be sets. Then $\operatorname{kroneckerTMulAlgEquiv}$ applied to $m$, $n$, $R$, $S$, $A$ and $B$ is an algebra isomorphism of the set of tensor products of the set of matrixes of $m$ and $A$ and the set of matrixes of $n$ and $B$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $n$ and the set of tensor products of $A$ and $B$.

Matrix.kroneckerTMulStarAlgEquivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

Let $m$, $n$, $R$, $S$, $A$ and $B$ be sets. Then $\operatorname{kroneckerTMulStarAlgEquiv}$ applied to $m$, $n$, $R$, $S$, $A$ and $B$ is a star algebra isomorphism of the set of tensor products of the set of matrixes of $m$ and $A$ and the set of matrixes of $n$ and $B$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $n$ and the set of tensor products of $A$ and $B$.

MatrixEquivTensor.equivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

the equivalence of R and A (from the name)

English

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

MatrixEquivTensor.invFundefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

the inverse function of M (from the name)

English

Let $n$, $R$ and $A$ be sets. Let $M$ be a matrix of $n$ and $A$. Then the inverse function of $M$ is a tensor product of $A$ and the set of matrixes of $n$ and $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{p}{\operatorname{tmul} (R , M (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {p}), \operatorname{single} (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {p}, 1))}$.

MatrixEquivTensor.toFunAlgHomdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

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

English

Let $n$, $R$ and $A$ be sets. Then the function algebra homomorphism of $R$ and $A$ is an algebra homomorphism of the set of tensor products of $A$ and the set of matrixes of $n$ and $R$ and the set of matrixes of $n$ and $A$.

MatrixEquivTensor.toFunBilineardefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

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

English

Let $n$, $R$ and $A$ be sets. Then the function bilinear of $R$ and $A$ is a linear map of $A$ and the set of linear maps of the set of matrixes of $n$ and $R$ and the set of matrixes of $n$ and $A$ defined as the complement of the linear map of $\operatorname{lsmul}$ applied to $R$, $R$ and the set of matrixes of $n$ and $A$ and the map matrix of the linear map of $R$ and $A$.

MatrixEquivTensor.toFunLineardefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

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

kroneckerLinearEquivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

Let $l$, $m$, $n$, $p$ and $R$ be sets. Then $\mathrm{kroneckerLinearEquiv}$ applied to $l$, $m$, $n$, $p$ and $R$ is a linear equivalence of the set of tensor products of the set of matrixes of $m$ and $R$ and the set of matrixes of $p$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $p$ and $R$ defined as the composition of $\mathrm{kroneckerTMulLinearEquiv}$ applied to $l$, $m$, $n$, $p$, $R$, $R$, $R$ and $R$ and the map matrix of $\operatorname{lid}$ applied to $R$ and $R$.

kroneckerTMulLinearEquivdefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

no wording

English

Let $l$, $m$, $n$, $p$, $R$, $S$, $M$ and $N$ be sets. Then $\mathrm{kroneckerTMulLinearEquiv}$ applied to $l$, $m$, $n$, $p$, $R$, $S$, $M$ and $N$ is a linear equivalence of the set of tensor products of the set of matrixes of $m$ and $M$ and the set of matrixes of $p$ and $N$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $p$ and the set of tensor products of $M$ and $N$.

matrixEquivTensordefMathlib.RingTheory.MatrixAlgebra, function or constant

Wording

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

English

Let $n$, $R$ and $A$ be sets. Then the matrix equivalence tensor of $R$ and $A$ is an algebra isomorphism of the set of matrixes of $n$ and $A$ and the set of tensor products of $A$ and the set of matrixes of $n$ and $R$.

Mathlib.RingTheory.MatrixPolynomialAlgebra

RingHom.polyToMatrixdefMathlib.RingTheory.MatrixPolynomialAlgebra, function or constant

Wording

the polynomial to matrix of f (from the name)

English

Let $f$ be a ring homomorphism of $A$ and the set of matrixes of $n$ and $R$. Then the polynomial to matrix of $f$ is a ring homomorphism of the set of polynomials of $A$ and the set of matrixes of $n$ and the set of polynomials of $R$ defined as the composition of the ring homomorphism of the ring isomorphism of the inverse of the matrix polynomial equivalence and the map ring homomorphism of $f$.

matPolyEquivdefMathlib.RingTheory.MatrixPolynomialAlgebra, function or constant

Wording

the matrix polynomial equivalence (from the name)

English

The matrix polynomial equivalence is an algebra isomorphism of the set of matrixes of $n$ and the set of polynomials of $R$ and the set of polynomials of the set of matrixes of $n$ and $R$ defined as the composition of the composition of the matrix equivalence tensor of $R$ and the set of polynomials of $R$ and $\operatorname{comm}$ applied to $R$, the set of polynomials of $R$ and the set of matrixes of $n$ and $R$ and the inverse of the polynomial equivalence tensor of $R$ and the set of matrixes of $n$ and $R$.

Mathlib.RingTheory.Morita.Basic

IsMoritaEquivalentstructureMathlib.RingTheory.Morita.Basic, predicate

Wording

no wording

English

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

MoritaEquivalencestructureMathlib.RingTheory.Morita.Basic, type

Wording

no wording

English

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

MoritaEquivalence.eqvdefMathlib.RingTheory.Morita.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $A$ and $B$. Then $\operatorname{eqv}$ applied to $\mathrm{self}$ is an equivalence of the set of module categories of $A$ and the set of module categories of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

MoritaEquivalence.ofAlgEquivdefMathlib.RingTheory.Morita.Basic, function or constant

Wording

no wording

English

Let $f$ be an algebra isomorphism of $A$ and $B$. Then $\operatorname{ofAlgEquiv}$ applied to $f$ is an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $A$ and $B$.

MoritaEquivalence.refldefMathlib.RingTheory.Morita.Basic, function or constant

Wording

the identity of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the identity of $R$ and $A$ is an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $A$ and $A$.

MoritaEquivalence.symmdefMathlib.RingTheory.Morita.Basic, function or constant

Wording

the inverse of R and e (from the name)

English

Let $R$ be a set. Let $e$ be an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $A$ and $B$. Then the inverse of $R$ and $e$ is an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $B$ and $A$.

MoritaEquivalence.transdefMathlib.RingTheory.Morita.Basic, function or constant

Wording

the composition of e and #3 (from the name)

English

Let $R$ be a set. Let $e$ be an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $A$ and $B$. Let $\mathrm{e'}$ be an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $B$ and $C$. Then the composition of $e$ and $\mathrm{e'}$ is an element of $\mathrm{MoritaEquivalence}$ applied to $R$, $A$ and $C$.

Mathlib.RingTheory.Morita.Matrix

MatrixModCat.counitIsodefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the counit isomorphism of R and i (from the name)

English

Let $R$ be a set. Let $i$ be an element of $x$. Then the counit isomorphism of $R$ and $i$ is an isomorphism of the composition of the module category of $R$ and $i$ and the matrix module category of $R$ and $x$ and the identity of the set of module categories of the set of matrixes of $x$ and $R$.

MatrixModCat.fromMatrixLineardefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Let $f$ be a linear map of $M$ and $N$. Then $\operatorname{fromMatrixLinear}$ applied to $i$ and $f$ is a linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{toModuleCatObj} (i)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{toModuleCatObj} (i)}{x_{11}})}$.

MatrixModCat.toModuleCatdefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the module category of R and i (from the name)

English

Let $R$ be a set. Let $i$ be an element of $x$. Then the module category of $R$ and $i$ is a functor of the set of module categories of the set of matrixes of $x$ and $R$ and the set of module categories of $R$.

MatrixModCat.toModuleCatObjdefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the module category object of i (from the name)

English

Let $R$ and $M$ be sets. Let $i$ be an element of $x$. Then the module category object of $i$ is a submodule of $R$ and $M$.

MatrixModCat.unitIsodefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the unit isomorphism of R and i (from the name)

English

Let $R$ be a set. Let $i$ be an element of $x$. Then the unit isomorphism of $R$ and $i$ is an isomorphism of the composition of the matrix module category of $R$ and $x$ and the module category of $R$ and $i$ and the identity of the set of module categories of $R$.

ModuleCat.matrixEquivalencedefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the matrix equivalence of R and i (from the name)

English

Let $R$ be a set. Let $i$ be an element of $x$. Then the matrix equivalence of $R$ and $i$ is an equivalence of the set of module categories of $R$ and the set of module categories of the set of matrixes of $x$ and $R$.

ModuleCat.toMatrixModCatdefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the matrix module category of R and x (from the name)

English

Let $R$ and $x$ be sets. Then the matrix module category of $R$ and $x$ is a functor of the set of module categories of $R$ and the set of module categories of the set of matrixes of $x$ and $R$.

fromModuleCatToModuleCatLinearEquivtoModuleCatObjdefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Let $i$ be an element of $x$. Then $\mathrm{fromModuleCatToModuleCatLinearEquivtoModuleCatObj}$ applied to $R$, $M$ and $i$ is a linear equivalence of the set of carriers of the action of the composition of the matrix module category of $R$ and $x$ and the module category of $R$ and $i$ and $\operatorname{of}$ applied to $R$ and $M$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{toModuleCatObj} (i)}{x_{6}})}$.

moritaEquivalenceMatrixdefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

no wording

English

Let $R$ and $x_{4}$ be sets. Let $i$ be an element of $x$. Then $\mathrm{moritaEquivalenceMatrix}$ applied to $R$, $x_{4}$ and $i$ is an element of $\mathrm{MoritaEquivalence}$ applied to $x_{4}$, $R$ and the set of matrixes of $x$ and $R$.

toModuleCatFromModuleCatLinearEquivdefMathlib.RingTheory.Morita.Matrix, function or constant

Wording

the module category from module category linear equivalence of M and j (from the name)

English

Let $R$ be a set. Let $M$ be a module category of the set of matrixes of $x$ and $R$. Let $j$ be an element of $x$. Then the module category from module category linear equivalence of $M$ and $j$ is a linear equivalence of the set of carriers of $M$ and the set of functions from elements of $x$ to elements of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{toModuleCatObj} (j)}{x_{5}})}$.

Mathlib.RingTheory.Multiplicity

FiniteMultiplicitydefMathlib.RingTheory.Multiplicity, predicate

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\mathrm{FiniteMultiplicity}$ holds for $a$ and $b$, if there exists a natural number $n$, such that $a ^ {(n + 1)}$ does not divide $b$.

emultiplicitydefMathlib.RingTheory.Multiplicity, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\mathrm{emultiplicity}$ applied to $a$ and $b$ is a natural number defined as $\mathrm{dite}$ applied to $\mathrm{FiniteMultiplicity}$ applied to $a$ and $b$, the function that maps $h$ to $\operatorname{find}$ applied to $h$ and the function that maps $h_{1}$ to the top.

multiplicitydefMathlib.RingTheory.Multiplicity, function or constant

Wording

the multiplicity of a in b (by hand)

English

Let $a$ and $b$ be elements of $x$. Then the multiplicity of $a$ in $b$ is a natural number defined as the natural number of $\mathrm{emultiplicity}$ applied to $a$ and $b$.

Mathlib.RingTheory.MvPolynomial.Basic

MvPolynomial.basisMonomialsdefMathlib.RingTheory.MvPolynomial.Basic, function or constant

Wording

the basis monomial of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the basis monomial of $x$ and $R$ is a basis of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{ofRepr}$ applied to the coefficient linear equivalence of $R$.

MvPolynomial.basisRestrictSupportdefMathlib.RingTheory.MvPolynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $s$ be an element of $\wp (\FinsuppMACRoQ {x}{\Natural})$. Then $\operatorname{basisRestrictSupport}$ applied to $R$ and $s$ is a basis of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{restrictSupport} (R , s)}{x_{2}})}$ defined as $\operatorname{ofRepr}$ applied to $\operatorname{supportedEquivFinsupp}$ applied to $s$.

MvPolynomial.restrictDegreedefMathlib.RingTheory.MvPolynomial.Basic, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $m$ be a natural number. Then $\operatorname{restrictDegree}$ applied to $x$, $R$ and $m$ is a submodule of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{restrictSupport}$ applied to $R$ and $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that for all elements $i$ of $x$, $n (i)\leq m$.

MvPolynomial.restrictSupportdefMathlib.RingTheory.MvPolynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $s$ be an element of $\wp (\FinsuppMACRoQ {x}{\Natural})$. Then $\operatorname{restrictSupport}$ applied to $R$ and $s$ is a submodule of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{supported}$ applied to $R$, $R$ and $s$.

MvPolynomial.restrictSupportIdealdefMathlib.RingTheory.MvPolynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $s$ be an element of $\wp (\FinsuppMACRoQ {x}{\Natural})$ such that $s$ is a upper set. Then $\operatorname{restrictSupportIdeal}$ applied to $R$, $s$ and $\mathrm{hs}$ is an ideal of the set of multivariate polynomials of $x$ and $R$.

MvPolynomial.restrictTotalDegreedefMathlib.RingTheory.MvPolynomial.Basic, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $m$ be a natural number. Then $\operatorname{restrictTotalDegree}$ applied to $x$, $R$ and $m$ is a submodule of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{restrictSupport}$ applied to $R$ and $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that the sum of $n$ and the function that maps $x_{2}$ and $e$ to $e$ is less than or equal to $m$.

Mathlib.RingTheory.MvPolynomial.FreeCommRing

FirstOrder.Ring.genericPolyMapdefMathlib.RingTheory.MvPolynomial.FreeCommRing, function or constant

Wording

the generic polynomial map of monoms and x2 (from the name)

English

Let $\mathrm{monoms}$ be a function from elements of $x$ to finite sets of $\FinsuppMACRoQ {x_{1}}{\Natural}$. Let $x_{2}$ be an element of $x$. Then the generic polynomial map of $\mathrm{monoms}$ and $x_{2}$ is a free commutative ring of $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{monoms} (i)}{x_{3}})}$ and $x_{1}$ defined as $\FinsetSum {\operatorname{attach} (\mathrm{monoms} (x_{2}))}{m}{(\operatorname{of} (\operatorname{inl} (\operatorname{mk} (x_{2} , m)))\times \FinsuppProd {m}{j}{n}{(\operatorname{of} (\operatorname{inr} (j))^ {n})})}$.

FirstOrder.Ring.mvPolynomialSupportLEEquivdefMathlib.RingTheory.MvPolynomial.FreeCommRing, function or constant

Wording

no wording

English

Let $\mathrm{monoms}$ be a function from elements of $x$ to finite sets of $\FinsuppMACRoQ {x_{1}}{\Natural}$. Then $\operatorname{mvPolynomialSupportLEEquiv}$ applied to $\mathrm{monoms}$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{\mathrm{forall} (x , \lambda i . \mathrm{Leq} (\operatorname{support} (p (i)), \mathrm{monoms} (i)))})}{(\mathrm{Elem} (\Sigma (\lambda i_{1} . \SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{monoms} (i_{1})}{x_{6}})}))\rightarrow R)}$.

Mathlib.RingTheory.MvPolynomial.Groebner

MonomialOrder.reducedefMathlib.RingTheory.MvPolynomial.Groebner, function or constant

Wording

no wording

English

Let $m$ be a monomial order of $x$ such that the leading coefficient of $m$ and $b$ is a unit. Let $f$ be a multivariate polynomial of $x$ and $R$. Then $\operatorname{reduce}$ applied to $m$, $\mathrm{hb}$ and $f$ is a multivariate polynomial of $x$ and $R$ defined as the difference between $f$ and the product of $\operatorname{monomial}$ applied to the difference between the degree of $m$ and $f$ and the degree of $m$ and $b$ and the product of the underlying value in the base of $\operatorname{inv}$ applied to the unit of $\mathrm{hb}$ and the leading coefficient of $m$ and $f$ and $b$.

MonomialOrder.subLTermdefMathlib.RingTheory.MvPolynomial.Groebner, function or constant

Wording

the difference term of m and f (from the name)

English

Let $m$ be a monomial order of $x$. Let $f$ be a multivariate polynomial of $x$ and $R$. Then the difference term of $m$ and $f$ is a multivariate polynomial of $x$ and $R$ defined as the difference between $f$ and $\operatorname{monomial}$ applied to the degree of $m$ and $f$ and the leading coefficient of $m$ and $f$.

Mathlib.RingTheory.MvPolynomial.Homogeneous

MvPolynomial.IsHomogeneousdefMathlib.RingTheory.MvPolynomial.Homogeneous, predicate

Wording

no wording

English

Let $x_{2}$ be a multivariate polynomial of $x$ and $R$. Let $n$ be a natural number. Then $\operatorname{IsHomogeneous}$ holds for $x_{2}$ and $n$, if $\operatorname{IsWeightedHomogeneous}$ holds for $1$, $x_{2}$ and $n$.

MvPolynomial.homogeneousComponentdefMathlib.RingTheory.MvPolynomial.Homogeneous, function or constant

Wording

the homogeneous component of n (from the name)

English

Let $n$ be a natural number. Then the homogeneous component of $n$ is a linear map of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the weighted homogeneous component of $1$ and $n$.

MvPolynomial.homogeneousSubmoduledefMathlib.RingTheory.MvPolynomial.Homogeneous, function or constant

Wording

the homogeneous submodule of n (from the name)

English

Let $x$ and $R$ be sets. Let $n$ be a natural number. Then the homogeneous submodule of $n$ is a submodule of $R$ and the set of multivariate polynomials of $x$ and $R$.

Mathlib.RingTheory.MvPolynomial.Ideal

MvPolynomial.idealOfVarsdefMathlib.RingTheory.MvPolynomial.Ideal, function or constant

Wording

the ideal spanned by all variables of x and R (from the docstring)

English

Let $x$ and $R$ be sets. Then the ideal spanned by all variables of $x$ and $R$ is an ideal of the set of multivariate polynomials of $x$ and $R$ defined as the span of the range of $\operatorname{X}$.

Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

MvPolynomial.sumSMulXdefMathlib.RingTheory.MvPolynomial.IrreducibleQuadratic, function or constant

Wording

the sum multiplicative (from the name)

English

The sum multiplicative is a linear map of $\FinsuppMACRoQ {n}{R}$ and the set of multivariate polynomials of $n$ and $R$ defined as the linear combination of $R$ and $\operatorname{X}$.

MvPolynomial.sumSMulXSMulYdefMathlib.RingTheory.MvPolynomial.IrreducibleQuadratic, function or constant

Wording

no wording

English

$\operatorname{sumSMulXSMulY}$ is a linear map of $\FinsuppMACRoQ {n}{R}$ and the set of multivariate polynomials of $\mathrm{Sum}$ applied to $n$ and $n$ and $R$ defined as the linear combination of $R$ and the function that maps $i$ to $\operatorname{X} (\operatorname{inl} (i))\times \operatorname{X} (\operatorname{inr} (i))$.

Mathlib.RingTheory.MvPolynomial.Localization

IsLocalization.Away.mvPolynomialQuotientEquivdefMathlib.RingTheory.MvPolynomial.Localization, function or constant

Wording

the multivariate polynomial quotient equivalence of S and r (from the name)

English

Let $S$ be a set. Let $r$ be an element of $R$. Then the multivariate polynomial quotient equivalence of $S$ and $r$ is an algebra isomorphism of the set of quotients of the set of multivariate polynomials of $\mathrm{Unit}$ and $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{C} (r)\times \operatorname{X} (\operatorname{unit})- 1$ and $S$.

Mathlib.RingTheory.MvPolynomial.MonomialOrder

MonomialOrder.MonicdefMathlib.RingTheory.MvPolynomial.MonomialOrder, predicate

Wording

f is monic with respect to m (from the name)

English

Let $m$ be a monomial order of $x$. Let $f$ be a multivariate polynomial of $x$ and $R$. Then $f$ is monic with respect to $m$, if the leading coefficient of $m$ and $f$ is equal to $1$.

MonomialOrder.degreedefMathlib.RingTheory.MvPolynomial.MonomialOrder, function or constant

Wording

the degree of m and f (from the docstring)

English

Let $m$ be a monomial order of $x$. Let $f$ be a multivariate polynomial of $x$ and $R$. Then the degree of $m$ and $f$ is an element of $\FinsuppMACRoQ {x}{\Natural}$ defined as $\operatorname{symm}$ applied to $\operatorname{toSyn}$ applied to $m$ and the supremum of the support of $f$ and $\operatorname{coe}$ applied to $\operatorname{toSyn}$ applied to $m$.

MonomialOrder.leadingCoeffdefMathlib.RingTheory.MvPolynomial.MonomialOrder, function or constant

Wording

the leading coefficient of m and f (from the docstring)

English

Let $m$ be a monomial order of $x$. Let $f$ be a multivariate polynomial of $x$ and $R$. Then the leading coefficient of $m$ and $f$ is an element of $R$ defined as $\operatorname{coeff}$ applied to $f$ and the degree of $m$ and $f$.

MonomialOrder.leadingTermdefMathlib.RingTheory.MvPolynomial.MonomialOrder, function or constant

Wording

the leading term of m and f (from the docstring)

English

Let $m$ be a monomial order of $x$. Let $f$ be a multivariate polynomial of $x$ and $R$. Then the leading term of $m$ and $f$ is a multivariate polynomial of $x$ and $R$ defined as $\operatorname{monomial}$ applied to the degree of $m$ and $f$ and the leading coefficient of $m$ and $f$.

MonomialOrder.sPolynomialdefMathlib.RingTheory.MvPolynomial.MonomialOrder, function or constant

Wording

the polynomial of f and g (from the name)

English

Let $m$ be a monomial order of $x$. Let $f$ and $g$ be multivariate polynomials of $x$ and $R$. Then the polynomial of $f$ and $g$ is a multivariate polynomial of $x$ and $R$ defined as the difference between the product of $\operatorname{monomial}$ applied to the difference between the degree of $m$ and $g$ and the degree of $m$ and $f$ and the leading coefficient of $m$ and $g$ and $f$ and the product of $\operatorname{monomial}$ applied to the difference between the degree of $m$ and $f$ and the degree of $m$ and $g$ and the leading coefficient of $m$ and $f$ and $g$.

MonomialOrder.withBotDegreedefMathlib.RingTheory.MvPolynomial.MonomialOrder, function or constant

Wording

the degree of m and f (from the docstring)

English

Let $m$ be a monomial order of $x$. Let $f$ be a multivariate polynomial of $x$ and $R$. Then the degree of $m$ and $f$ is an element of $\mathrm{WithBot}$ applied to $\FinsuppMACRoQ {x}{\Natural}$ defined as the map of $\operatorname{coe}$ applied to the inverse of $\operatorname{toSyn}$ applied to $m$ and the maximum of the forward image of the support of $f$ under $\operatorname{coe}$ applied to $\operatorname{toSyn}$ applied to $m$.

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Multiset.esymmdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $s$ be a multiset of $R$. Let $n$ be a natural number. Then $\operatorname{esymm}$ applied to $s$ and $n$ is an element of $R$ defined as the sum of the map of $\operatorname{prod}$ and the powerset cardinality of $n$ and $s$.

MvPolynomial.IsSymmetricdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, predicate

Wording

x2 is symmetric (from the name)

English

Let $x_{2}$ be a multivariate polynomial of $x$ and $R$. Then $x_{2}$ is symmetric, if for all permutations $e$ of $x$, $\operatorname{rename}$ applied to $\operatorname{coe}$ applied to $e$ and $x_{2}$ is equal to $x_{2}$.

MvPolynomial.esymmdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $n$ be an element of $\Natural$. Then $\operatorname{esymm}$ applied to $x$, $R$ and $n$ is a multivariate polynomial of $x$ and $R$ defined as $\FinsetSum {\operatorname{powersetCard} (n , \FinsetunivMACRoAC)}{t}{(\FinsetProd {t}{i}{\operatorname{X} (i)})}$.

MvPolynomial.esymmPartdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{3}$ be a partition of $n$. Then $\operatorname{esymmPart}$ applied to $x$, $R$ and $x_{3}$ is a multivariate polynomial of $x$ and $R$ defined as the product of the map of $\operatorname{esymm}$ applied to $x$ and $R$ and the set of parts of $x_{3}$.

MvPolynomial.hsymmdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $n$ be an element of $\Natural$. Then $\operatorname{hsymm}$ applied to $x$, $R$ and $n$ is a multivariate polynomial of $x$ and $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{s}{\operatorname{prod} (\operatorname{map} (\operatorname{X} , s))}$.

MvPolynomial.hsymmPartdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{4}$ be a partition of $n$. Then $\operatorname{hsymmPart}$ applied to $x$, $R$ and $x_{4}$ is a multivariate polynomial of $x$ and $R$ defined as the product of the map of $\operatorname{hsymm}$ applied to $x$ and $R$ and the set of parts of $x_{4}$.

MvPolynomial.msymmdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{4}$ be a partition of $n$. Then $\operatorname{msymm}$ applied to $x$, $R$ and $x_{4}$ is a multivariate polynomial of $x$ and $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{s}{\operatorname{prod} (\operatorname{map} (\operatorname{X} , s))}$.

MvPolynomial.psumdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $n$ be a natural number. Then $\operatorname{psum}$ applied to $x$, $R$ and $n$ is a multivariate polynomial of $x$ and $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(\operatorname{X} (i)^ {n})}$.

MvPolynomial.psumPartdefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $x_{3}$ be a partition of $n$. Then $\operatorname{psumPart}$ applied to $x$, $R$ and $x_{3}$ is a multivariate polynomial of $x$ and $R$ defined as the product of the map of $\operatorname{psum}$ applied to $x$ and $R$ and the set of parts of $x_{3}$.

MvPolynomial.renameSymmetricSubalgebradefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

no wording

English

Let $e$ be an element of $\EquivMACRoAE {x}{x_{1}}$. Then $\operatorname{renameSymmetricSubalgebra}$ applied to $e$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{symmetricSubalgebra} (x , R)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{symmetricSubalgebra} (x_{1} , R)}{x_{4}})}$.

MvPolynomial.symmetricSubalgebradefMathlib.RingTheory.MvPolynomial.Symmetric.Defs, function or constant

Wording

the symmetric subalgebra of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the symmetric subalgebra of $x$ and $R$ is a subalgebra of $R$ and the set of multivariate polynomials of $x$ and $R$.

Mathlib.RingTheory.MvPolynomial.Symmetric.Eval

MvPolynomial.symmetricSubalgebra.aevalMultisetdefMathlib.RingTheory.MvPolynomial.Symmetric.Eval, function or constant

Wording

the algebra evaluation multiset of m (from the name)

English

Let $x$ and $R$ be sets. Let $m$ be a multiset of $S$. Then the algebra evaluation multiset of $m$ is an algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{symmetricSubalgebra} (x , R)}{x_{5}})}$ and $S$.

MvPolynomial.symmetricSubalgebra.sumPolynomialdefMathlib.RingTheory.MvPolynomial.Symmetric.Eval, function or constant

Wording

the sum polynomial of x and p (from the name)

English

Let $x$ be a set. Let $p$ be a polynomial of $R$. Then the sum polynomial of $x$ and $p$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{symmetricSubalgebra} (x , R)}{x_{3}})}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{aeval} (\operatorname{X} (i), p)}$.

Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Fin.accumulatedefMathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem, function or constant

Wording

no wording

English

Let $n$ and $m$ be natural numbers. Then $\operatorname{accumulate}$ applied to $n$ and $m$ is an additive monoid homomorphism of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to natural numbers and the set of functions from elements of $\mathrm{Fin}$ applied to $m$ to natural numbers.

Fin.invAccumulatedefMathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem, function or constant

Wording

no wording

English

Let $n$ and $m$ be natural numbers. Let $s$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to natural numbers. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{invAccumulate}$ applied to $n$, $m$, $s$ and $i$ is a natural number defined as $\mathrm{dite} (\mathrm{Lt} (\operatorname{val} (i), m), \lambda \mathrm{hi} . s (\operatorname{mk} (\operatorname{val} (i), \mathrm{hi})), \lambda \mathrm{hi1} . 0)- \mathrm{dite} (\mathrm{Lt} (\operatorname{val} (i)+ 1 , m), \lambda \mathrm{hi2} . s (\operatorname{mk} (\operatorname{val} (i)+ 1 , \mathrm{hi2})), \lambda \mathrm{hi3} . 0)$.

MvPolynomial.esymmAlgEquivdefMathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets such that $\operatorname{card} (x)= n$. Then $\operatorname{esymmAlgEquiv}$ applied to $x$, $R$ and $\mathrm{hn}$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{symmetricSubalgebra} (x , R)}{x_{3}})}$.

MvPolynomial.esymmAlgHomdefMathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Let $n$ be an element of $\Natural$. Then $\operatorname{esymmAlgHom}$ applied to $x$, $R$ and $n$ is an algebra homomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{symmetricSubalgebra} (x , R)}{x_{3}})}$ defined as the algebra evaluation of the function that maps $i$ to $\operatorname{esymm}$ applied to $x$, $R$ and $\operatorname{val} (i)+ 1$.

MvPolynomial.esymmAlgHomMonomialdefMathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem, function or constant

Wording

the image of a monomial under x (from the docstring)

English

Let $x$ be a set. Let $t$ be an element of $\FinsuppMACRoQ {\mathrm{Fin} (n)}{\Natural}$. Let $r$ be an element of $R$. Then the image of a monomial under $x$ is a multivariate polynomial of $x$ and $R$ defined as $\operatorname{esymmAlgHom}$ applied to $x$, $R$, $n$ and $\operatorname{monomial}$ applied to $t$ and $r$.

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

MvPolynomial.IsWeightedHomogeneousdefMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, predicate

Wording

no wording

English

Let $w$ be a function from elements of $x_{1}$ to elements of $M$. Let $x_{3}$ be a multivariate polynomial of $x_{1}$ and $R$. Let $m$ be an element of $M$. Then $\operatorname{IsWeightedHomogeneous}$ holds for $w$, $x_{3}$ and $m$, if for all elements $d$ of $\FinsuppMACRoQ {x_{1}}{\Natural}$, if $\operatorname{coeff} (x_{3} , d)\neq 0$, then $\EqtMACRoH {\operatorname{weight} (w , d)}{m}$.

MvPolynomial.NonTorsionWeightdefMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, predicate

Wording

no wording

English

Let $w$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{NonTorsionWeight}$ holds for $w$, if for all natural numbers $n$, for all elements $x_{2}$ of $x$, if $\EqtMACRoH {\HSMulhSMulMACRoAL {n}{w (x_{2})}}{0}$, then $n = 0$.

MvPolynomial.decompose'defMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, function or constant

Wording

no wording

English

Let $R$ be a set. Let $w$ be a function from elements of $x_{1}$ to elements of $M$. Let $x_{4}$ be a multivariate polynomial of $x_{1}$ and $R$. Then $\operatorname{decompose'}$ applied to $R$, $w$ and $x_{4}$ is a direct sum of $M$ and the function that maps $i$ to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{weightedHomogeneousSubmodule} (w , i)}{x_{5}})}$ defined as $\operatorname{mk}$ applied to the function that maps $i_{2}$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{weightedHomogeneousSubmodule} (w , i_{2})}{x_{7}})}$, the forward image of the support of $x_{4}$ under $\operatorname{coe}$ applied to $\operatorname{weight}$ applied to $w$ and the function that maps $m_{1}$ to $\operatorname{weightedHomogeneousComponent}$ applied to $w$, $m_{1}$ and $x_{4}$.

MvPolynomial.weightedHomogeneousComponentdefMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, function or constant

Wording

the weighted homogeneous component of w and n (from the name)

English

Let $w$ be a function from elements of $x_{1}$ to elements of $M$. Let $n$ be an element of $M$. Then the weighted homogeneous component of $w$ and $n$ is a linear map of the set of multivariate polynomials of $x_{1}$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $R$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $R$ and the composition of the subtype of $\operatorname{supported}$ applied to $R$, $R$ and $\operatorname{ofPred}$ applied to the function that maps $d$ to $\EqtMACRoH {\operatorname{weight} (w , d)}{n}$ and the composition of $\operatorname{restrictDom}$ applied to $R$, $R$ and $\operatorname{ofPred}$ applied to the function that maps $d_{1}$ to $\EqtMACRoH {\operatorname{weight} (w , d_{1})}{n}$ and $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$.

MvPolynomial.weightedHomogeneousSubmoduledefMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, function or constant

Wording

the weighted homogeneous submodule of w and m (from the name)

English

Let $R$ be a set. Let $w$ be a function from elements of $x_{1}$ to elements of $M$. Let $m$ be an element of $M$. Then the weighted homogeneous submodule of $w$ and $m$ is a submodule of $R$ and the set of multivariate polynomials of $x_{1}$ and $R$.

MvPolynomial.weightedTotalDegreedefMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, function or constant

Wording

the weighted total degree of w and p (from the name)

English

Let $w$ be a function from elements of $x_{1}$ to elements of $M$. Let $p$ be a multivariate polynomial of $x_{1}$ and $R$. Then the weighted total degree of $w$ and $p$ is an element of $M$ defined as the supremum of the support of $p$ and the function that maps $s$ to $\operatorname{weight}$ applied to $w$ and $s$.

MvPolynomial.weightedTotalDegree'defMathlib.RingTheory.MvPolynomial.WeightedHomogeneous, function or constant

Wording

the weighted total degree of w and p (from the docstring)

English

Let $w$ be a function from elements of $x_{1}$ to elements of $M$. Let $p$ be a multivariate polynomial of $x_{1}$ and $R$. Then the weighted total degree of $w$ and $p$ is an element of $\mathrm{WithBot}$ applied to $M$ defined as the supremum of the support of $p$ and the function that maps $s$ to $\operatorname{some}$ applied to $\operatorname{weight}$ applied to $w$ and $s$.

Mathlib.RingTheory.MvPowerSeries.Basic

MvPolynomial.coeToMvPowerSeries.algHomdefMathlib.RingTheory.MvPowerSeries.Basic, function or constant

Wording

the algebra homomorphism of A (from the name)

English

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

MvPolynomial.coeToMvPowerSeries.ringHomdefMathlib.RingTheory.MvPowerSeries.Basic, function or constant

Wording

the ring homomorphism (from the name)

English

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

MvPolynomial.toMvPowerSeriesdefMathlib.RingTheory.MvPowerSeries.Basic, function or constant

Wording

the multivariate power series of x2 (from the name)

English

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

MvPowerSeriesdefMathlib.RingTheory.MvPowerSeries.Basic, type

Wording

multivariate power series of x and R (from the name)

English

Let $x$ and $R$ be sets. Then a multivariate power series of $x$ and $R$ is an element of the function that maps $x$ and $R$ to the set of functions from elements of $\FinsuppMACRoQ {x}{\Natural}$ to elements of $R$.

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

Wording

no wording

English

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

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

Wording

no wording

English

Let $s$ be an element of $x$. Then there is a multivariate power series of $x$ and $R$. Proof. Let $s$ be arbitrary. By s. By 1. By Finsupp__single. By 1. By MvPowerSeries__monomial__app.

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

Wording

the coefficient of n (from the name)

English

Let $n$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then the coefficient of $n$ is a linear map of the set of multivariate power series of $x$ and $R$ and $R$ defined as the projection of $n$.

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

Wording

the constant coefficient (from the docstring)

English

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

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

Wording

the map of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a ring homomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $S$.

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

Wording

the map algebra homomorphism of x6 (from the name)

English

Let $x_{6}$ be an algebra homomorphism of $A$ and $B$. Then the map algebra homomorphism of $x_{6}$ is an algebra homomorphism of the set of multivariate power series of $x$ and $A$ and the set of multivariate power series of $x$ and $B$.

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

Wording

the monomial of n (from the name)

English

Let $n$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then the monomial of $n$ is a linear map of $R$ and the set of multivariate power series of $x$ and $R$ defined as $\operatorname{single}$ applied to $R$, the function that maps $x_{2}$ to $R$ and $n$.

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

Wording

the subring of p and T (from the name)

English

Let $p$ be a multivariate power series of $x$ and $R$. Let $T$ be a subring of $R$ such that for all elements $n$ of $\FinsuppMACRoQ {x}{\Natural}$, $\MembershipmemMACRoT {T}{\operatorname{coeff} (n , p)}$. Then the subring of $p$ and $T$ is a multivariate power series of $x$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$ defined as the function that maps $n$ to $\operatorname{coeff}$ applied to $n$ and $p$.

Mathlib.RingTheory.MvPowerSeries.Derivative

MvPowerSeries.pderivdefMathlib.RingTheory.MvPowerSeries.Derivative, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\operatorname{pderiv}$ applied to $i$ is a derivation of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$.

MvPowerSeries.pderivFundefMathlib.RingTheory.MvPowerSeries.Derivative, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Let $f$ be a multivariate power series of $x$ and $R$. Then there is a multivariate power series of $x$ and $R$. Proof. Let $i$ be arbitrary. Let $f$ be arbitrary. Let $d$ be arbitrary. By d. By i. By 1. By Finsupp__single. By plus. By f. By MvPowerSeries__coeff__app. By i. By d. By 1. By plus. By times.

Mathlib.RingTheory.MvPowerSeries.Equiv

MvPowerSeries.finSuccEquivdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the finite successor equivalence of R and n (from the name)

English

Let $R$ be a set. Let $n$ be a natural number. Then the finite successor equivalence of $R$ and $n$ is an algebra isomorphism of the set of multivariate power series of $\mathrm{Fin}$ applied to $n + 1$ and $R$ and the set of power series of the set of multivariate power series of $\mathrm{Fin}$ applied to $n$ and $R$ defined as the composition of $\operatorname{renameEquiv}$ applied to $R$ and the finite successor equivalence of $n$ and the left option equivalence of $\mathrm{Fin}$ applied to $n$ and $R$.

MvPowerSeries.isEmptyEquivdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

no wording

English

Let $x$ and $R$ be sets. Then $\operatorname{isEmptyEquiv}$ applied to $x$ and $R$ is an algebra isomorphism of the set of multivariate power series of $x$ and $R$ and $R$.

MvPowerSeries.optionEquivLeftdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the left option equivalence of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the left option equivalence of $x$ and $R$ is an algebra isomorphism of the set of multivariate power series of $\mathrm{Option}$ applied to $x$ and $R$ and the set of power series of the set of multivariate power series of $x$ and $R$.

MvPowerSeries.toAdicCompletiondefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the adic completion of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the adic completion of $x$ and $R$ is an algebra homomorphism of the set of multivariate power series of $x$ and $R$ and the set of adic completions of the ideal spanned by all variables of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$.

MvPowerSeries.toAdicCompletionAlgEquivdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the adic completion algebra isomorphism of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the adic completion algebra isomorphism of $x$ and $R$ is an algebra isomorphism of the set of multivariate power series of $x$ and $R$ and the set of adic completions of the ideal spanned by all variables of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$.

MvPowerSeries.toAdicCompletionInvdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the adic completion inverse of f (from the name)

English

Let $x$ and $R$ be sets. Let $f$ be an adic completion of the ideal spanned by all variables of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$. Then the adic completion inverse of $f$ is a multivariate power series of $x$ and $R$ defined as the function that maps $x_{2}$ to $\operatorname{coeff}$ applied to $\operatorname{out}$ applied to $\operatorname{degree} (x_{2})+ 1$ and $x_{2}$.

MvPowerSeries.truncTotalAlgHomdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the truncation total algebra homomorphism of n (from the name)

English

Let $x$ and $R$ be sets. Let $n$ be a natural number. Then the truncation total algebra homomorphism of $n$ is an algebra homomorphism of the set of multivariate power series of $x$ and $R$ and the set of quotients of the set of multivariate polynomials of $x$ and $R$ and the exponentiation of the ideal spanned by all variables of $x$ and $R$ to $n$.

PowerSeries.toMvPowerSeriesdefMathlib.RingTheory.MvPowerSeries.Equiv, function or constant

Wording

the multivariate power series of i (from the name)

English

Let $i$ be an element of $x$. Then the multivariate power series of $i$ is an algebra homomorphism of the set of power series of $R$ and the set of multivariate power series of $x$ and $R$ defined as $\operatorname{rename}$ applied to the function that maps $x_{2}$ to $i$.

Mathlib.RingTheory.MvPowerSeries.Evaluation

MvPowerSeries.HasEvalstructureMathlib.RingTheory.MvPowerSeries.Evaluation, predicate

Wording

a has evaluations (from the name)

English

Let $a$ be a function from elements of $x$ to elements of $S$. Then we can say that $a$ has evaluations.

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

Wording

the algebra evaluation of ha (from the name)

English

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

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

Wording

the evaluation of a and f (from the name)

English

Let $x_{5}$ be a ring homomorphism of $R$ and $S$. Let $a$ be a function from elements of $x$ to elements of $S$. Let $f$ be a multivariate power series of $x$ and $R$. Then the evaluation of $a$ and $f$ is an element of $S$ defined as $\mathrm{dite}$ applied to the proposition that there exists a multivariate polynomial $p$ of $x$ and $R$, such that the multivariate power series of $p$ is equal to $f$, the function that maps $H$ to the evaluation of $a$ and $\operatorname{choose}$ applied to $H$ and the function that maps $H_{1}$ to $\operatorname{extend}$ applied to $\mathrm{MvPolynomial\_\_toMvPowerSeries\_isDenseInducing}$, $\mathrm{MvPolynomial\_\_eval\_u2082\_}$ applied to $a$ and $f$.

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

Wording

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

English

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

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

Wording

no wording

English

$\operatorname{hasEvalIdeal}$ is an ideal of the set of functions from elements of $x$ to elements of $S$.

Mathlib.RingTheory.MvPowerSeries.Expand

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

Wording

the expand of p and hp (from the name)

English

Let $p$ be a natural number such that $p \neq 0$. Then the expand of $p$ and $\mathrm{hp}$ is an algebra homomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$ defined as the substitution algebra homomorphism of $\mathrm{MvPowerSeries\_\_HasSubst\_\_X\_pow}$ applied to $\mathrm{hp}$.

Mathlib.RingTheory.MvPowerSeries.GaussNorm

MvPowerSeries.AchievesGaussNormdefMathlib.RingTheory.MvPowerSeries.GaussNorm, predicate

Wording

no wording

English

Let $v$ be a function from elements of $R$ to real numbers. Let $c$ be a function from elements of $x$ to real numbers. Let $f$ be a multivariate power series of $x$ and $R$. Let $i$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{AchievesGaussNorm}$ holds for $v$, $c$, $f$ and $i$, if $v (\operatorname{coeff} (i , f))\times \FinsuppProd {i}{x_{2}}{x_{3}}{(c (x_{2})^ {x_{3}})}$ is equal to the Gauss norm of $c$ and $f$.

MvPowerSeries.HasGaussNormdefMathlib.RingTheory.MvPowerSeries.GaussNorm, predicate

Wording

no wording

English

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

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

Wording

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

English

Let $v$ be a function from elements of $R$ to real numbers. Let $c$ be a function from elements of $x$ to real numbers. Let $f$ be a multivariate power series of $x$ and $R$. Then the Gauss norm of $c$ and $f$ is a real number defined as the supremum of the function that maps $t$ to $v (\operatorname{coeff} (t , f))\times \FinsuppProd {t}{x_{2}}{x_{3}}{(c (x_{2})^ {x_{3}})}$.

Mathlib.RingTheory.MvPowerSeries.Inverse

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

Wording

the inverse of x2 (from the docstring)

English

Let $x_{2}$ be a multivariate power series of $x$ and $k$. Then the inverse of $x_{2}$ is a multivariate power series of $x$ and $k$ defined as $\operatorname{aux}$ applied to $\operatorname{inv}$ applied to $\operatorname{constantCoeff}$ applied to $x_{2}$ and $x_{2}$.

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

Wording

the inverse of x2 and u (from the name)

English

Let $x_{2}$ be a multivariate power series of $x$ and $R$. Let $u$ be a unit of $R$. Then the inverse of $x_{2}$ and $u$ is a multivariate power series of $x$ and $R$ defined as $\operatorname{aux}$ applied to the underlying value in the base of $\operatorname{inv}$ applied to $u$ and $x_{2}$.

Mathlib.RingTheory.MvPowerSeries.LexOrder

MvPowerSeries.lexOrderdefMathlib.RingTheory.MvPowerSeries.LexOrder, function or constant

Wording

the lexicographic order of x3 (from the name)

English

Let $x_{3}$ be a multivariate power series of $x$ and $R$. Then the lexicographic order of $x_{3}$ is an element of $\mathrm{WithTop}$ applied to $\mathrm{Lex}$ applied to $\FinsuppMACRoQ {x}{\Natural}$.

Mathlib.RingTheory.MvPowerSeries.LinearTopology

MvPowerSeries.LinearTopology.basisdefMathlib.RingTheory.MvPowerSeries.LinearTopology, function or constant

Wording

the basis of Jd (from the name)

English

Let $x$ and $R$ be sets. Let $\mathrm{Jd}$ be an element of $\mathrm{Prod}$ applied to $\mathrm{TwoSidedIdeal}$ applied to $R$ and $\FinsuppMACRoQ {x}{\Natural}$. Then the basis of $\mathrm{Jd}$ is an element of $\mathrm{TwoSidedIdeal}$ applied to the set of multivariate power series of $x$ and $R$.

Mathlib.RingTheory.MvPowerSeries.Order

MvPowerSeries.IsHomogeneousdefMathlib.RingTheory.MvPowerSeries.Order, predicate

Wording

no wording

English

Let $f$ be a multivariate power series of $x$ and $R$. Let $p$ be a natural number. Then $\operatorname{IsHomogeneous}$ holds for $f$ and $p$, if $\operatorname{IsWeightedHomogeneous}$ holds for $1$, $f$ and $p$.

MvPowerSeries.IsWeightedHomogeneousdefMathlib.RingTheory.MvPowerSeries.Order, predicate

Wording

no wording

English

Let $w$ be a function from elements of $x$ to natural numbers. Let $f$ be a multivariate power series of $x$ and $R$. Let $p$ be a natural number. Then $\operatorname{IsWeightedHomogeneous}$ holds for $w$, $f$ and $p$, if for all elements $d$ of $\FinsuppMACRoQ {x}{\Natural}$, if $\operatorname{coeff} (d , f)\neq 0$, then $\operatorname{weight} (w , d)= p$.

MvPowerSeries.homogeneousComponentdefMathlib.RingTheory.MvPowerSeries.Order, function or constant

Wording

the homogeneous component of p (from the name)

English

Let $p$ be a natural number. Then the homogeneous component of $p$ is a linear map of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$ defined as the weighted homogeneous component of $1$ and $p$.

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

Wording

the order of f (from the docstring)

English

Let $f$ be a multivariate power series of $x$ and $R$. Then the order of $f$ is a natural number defined as the weighted order of the function that maps $x_{2}$ to $1$ and $f$.

MvPowerSeries.weightedHomogeneousComponentdefMathlib.RingTheory.MvPowerSeries.Order, function or constant

Wording

the weighted homogeneous component of w and p (from the name)

English

Let $w$ be a function from elements of $x$ to natural numbers. Let $p$ be a natural number. Then the weighted homogeneous component of $w$ and $p$ is a linear map of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$.

MvPowerSeries.weightedOrderdefMathlib.RingTheory.MvPowerSeries.Order, function or constant

Wording

the weighted order of w and f (from the name)

English

Let $w$ be a function from elements of $x$ to natural numbers. Let $f$ be a multivariate power series of $x$ and $R$. Then the weighted order of $w$ and $f$ is a natural number.

Mathlib.RingTheory.MvPowerSeries.Rename

MvPowerSeries.killCompldefMathlib.RingTheory.MvPowerSeries.Rename, function or constant

Wording

no wording

English

Let $e$ be an embedding of $x$ and $x_{1}$. Then $\operatorname{killCompl}$ applied to $e$ is an algebra homomorphism of the set of multivariate power series of $x_{1}$ and $R$ and the set of multivariate power series of $x$ and $R$.

MvPowerSeries.renamedefMathlib.RingTheory.MvPowerSeries.Rename, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{rename}$ applied to $f$ is an algebra homomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x_{1}$ and $R$.

MvPowerSeries.renameEquivdefMathlib.RingTheory.MvPowerSeries.Rename, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{renameEquiv}$ applied to $R$ and $e$ is an algebra isomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x_{1}$ and $R$.

Mathlib.RingTheory.MvPowerSeries.Restricted

MvPolynomial.toRestricteddefMathlib.RingTheory.MvPowerSeries.Restricted, function or constant

Wording

no wording

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Then $\operatorname{toRestricted}$ applied to $c$ is a ring homomorphism of the set of multivariate polynomials of $x_{1}$ and $R$ and $\operatorname{Restricted}$ applied to $R$ and $c$ defined as $\operatorname{codRestrict}$ applied to the ring homomorphism, the subring of $c$ and the function that maps $p$ to $\operatorname{isRestricted}$ applied to $c$ and $p$.

MvPowerSeries.IsRestricteddefMathlib.RingTheory.MvPowerSeries.Restricted, predicate

Wording

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

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Let $f$ be a multivariate power series of $x_{1}$ and $R$. Then $f$ is restricted with respect to $c$, if $\operatorname{Tendsto}$ holds for the function that maps $t$ to the product of the norm of $\operatorname{coeff}$ applied to $t$ and $f$ and $\FinsuppProd {t}{x_{2}}{x_{3}}{(c (x_{2})^ {x_{3}})}$, the cofinite filter and the neighbourhood filter of $0$.

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

Wording

the additive subgroup of c (from the name)

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Then the additive subgroup of $c$ is an additive subgroup of the set of multivariate power series of $x_{1}$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that $f$ is restricted with respect to $c$ and the function that maps $x_{2}$, $x_{3}$, $a$ and $b$ to $\operatorname{add}$ applied to $a$ and $b$ and $\mathrm{MvPowerSeries\_\_isRestricted\_zero}$ applied to $c$ and the function that maps $x_{4}$ to $\operatorname{neg}$.

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

Wording

the subring of c (from the name)

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Then the subring of $c$ is a subring of the set of multivariate power series of $x_{1}$ and $R$.

MvPowerSeries.RestricteddefMathlib.RingTheory.MvPowerSeries.Restricted, type

Wording

no wording

English

Let $R$ be a set. Let $c$ be a function from elements of $x_{1}$ to elements of $\Real$. Then an element of $\operatorname{Restricted}$ applied to $R$ and $c$ is an element of the function that maps $R$ and $c$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{subring} (c)}{x_{2}})}$.

MvPowerSeries.Restricted.CdefMathlib.RingTheory.MvPowerSeries.Restricted, function or constant

Wording

no wording

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Then $\operatorname{C}$ applied to $c$ is a ring homomorphism of $R$ and $\operatorname{Restricted}$ applied to $R$ and $c$ defined as $\operatorname{codRestrict}$ applied to $\operatorname{C}$, the subring of $c$ and $\mathrm{MvPowerSeries\_\_isRestricted\_C}$ applied to $c$.

MvPowerSeries.Restricted.XdefMathlib.RingTheory.MvPowerSeries.Restricted, function or constant

Wording

no wording

English

Let $R$ be a set. Let $c$ be a function from elements of $x_{1}$ to real numbers. Let $s$ be an element of $x_{1}$. Then $\operatorname{X}$ applied to $R$, $c$ and $s$ is an element of $\operatorname{Restricted}$ applied to $R$ and $c$ defined as $\operatorname{X}$ applied to $s$.

MvPowerSeries.Restricted.mapdefMathlib.RingTheory.MvPowerSeries.Restricted, function or constant

Wording

the map of c and h2 (from the name)

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Assume that for all elements $x_{4}$ of $R$, the norm of $x_{3}$ applied to $x_{4}$ is less than or equal to the product of $K$ and the norm of $x_{4}$. Then the map of $c$ and $h_{2}$ is a ring homomorphism of $\operatorname{Restricted}$ applied to $R$ and $c$ and $\operatorname{Restricted}$ applied to $S$ and $c$.

MvPowerSeries.Restricted.mapAdditivedefMathlib.RingTheory.MvPowerSeries.Restricted, function or constant

Wording

no wording

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Let $x_{3}$ be an additive monoid homomorphism of $S$ and $R$ such that for all elements $x_{4}$ of $S$, the norm of $x_{3}$ applied to $x_{4}$ is less than or equal to the product of $K$ and the norm of $x_{4}$. Then $\operatorname{mapAdditive}$ applied to $c$, $x_{3}$ and $\mathrm{hK}$ is an additive monoid homomorphism of $\operatorname{Restricted}$ applied to $S$ and $c$ and $\operatorname{Restricted}$ applied to $R$ and $c$.

MvPowerSeries.Restricted.monomialdefMathlib.RingTheory.MvPowerSeries.Restricted, function or constant

Wording

the monomial of n and a (from the name)

English

Let $c$ be a function from elements of $x_{1}$ to real numbers. Let $n$ be an element of $\FinsuppMACRoQ {x_{1}}{\Natural}$. Let $a$ be an element of $R$. Then the monomial of $n$ and $a$ is an element of $\operatorname{Restricted}$ applied to $R$ and $c$ defined as $\operatorname{monomial}$ applied to $n$ and $a$.

Mathlib.RingTheory.MvPowerSeries.Substitution

MvPowerSeries.HasSubststructureMathlib.RingTheory.MvPowerSeries.Substitution, predicate

Wording

a has substitutions (from the name)

English

Let $a$ be a function from elements of $x$ to multivariate power series of $x_{1}$ and $S$. Then we can say that $a$ has substitutions.

MvPowerSeries.hasSubstIdealdefMathlib.RingTheory.MvPowerSeries.Substitution, function or constant

Wording

no wording

English

$\operatorname{hasSubstIdeal}$ is an ideal of the set of functions from elements of $x$ to multivariate power series of $x_{1}$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the proposition that $\operatorname{HasSubst}$ and the function that maps $x_{3}$ and $x_{4}$ to $\operatorname{add}$ and $\operatorname{zero}$ and $\mathrm{MvPowerSeries\_\_HasSubst\_\_mul\_left}$.

MvPowerSeries.rescaledefMathlib.RingTheory.MvPowerSeries.Substitution, function or constant

Wording

no wording

English

Let $a$ be a function from elements of $x$ to elements of $R$. Then $\operatorname{rescale}$ applied to $a$ is a ring homomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$.

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

Wording

no wording

English

Let $a$ be a function from elements of $x$ to elements of $R$. Then $\operatorname{rescaleAlgHom}$ applied to $a$ is an algebra homomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$ defined as the substitution algebra homomorphism of $\mathrm{MvPowerSeries\_\_HasSubst\_\_smul\_X}$ applied to $a$.

MvPowerSeries.rescaleMonoidHomdefMathlib.RingTheory.MvPowerSeries.Substitution, function or constant

Wording

no wording

English

$\operatorname{rescaleMonoidHom}$ is a monoid homomorphism of the set of functions from elements of $x$ to elements of $R$ and the set of ring homomorphisms of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x$ and $R$.

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

Wording

the substitution of a and f (from the name)

English

Let $a$ be a function from elements of $x$ to multivariate power series of $x_{2}$ and $S$. Let $f$ be a multivariate power series of $x$ and $R$. Then the substitution of $a$ and $f$ is a multivariate power series of $x_{2}$ and $S$ defined as the evaluation of $a$ and $f$.

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

Wording

the substitution algebra homomorphism of ha (from the name)

English

Assume that $a$ has substitutions. Then the substitution algebra homomorphism of $\mathrm{ha}$ is an algebra homomorphism of the set of multivariate power series of $x$ and $R$ and the set of multivariate power series of $x_{2}$ and $S$.

Mathlib.RingTheory.MvPowerSeries.Trunc

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

Wording

the truncation of R and n (from the name)

English

Let $R$ be a set. Let $n$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then the truncation of $R$ and $n$ is a linear map of the set of multivariate power series of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the truncation finite set of $R$ and $\FinsetIioMACRoAK {n}$.

MvPowerSeries.trunc'defMathlib.RingTheory.MvPowerSeries.Trunc, function or constant

Wording

the truncation of R and n (from the name)

English

MvPowerSeries.truncFinsetdefMathlib.RingTheory.MvPowerSeries.Trunc, function or constant

Wording

the truncation finite set of R and s (from the name)

English

Let $R$ be a set. Let $s$ be a finite set of $\FinsuppMACRoQ {x}{\Natural}$. Then the truncation finite set of $R$ and $s$ is a linear map of the set of multivariate power series of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$.

MvPowerSeries.truncTotaldefMathlib.RingTheory.MvPowerSeries.Trunc, function or constant

Wording

the truncation of n (from the docstring)

English

Let $n$ be a natural number. Then the truncation of $n$ is a linear map of the set of multivariate power series of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the truncation finite set of $R$ and the finite set of $\mathrm{Finsupp\_\_finite\_of\_degree\_lt}$ applied to $n$.

Mathlib.RingTheory.Nilpotent.Defs

IsRadicaldefMathlib.RingTheory.Nilpotent.Defs, predicate

Wording

y is a radical (from the name)

English

Let $y$ be an element of $R$. Then $y$ is a radical, if for all natural numbers $n$, for all elements $x_{2}$ of $R$, if $y$ divides $x_{2} ^ {n}$, then $y$ divides $x_{2}$.

nilpotencyClassdefMathlib.RingTheory.Nilpotent.Defs, function or constant

Wording

the nilpotency class of x (from the name)

English

Let $x$ be an element of $R$. Then the nilpotency class of $x$ is a natural number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $k$ to $\EqtMACRoH {(x ^ {k})}{0}$.

Mathlib.RingTheory.Nilpotent.Exp

IsNilpotent.expdefMathlib.RingTheory.Nilpotent.Exp, function or constant

Wording

the exponential of a (from the name)

English

Let $a$ be an element of $A$. Then the exponential of $a$ is an element of $A$ defined as $\FinsetSum {\FinsetrangeMACRoN {\mathrm{nilpotencyClass} (a)}}{i}{(\HSMulhSMulMACRoAL {\operatorname{inv} (i !)}{(a ^ {i})})}$.

Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Algebra.IsGeometricallyReducedclassMathlib.RingTheory.Nilpotent.GeometricallyReduced, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Nilpotent.Lemmas

nilradicaldefMathlib.RingTheory.Nilpotent.Lemmas, function or constant

Wording

the nilradical of R (from the docstring)

English

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

Mathlib.RingTheory.NoetherNormalization

NoetherNormalization.T1defMathlib.RingTheory.NoetherNormalization, function or constant

Wording

no wording

English

Let $f$ be a multivariate polynomial of $\mathrm{Fin}$ applied to $n + 1$ and $k$. Let $c$ be an element of $k$. Then $\operatorname{T1}$ applied to $f$ and $c$ is an algebra homomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n + 1$ and $k$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n + 1$ and $k$ defined as the algebra evaluation of the function that maps $i$ to $\iteMACRoG {(\EqtMACRoH {i}{0})}{\operatorname{X} (0)}{(\operatorname{X} (i)+ \HSMulhSMulMACRoAL {c}{(\operatorname{X} (0)^ {(2 + \operatorname{totalDegree} (f))^ {\operatorname{val} (i)}})})}$.

NoetherNormalization.varChangedefMathlib.RingTheory.NoetherNormalization, function or constant

Wording

the variable change of f (from the name)

English

Let $f$ be a multivariate polynomial of $\mathrm{Fin}$ applied to $n + 1$ and $k$. Then the variable change of $f$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n + 1$ and $k$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n + 1$ and $k$.

Mathlib.RingTheory.Noetherian.Defs

IsNoetherianclassMathlib.RingTheory.Noetherian.Defs, predicate

Wording

no wording

English

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

IsNoetherianRingdefMathlib.RingTheory.Noetherian.Defs, predicate

Wording

R is a Noetherian ring (from the name)

English

Let $R$ be a set. Then $R$ is a Noetherian ring, if $\mathrm{IsNoetherian}$ holds for $R$ and $R$.

Mathlib.RingTheory.Noetherian.Orzech

IsNoetherian.equivPUnitOfProdInjectivedefMathlib.RingTheory.Noetherian.Orzech, function or constant

Wording

the equivalence unit of f and i (from the name)

English

Let $f$ be a linear map of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence unit of $f$ and $i$ is a linear equivalence of $N$ and $\mathrm{PUnit}$ defined as the linear equivalence of $N$ and $\mathrm{PUnit}$.

Mathlib.RingTheory.NonUnitalSubring.Basic

NonUnitalRingHom.eqLocusdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

no wording

English

Let $f$ and $g$ be non unital ring homomorphisms of $R$ and $S$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is a non unital subring of $R$.

NonUnitalRingHom.rangedefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Then the range of $f$ is a non unital subring of $S$.

NonUnitalRingHom.rangeRestrictdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

no wording

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a non unital ring homomorphism of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

NonUnitalSubring.centerdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the center of R (from the docstring)

English

Let $R$ be a set. Then the center of $R$ is a non unital subring of $R$ defined as $\operatorname{mk}$ applied to the center of $R$ and the function that maps $x_{1}$ to $\mathrm{Set\_\_neg\_mem\_center}$.

NonUnitalSubring.centerCongrdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the center congruence of e (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then the center congruence of $e$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (R)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (S)}{x_{3}})}$ defined as the center congruence of $e$.

NonUnitalSubring.centerToMulOppositedefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the center (from the docstring)

English

The center is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (R)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{MulOpposite} (R))}{x_{2}})}$ defined as the center.

NonUnitalSubring.centralizerdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the centralizer of s (from the docstring)

English

Let $s$ be an element of $\wp R$. Then the centralizer of $s$ is a non unital subring of $R$.

NonUnitalSubring.closuredefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the closure of s (from the name)

English

Let $s$ be an element of $\wp R$. Then the closure of $s$ is a non unital subring of $R$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Leq} (s , S)$.

NonUnitalSubring.comapdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the preimage of f and s (from the docstring)

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Let $s$ be a non unital subring of $S$. Then the preimage of $f$ and $s$ is a non unital subring of $R$.

NonUnitalSubring.equivMapOfInjectivedefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the equivalence map of s and f (from the name)

English

Let $s$ be a non unital subring of $R$. Let $f$ be a non unital ring homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $s$ and $f$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , s)}{x_{3}})}$.

NonUnitalSubring.gidefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

no wording

English

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

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

Wording

the map of f and s (from the name)

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Let $s$ be a non unital subring of $R$. Then the map of $f$ and $s$ is a non unital subring of $S$.

NonUnitalSubring.proddefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a non unital subring of $R$. Let $t$ be a non unital subring of $S$. Then the product of $s$ and $t$ is a non unital subring of $\mathrm{Prod}$ applied to $R$ and $S$.

NonUnitalSubring.prodEquivdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the product equivalence of s and t (from the name)

English

Let $s$ be a non unital subring of $R$. Let $t$ be a non unital subring of $S$. Then the product equivalence of $s$ and $t$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{prod} (s , t)}{x_{2}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {t}{x_{4}})}$.

NonUnitalSubring.topEquivdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the top equivalence (from the name)

English

The top equivalence is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $R$ defined as the top equivalence.

RingEquiv.nonUnitalSubringCongrdefMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the non unital subring congruence of h (from the name)

English

Assume that $\EqtMACRoH {s}{t}$. Then the non unital subring congruence of $h$ is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$.

RingEquiv.ofLeftInverse'defMathlib.RingTheory.NonUnitalSubring.Basic, function or constant

Wording

the ring isomorphism of h (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the ring isomorphism of $h$ is a ring isomorphism of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

Mathlib.RingTheory.NonUnitalSubring.Defs

NonUnitalSubringstructureMathlib.RingTheory.NonUnitalSubring.Defs, type

Wording

non unital subring of R (from the name)

English

Let $R$ be a set. Then the non unital subrings of $R$ are a basic type.

NonUnitalSubring.copydefMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

the copy of S and s (from the name)

English

Let $S$ be a non unital subring of $R$. Let $s$ be an element of $\wp R$ such that $\EqtMACRoH {s}{S}$. Then the copy of $S$ and $s$ is a non unital subring of $R$.

NonUnitalSubring.inclusiondefMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $S \leq T$. Then the inclusion of $h$ is a non unital ring homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$.

NonUnitalSubring.mk'defMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp R$. Let $\mathrm{sm}$ be a subsemigroup of $R$. Let $\mathrm{sa}$ be an additive subgroup of $R$. Assume that $\EqtMACRoH {\mathrm{sm}}{s}$. Assume that $\EqtMACRoH {\mathrm{sa}}{s}$. Then $\operatorname{mk'}$ applied to $s$, $\mathrm{sm}$, $\mathrm{sa}$, $\mathrm{hm}$ and $\mathrm{ha}$ is a non unital subring of $R$.

NonUnitalSubring.ofClassdefMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

the non unital subring of s (from the name)

English

Let $s$ be an element of $S$. Then the non unital subring of $s$ is a non unital subring of $R$.

NonUnitalSubring.toAddSubgroupdefMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

the additive subgroup of self (from the name)

English

Let $\mathrm{self}$ be a non unital subring of $R$. Then the additive subgroup of $\mathrm{self}$ is an additive subgroup of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddSubmonoid}$ applied to $\operatorname{toNonUnitalSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{NonUnitalSubring\_\_neg\_mem'}$ applied to $\mathrm{self}$.

NonUnitalSubring.toSubsemigroupdefMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

the subsemigroup of s (from the name)

English

Let $s$ be a non unital subring of $R$. Then the subsemigroup of $s$ is a subsemigroup of $R$.

NonUnitalSubringClassclassMathlib.RingTheory.NonUnitalSubring.Defs, predicate

Wording

no wording

English

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

NonUnitalSubringClass.subtypedefMathlib.RingTheory.NonUnitalSubring.Defs, function or constant

Wording

the subtype of s (from the name)

English

Let $s$ be an element of $S$. Then the subtype of $s$ is a non unital ring homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $R$.

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

NonUnitalRingHom.srangedefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

no wording

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Then $\operatorname{srange}$ applied to $f$ is a non unital subsemiring of $S$.

NonUnitalRingHom.srangeRestrictdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

no wording

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Then $\operatorname{srangeRestrict}$ applied to $f$ is a non unital ring homomorphism of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{srange} (f)}{x_{2}})}$ defined as $\operatorname{codRestrict}$ applied to $f$, $\operatorname{srange}$ applied to $f$ and $\mathrm{NonUnitalRingHom\_\_mem\_srange\_self}$ applied to $f$.

NonUnitalSubsemiring.centerdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the center of R (from the docstring)

English

Let $R$ be a set. Then the center of $R$ is a non unital subsemiring of $R$.

NonUnitalSubsemiring.centerCongrdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the center congruence of e (from the name)

English

NonUnitalSubsemiring.centerToMulOppositedefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the center (from the docstring)

English

NonUnitalSubsemiring.centralizerdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the centralizer of s (from the docstring)

English

Let $s$ be an element of $\wp R$. Then the centralizer of $s$ is a non unital subsemiring of $R$.

NonUnitalSubsemiring.closuredefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the closure of s (from the name)

English

Let $s$ be an element of $\wp R$. Then the closure of $s$ is a non unital subsemiring of $R$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Leq} (s , S)$.

NonUnitalSubsemiring.comapdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the preimage of f and s (from the docstring)

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Let $s$ be a non unital subsemiring of $S$. Then the preimage of $f$ and $s$ is a non unital subsemiring of $R$.

NonUnitalSubsemiring.equivMapOfInjectivedefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the equivalence map of s and f (from the name)

English

Let $s$ be a non unital subsemiring of $R$. Let $f$ be a non unital ring homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $s$ and $f$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , s)}{x_{3}})}$.

NonUnitalSubsemiring.gidefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

no wording

English

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

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

Wording

the map of f and s (from the name)

English

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Let $s$ be a non unital subsemiring of $R$. Then the map of $f$ and $s$ is a non unital subsemiring of $S$.

NonUnitalSubsemiring.proddefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a non unital subsemiring of $R$. Let $t$ be a non unital subsemiring of $S$. Then the product of $s$ and $t$ is a non unital subsemiring of $\mathrm{Prod}$ applied to $R$ and $S$.

NonUnitalSubsemiring.prodEquivdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the product equivalence of s and t (from the name)

English

Let $s$ be a non unital subsemiring of $R$. Let $t$ be a non unital subsemiring of $S$. Then the product equivalence of $s$ and $t$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{prod} (s , t)}{x_{2}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {t}{x_{4}})}$.

NonUnitalSubsemiring.topEquivdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the top equivalence (from the name)

English

The top equivalence is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $R$.

RingEquiv.nonUnitalSubsemiringCongrdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the non unital subsemiring congruence of h (from the name)

English

Assume that $\EqtMACRoH {s}{t}$. Then the non unital subsemiring congruence of $h$ is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$.

RingEquiv.nonUnitalSubsemiringMapdefMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

the non unital subsemiring map of e and s (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Let $s$ be a non unital subsemiring of $R$. Then the non unital subsemiring map of $e$ and $s$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toNonUnitalRingHom} (e), s)}{x_{3}})}$.

RingEquiv.sofLeftInverse'defMathlib.RingTheory.NonUnitalSubsemiring.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then $\operatorname{sofLeftInverse'}$ applied to $h$ is a ring isomorphism of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{srange} (f)}{x_{2}})}$.