Definitions: Mathlib.RingTheory, part 6 of 6

Algebra.Generators.basisCotangentAwaydefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

no wording

English

Let $S$ be a set. Let $r$ be an element of $R$. Then $\operatorname{basisCotangentAway}$ applied to $S$ and $r$ is a basis of $S$ and $\operatorname{Cotangent}$ applied to the extension of $\operatorname{localizationAway}$ applied to $S$ and $r$ defined as $\operatorname{basisCotangent}$ applied to $\operatorname{localizationAway}$ applied to $S$ and $r$.

Algebra.Generators.cMulXSubOneCotangentdefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

no wording

English

Let $S$ be a set. Let $r$ be an element of $R$. Then $\operatorname{cMulXSubOneCotangent}$ applied to $S$ and $r$ is an element of $\operatorname{Cotangent}$ applied to the extension of $\operatorname{localizationAway}$ applied to $S$ and $r$ defined as $\operatorname{mk}$ applied to $\operatorname{C} (r)\times \operatorname{X} (\operatorname{unit})- 1$.

Algebra.SubmersivePresentation.basisCotangentdefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

no wording

English

Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then $\operatorname{basisCotangent}$ applied to $P$ is a basis of $S$ and $\operatorname{Cotangent}$ applied to the extension of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$ defined as the map of the basis derivative of $P$ and the inverse of the cotangent equivalence of $P$.

Algebra.SubmersivePresentation.basisKaehlerdefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

no wording

English

Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then $\operatorname{basisKaehler}$ applied to $P$ is a basis of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

Algebra.SubmersivePresentation.basisKaehlerOfIsCompldefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

no wording

English

Let $P$ be a submersive presentation of $x$ and $x_{1}$. Assume that $f$ is injective. Assume that $\mathrm{IsCompl}$ holds for the range of $f$ and the range of $\operatorname{map}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$. Then $\operatorname{basisKaehlerOfIsCompl}$ applied to $P$, $\mathrm{hf}$ and $\mathrm{hcompl}$ is a basis of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

Algebra.SubmersivePresentation.cotangentEquivdefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

the cotangent equivalence of P (from the name)

English

Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then the cotangent equivalence of $P$ is a linear equivalence of $\operatorname{Cotangent}$ applied to the extension of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$ and the set of functions from elements of $x_{1}$ to elements of $S$.

Algebra.SubmersivePresentation.sectionCotangentdefMathlib.RingTheory.Smooth.StandardSmoothCotangent, function or constant

Wording

no wording

English

Let $P$ be a submersive presentation of $x$ and $x_{1}$. Then $\operatorname{sectionCotangent}$ applied to $P$ is a linear map of the set of cotangent spaces of the extension of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$ and $\operatorname{Cotangent}$ applied to the extension of $\operatorname{toGenerators}$ applied to $\operatorname{toPresentation}$ applied to $\operatorname{toPreSubmersivePresentation}$ applied to $P$.

Mathlib.RingTheory.Spectrum.Maximal.Basic

MaximalSpectrum.equivSubtypedefMathlib.RingTheory.Spectrum.Maximal.Basic, function or constant

Wording

the equivalence subtype of R (from the name)

English

Let $R$ be a set. Then the equivalence subtype of $R$ is an element of $\EquivMACRoAE {\mathrm{MaximalSpectrum} (R)}{(\SubtypeSet {I}{\operatorname{IsMaximal} (I)})}$.

MaximalSpectrum.toPrimeSpectrumdefMathlib.RingTheory.Spectrum.Maximal.Basic, function or constant

Wording

the natural inclusion from the maximal spectrum to the prime spectrum of x1 (from the docstring)

English

Let $x_{1}$ be a maximal spectrum of $R$. Then the natural inclusion from the maximal spectrum to the prime spectrum of $x_{1}$ is a prime spectrum of $R$.

Mathlib.RingTheory.Spectrum.Maximal.Defs

MaximalSpectrumstructureMathlib.RingTheory.Spectrum.Maximal.Defs, type

Wording

maximal spectrum of R (from the name)

English

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

MaximalSpectrum.asIdealdefMathlib.RingTheory.Spectrum.Maximal.Defs, function or constant

Wording

no wording

English

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

Mathlib.RingTheory.Spectrum.Maximal.Localization

MaximalSpectrum.PiLocalizationdefMathlib.RingTheory.Spectrum.Maximal.Localization, type

Wording

product localization of R (from the name)

English

Let $R$ be a set. Then a product localization of $R$ is an element of the function that maps $R$ to the set of functions from maximal spectra $I$ of $R$ to elements of $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $I$.

MaximalSpectrum.mapPiLocalizationdefMathlib.RingTheory.Spectrum.Maximal.Localization, function or constant

Wording

the map product localization of f and hf (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the map product localization of $f$ and $\mathrm{hf}$ is a ring homomorphism of the set of product localizations of $R$ and the set of product localizations of $S$.

MaximalSpectrum.toPiLocalizationdefMathlib.RingTheory.Spectrum.Maximal.Localization, function or constant

Wording

the product localization of R (from the name)

English

Let $R$ be a set. Then the product localization of $R$ is an algebra homomorphism of $R$ and the set of product localizations of $R$ defined as the algebra of $R$ and the set of product localizations of $R$.

PrimeSpectrum.PiLocalizationdefMathlib.RingTheory.Spectrum.Maximal.Localization, type

Wording

product localization of R (from the name)

English

Let $R$ be a set. Then a product localization of $R$ is an element of the function that maps $R$ to the set of functions from prime spectra $p$ of $R$ to localizations of the complement of $\operatorname{asIdeal}$ applied to $p$.

PrimeSpectrum.mapPiLocalizationdefMathlib.RingTheory.Spectrum.Maximal.Localization, function or constant

Wording

the map product localization of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map product localization of $f$ is a ring homomorphism of the set of product localizations of $R$ and the set of product localizations of $S$.

PrimeSpectrum.piLocalizationToMaximaldefMathlib.RingTheory.Spectrum.Maximal.Localization, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{piLocalizationToMaximal}$ applied to $R$ is an algebra homomorphism of the set of product localizations of $R$ and the set of product localizations of $R$ defined as the product of the function that maps $I$ to the evaluation algebra homomorphism of the function that maps $p$ to the set of localizations of the complement of $\operatorname{asIdeal}$ applied to $p$ and the natural inclusion from the maximal spectrum to the prime spectrum of $I$.

PrimeSpectrum.piLocalizationToMaximalEquivdefMathlib.RingTheory.Spectrum.Maximal.Localization, function or constant

Wording

the product localization to maximal equivalence of h (from the name)

English

Assume that for all ideals $I$ of $R$, if $I$ is prime, then $I$ is maximal. Then the product localization to maximal equivalence of $h$ is a ring isomorphism of the set of product localizations of $R$ and the set of product localizations of $R$.

PrimeSpectrum.toPiLocalizationdefMathlib.RingTheory.Spectrum.Maximal.Localization, function or constant

Wording

the product localization of R (from the name)

English

Mathlib.RingTheory.Spectrum.Prime.Basic

PrimeSpectrum.primeSpectrumProddefMathlib.RingTheory.Spectrum.Prime.Basic, function or constant

Wording

the prime spectrum product of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the prime spectrum product of $R$ and $S$ is an equivalence from the set of prime spectra of $\mathrm{Prod}$ applied to $R$ and $S$ to $\mathrm{Sum}$ applied to the set of prime spectra of $R$ and the set of prime spectra of $S$.

PrimeSpectrum.primeSpectrumProdOfSumdefMathlib.RingTheory.Spectrum.Prime.Basic, function or constant

Wording

the prime spectrum product of x2 (from the name)

English

Let $R$ and $S$ be sets. Let $x_{2}$ be an element of $\mathrm{Sum}$ applied to the set of prime spectra of $R$ and the set of prime spectra of $S$. Then the prime spectrum product of $x_{2}$ is a prime spectrum of $\mathrm{Prod}$ applied to $R$ and $S$.

PrimeSpectrum.vanishingIdealdefMathlib.RingTheory.Spectrum.Prime.Basic, function or constant

Wording

the vanishing ideal of t (from the docstring)

English

Let $t$ be an element of the power set of the set of prime spectra of $R$. Then the vanishing ideal of $t$ is an ideal of $R$ defined as the infimum of the function that maps $x_{1}$ to the infimum of the function that maps $h$ to $\operatorname{asIdeal}$ applied to $x_{1}$.

PrimeSpectrum.zeroLocusdefMathlib.RingTheory.Spectrum.Prime.Basic, function or constant

Wording

the zero locus of s (from the docstring)

English

Let $s$ be an element of $\wp R$. Then the zero locus of $s$ is an element of the power set of the set of prime spectra of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\mathrm{Leq} (s , \operatorname{asIdeal} (x_{1}))$.

Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

ChevalleyThm.MvPolynomialC.degBounddefMathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity, function or constant

Wording

the degree bound of D and x (from the name)

English

Let $k$ and $x$ be natural numbers. Let $D$ be a function from natural numbers to natural numbers. Then the degree bound of $D$ and $x$ is a natural number defined as $\mathrm{ChevalleyThm\_\_MvPolynomialC\_\_numBound\_\_\_mutual}$ applied to $k$, $D$ and $\operatorname{inr}$ applied to $x$.

ChevalleyThm.MvPolynomialC.numBounddefMathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity, function or constant

Wording

the numerator bound of D and x (from the name)

English

Let $k$ and $x$ be natural numbers. Let $D$ be a function from natural numbers to natural numbers. Then the numerator bound of $D$ and $x$ is a natural number defined as $\mathrm{ChevalleyThm\_\_MvPolynomialC\_\_numBound\_\_\_mutual}$ applied to $k$, $D$ and $\operatorname{inl}$ applied to $x$.

ChevalleyThm.degBounddefMathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity, function or constant

Wording

the degree bound of n and d (from the name)

English

Let $k$, $m$ and $n$ be natural numbers. Let $d$ be a multiset of $\mathrm{Fin}$ applied to $m$. Then the degree bound of $n$ and $d$ is a natural number defined as the degree bound of the function that maps $x$ to the sum of $1$ and the count of $x$ and the map of $\operatorname{val}$ and $d$ and $m$.

ChevalleyThm.numBounddefMathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity, function or constant

Wording

the numerator bound of n and d (from the name)

English

Let $k$, $m$ and $n$ be natural numbers. Let $d$ be a multiset of $\mathrm{Fin}$ applied to $m$. Then the numerator bound of $n$ and $d$ is a natural number defined as the numerator bound of the function that maps $x$ to the sum of $1$ and the count of $x$ and the map of $\operatorname{val}$ and $d$ and $m$.

Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

PrimeSpectrum.BasicConstructibleSetDatastructureMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, type

Wording

no wording

English

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

PrimeSpectrum.BasicConstructibleSetData.fdefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{BasicConstructibleSetData}$ applied to $R$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

PrimeSpectrum.BasicConstructibleSetData.gdefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{BasicConstructibleSetData}$ applied to $R$. Let $x$ be an element of $\mathrm{Fin}$ applied to $\operatorname{n}$ applied to $\mathrm{self}$. Then $\operatorname{g}$ applied to $\mathrm{self}$ and $x$ is an element of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x$.

PrimeSpectrum.BasicConstructibleSetData.mapdefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

the map of x2 and C (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $C$ be an element of $\operatorname{BasicConstructibleSetData}$ applied to $R$. Then the map of $x_{2}$ and $C$ is an element of $\operatorname{BasicConstructibleSetData}$ applied to $S$ defined as $\operatorname{mk}$ applied to $x_{2}$ applied to $\operatorname{f}$ applied to $C$, $\operatorname{n}$ applied to $C$ and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $x_{2}$ and $\operatorname{g}$ applied to $C$.

PrimeSpectrum.BasicConstructibleSetData.ndefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{BasicConstructibleSetData}$ applied to $R$. Then $\operatorname{n}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

PrimeSpectrum.BasicConstructibleSetData.toSetdefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

the set of C (from the name)

English

Let $C$ be an element of $\operatorname{BasicConstructibleSetData}$ applied to $R$. Then the set of $C$ is an element of the power set of the set of prime spectra of $R$ defined as $\operatorname{sdiff}$ applied to the zero locus of the range of $\operatorname{g}$ applied to $C$ and the zero locus of $\operatorname{singleton}$ applied to $\operatorname{f}$ applied to $C$.

PrimeSpectrum.ConstructibleSetDatadefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, type

Wording

constructible set data of R (from the name)

English

Let $R$ be a set. Then a constructible set data of $R$ is an element of the function that maps $R$ to the set of finite sets of $\operatorname{BasicConstructibleSetData}$ applied to $R$.

PrimeSpectrum.ConstructibleSetData.degBounddefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

the degree bound of S (from the name)

English

Let $S$ be a constructible set data of the set of polynomials of $R$. Then the degree bound of $S$ is an element of $\Natural$ defined as the supremum of $S$ and the function that maps $C$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{succ} (\operatorname{degree} (\operatorname{g} (C , i)))}$.

PrimeSpectrum.ConstructibleSetData.mapdefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

the map of x2 and s (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $s$ be a constructible set data of $R$. Then the map of $x_{2}$ and $s$ is a constructible set data of $S$ defined as the forward image of $s$ under $\operatorname{map}$ applied to $x_{2}$.

PrimeSpectrum.ConstructibleSetData.toSetdefMathlib.RingTheory.Spectrum.Prime.ConstructibleSet, function or constant

Wording

the set of S (from the name)

English

Let $S$ be a constructible set data of $R$. Then the set of $S$ is an element of the power set of the set of prime spectra of $R$ defined as the union of the function that maps $C$ to the union of the function that maps $h$ to the set of $C$.

Mathlib.RingTheory.Spectrum.Prime.Defs

PrimeSpectrumstructureMathlib.RingTheory.Spectrum.Prime.Defs, type

Wording

prime spectrum of R (from the name)

English

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

PrimeSpectrum.asIdealdefMathlib.RingTheory.Spectrum.Prime.Defs, function or constant

Wording

no wording

English

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

PrimeSpectrum.equivSubtypedefMathlib.RingTheory.Spectrum.Prime.Defs, function or constant

Wording

the equivalence subtype of R (from the name)

English

Let $R$ be a set. Then the equivalence subtype of $R$ is an order isomorphism of the set of prime spectra of $R$ and $\SubtypeSet {I}{\operatorname{IsPrime} (I)}$.

Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Module.freeLocusdefMathlib.RingTheory.Spectrum.Prime.FreeLocus, function or constant

Wording

the free locus of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the free locus of $R$ and $M$ is an element of the power set of the set of prime spectra of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\operatorname{Free}$ applied to $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $p$ and the set of localized modules of the complement of $\operatorname{asIdeal}$ applied to $p$ and $M$.

Module.rankAtStalkdefMathlib.RingTheory.Spectrum.Prime.FreeLocus, function or constant

Wording

the rank at stalk of M and p (from the name)

English

Let $M$ be a set. Let $p$ be a prime spectrum of $R$. Then the rank at stalk of $M$ and $p$ is a natural number defined as the rank of $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $p$ and the set of localized modules of the complement of $\operatorname{asIdeal}$ applied to $p$ and $M$.

Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

AlgebraicGeometry.Polynomial.imageOfDfdefMathlib.RingTheory.Spectrum.Prime.IsOpenComapC, function or constant

Wording

the image of f (from the name)

English

Let $f$ be a polynomial of $R$. Then the image of $f$ is an element of the power set of the set of prime spectra of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that there exists a natural number $i$, such that it is not the case that $\MembershipmemMACRoT {\operatorname{asIdeal} (p)}{\operatorname{coeff} (f , i)}$.

Mathlib.RingTheory.Spectrum.Prime.RingHom

Ideal.primeSpectrumOrderIsoZeroLocusOfSurjdefMathlib.RingTheory.Spectrum.Prime.RingHom, function or constant

Wording

the prime spectrum order isomorphism zero locus of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$ and the kernel of $f$ is equal to $I$. Then the prime spectrum order isomorphism zero locus of $f$ is an order isomorphism of the set of prime spectra of $S$ and the set of elements of the zero locus of $I$.

Ideal.primeSpectrumQuotientOrderIsoZeroLocusdefMathlib.RingTheory.Spectrum.Prime.RingHom, function or constant

Wording

the prime spectrum quotient order isomorphism zero locus of I (from the name)

English

Let $I$ be an ideal of $R$. Then the prime spectrum quotient order isomorphism zero locus of $I$ is an order isomorphism of the set of prime spectra of the set of quotients of $R$ and $I$ and the set of elements of the zero locus of $I$.

PrimeSpectrum.comapdefMathlib.RingTheory.Spectrum.Prime.RingHom, function or constant

Wording

the preimage of f and p (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $p$ be a prime spectrum of $S$. Then the preimage of $f$ and $p$ is a prime spectrum of $R$.

PrimeSpectrum.comapEquivdefMathlib.RingTheory.Spectrum.Prime.RingHom, function or constant

Wording

the preimage equivalence of e (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then the preimage equivalence of $e$ is an order isomorphism of the set of prime spectra of $R$ and the set of prime spectra of $S$.

PrimeSpectrum.sigmaToPidefMathlib.RingTheory.Spectrum.Prime.RingHom, function or constant

Wording

the sigma to product of R and x2 (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to the set of prime spectra of $R$ applied to $i_{1}$. Then the sigma to product of $R$ and $x_{2}$ is a prime spectrum of the set of functions from elements $i$ of $x$ to elements of $R$ applied to $i$.

Mathlib.RingTheory.Spectrum.Prime.TensorProduct

PrimeSpectrum.tensorProductTodefMathlib.RingTheory.Spectrum.Prime.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $S$ and $T$ be sets. Let $x_{5}$ be a prime spectrum of the set of tensor products of $S$ and $T$. Then $\operatorname{tensorProductTo}$ applied to $R$, $S$, $T$ and $x_{5}$ is an element of $\mathrm{Prod}$ applied to the set of prime spectra of $S$ and the set of prime spectra of $T$ defined as $\ProdmkMACRoU {\operatorname{comap} (\operatorname{algebraMap} (S , \mathrm{TensorProduct} (S , T)), x_{5})}{\operatorname{comap} (\operatorname{toRingHom} (\operatorname{includeRight}), x_{5})}$.

Mathlib.RingTheory.Spectrum.Prime.Topology

Ideal.minimalPrimes.equivIrreducibleComponentsdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the equivalence irreducible component of I (from the name)

English

Let $I$ be an ideal of $R$. Then the equivalence irreducible component of $I$ is an order isomorphism of the set of elements of the minimal prime of $I$ and the set of order duals of the set of elements of the irreducible component of the set of elements of the zero locus of $I$.

IsLocalRing.closedPointdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the closed point in the prime spectrum of R (from the docstring)

English

Let $R$ be a set. Then the closed point in the prime spectrum of $R$ is a prime spectrum of $R$.

MaximalSpectrum.toPiLocalizationEquivdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the product localization equivalence of R (from the name)

English

Let $R$ be a set. Then the product localization equivalence of $R$ is an algebra isomorphism of $R$ and the set of product localizations of $R$.

PrimeSpectrum.basicOpendefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Then $\operatorname{basicOpen}$ applied to $r$ is an open of the set of prime spectra of $R$.

PrimeSpectrum.closedsEmbeddingdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the closed embedding of R (from the name)

English

Let $R$ be a set. Then the closed embedding of $R$ is an order embedding of the set of order duals of $\operatorname{Closeds}$ applied to the set of prime spectra of $R$ and the set of ideals of $R$.

PrimeSpectrum.homeomorphOfRingEquivdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then the homeomorphism of $e$ is a homeomorphism of the set of prime spectra of $R$ and the set of prime spectra of $S$.

PrimeSpectrum.isIdempotentElemEquivClopensdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

no wording

English

$\operatorname{isIdempotentElemEquivClopens}$ is an order isomorphism of $\SubtypeSet {e}{\mathrm{IsIdempotentElem} (e)}$ and the set of clopens of the set of prime spectra of $R$ defined as the composition of $\operatorname{isIdempotentElemMulZeroAddOne}$ and the multiplicative zero additive one equivalence clopen.

PrimeSpectrum.localizationMapOfSpecializesdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the localization map of h (from the name)

English

Assume that $\mathrm{Specializes}$ holds for $x_{1}$ and $y$. Then the localization map of $h$ is a ring homomorphism of $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $y$ and $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $x_{1}$.

PrimeSpectrum.mulZeroAddOneEquivClopensdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the multiplicative zero additive one equivalence clopen (from the name)

English

The multiplicative zero additive one equivalence clopen is an order isomorphism of $\SubtypeSet {e}{\mathrm{and} (\EqtMACRoH {(\ProdfstMACRoZ {e}\times \ProdsndMACRoAA {e})}{0}, \EqtMACRoH {(\ProdfstMACRoZ {e}+ \ProdsndMACRoAA {e})}{1})}$ and the set of clopens of the set of prime spectra of $R$.

PrimeSpectrum.nhdsOrderEmbeddingdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the neighbourhood filter order embedding (from the name)

English

The neighbourhood filter order embedding is an order embedding of the set of prime spectra of $R$ and the set of filters of the set of prime spectra of $R$.

PrimeSpectrum.pointsEquivIrreducibleClosedsdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{pointsEquivIrreducibleCloseds}$ applied to $R$ is an order isomorphism of the set of prime spectra of $R$ and the set of order duals of $\operatorname{IrreducibleCloseds}$ applied to the set of prime spectra of $R$.

PrimeSpectrum.primeSpectrumProdHomeodefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the prime spectrum product homeomorphism (from the name)

English

The prime spectrum product homeomorphism is a homeomorphism of the set of prime spectra of $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Sum}$ applied to the set of prime spectra of $R$ and the set of prime spectra of $S$.

PrimeSpectrum.sigmaToPiHomeodefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the sigma to product homeomorphism of R (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Then the sigma to product homeomorphism of $R$ is a homeomorphism of $\Sigma$ applied to the function that maps $i$ to the set of prime spectra of $R$ applied to $i$ and the set of prime spectra of the set of functions from elements $i_{1}$ of $x$ to elements of $R$ applied to $i_{1}$.

PrimeSpectrum.toPiLocalizationEquivdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the product localization equivalence of R (from the name)

English

Let $R$ be a set. Then the product localization equivalence of $R$ is an algebra isomorphism of $R$ and the set of product localizations of $R$ defined as the algebra isomorphism of the product localization of $R$ and $\mathrm{PrimeSpectrum\_\_toPiLocalization\_bijective}$.

PrimeSpectrum.zeroLocusEquivIrreducibleClosedsdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

no wording

English

Let $I$ be an element of $\wp R$. Then $\operatorname{zeroLocusEquivIrreducibleCloseds}$ applied to $I$ is an order isomorphism of the set of elements of the zero locus of $I$ and the set of order duals of $\operatorname{IrreducibleCloseds}$ applied to the set of elements of the zero locus of $I$.

minimalPrimes.equivIrreducibleComponentsdefMathlib.RingTheory.Spectrum.Prime.Topology, function or constant

Wording

the equivalence irreducible component of R (from the name)

English

Let $R$ be a set. Then the equivalence irreducible component of $R$ is an order isomorphism of the set of elements of the minimal prime of $R$ and the set of order duals of the set of elements of the irreducible component of the set of prime spectra of $R$.

Mathlib.RingTheory.Support

Module.supportdefMathlib.RingTheory.Support, function or constant

Wording

the support of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the support of $R$ and $M$ is an element of the power set of the set of prime spectra of $R$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that the set of localized modules of the complement of $\operatorname{asIdeal}$ applied to $p$ and $M$ is nontrivial.

Mathlib.RingTheory.SurjectiveOnStalks

RingHom.SurjectiveOnStalksdefMathlib.RingTheory.SurjectiveOnStalks, predicate

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then we can say that $\operatorname{SurjectiveOnStalks}$ holds for $f$.

Mathlib.RingTheory.Teichmuller

Perfection.quotientMulEquivdefMathlib.RingTheory.Teichmuller, function or constant

Wording

the quotient multiplicative equivalence of p and I (from the name)

English

Let $p$ be a natural number. Let $I$ be an ideal of $R$. Then the quotient multiplicative equivalence of $p$ and $I$ is a multiplicative equivalence of the set of perfections of $R$ and $p$ and the set of perfections of the set of quotients of $R$ and $I$ and $p$.

Perfection.teichmullerdefMathlib.RingTheory.Teichmuller, function or constant

Wording

the Teichmuller of p and I (from the name)

English

Let $p$ be a natural number. Let $I$ be an ideal of $R$. Then the Teichmuller of $p$ and $I$ is a monoid homomorphism of the set of perfections of the set of quotients of $R$ and $I$ and $p$ and $R$.

Perfection.teichmullerCauchydefMathlib.RingTheory.Teichmuller, function or constant

Wording

no wording

English

Let $x_{1}$ be a perfection of the set of quotients of $R$ and $I$ and $p$. Then $\operatorname{teichmullerCauchy}$ applied to $x_{1}$ is an adic Cauchy sequence of $I$ and $R$.

Perfection.teichmullerFundefMathlib.RingTheory.Teichmuller, function or constant

Wording

the Teichmuller function of x1 (from the name)

English

Let $x_{1}$ be a perfection of the set of quotients of $R$ and $I$ and $p$. Then the Teichmuller function of $x_{1}$ is an element of $R$ defined as $\operatorname{choose}$ applied to $\mathrm{Perfection\_\_exists\_teichmullerFun}$ applied to $x_{1}$.

Perfection.teichmuller₀defMathlib.RingTheory.Teichmuller, function or constant

Wording

the Teichmuller of p and I (from the name)

English

Let $p$ be a natural number. Let $I$ be an ideal of $R$. Then the Teichmuller of $p$ and $I$ is a monoid with zero homomorphism of the set of perfections of the set of quotients of $R$ and $I$ and $p$ and $R$.

Mathlib.RingTheory.TensorProduct.Basic

AlgHom.liftEquivdefMathlib.RingTheory.TensorProduct.Basic, function or constant

Wording

the lift equivalence of A and B (from the name)

English

Let $R$, $S$, $A$ and $B$ be sets. Then the lift equivalence of $A$ and $B$ is an equivalence from the set of algebra homomorphisms of $A$ and $B$ to the set of algebra homomorphisms of the set of tensor products of $S$ and $A$ and $B$.

Algebra.TensorProduct.includeLeftdefMathlib.RingTheory.TensorProduct.Basic, function or constant

Wording

no wording

English

$\operatorname{includeLeft}$ is an algebra homomorphism of $A$ and the set of tensor products of $A$ and $B$.

Algebra.TensorProduct.includeLeftRingHomdefMathlib.RingTheory.TensorProduct.Basic, function or constant

Wording

the ring morphism (from the docstring)

English

The ring morphism is a ring homomorphism of $A$ and the set of tensor products of $A$ and $B$.

Algebra.TensorProduct.includeRightdefMathlib.RingTheory.TensorProduct.Basic, function or constant

Wording

no wording

English

$\operatorname{includeRight}$ is an algebra homomorphism of $B$ and the set of tensor products of $A$ and $B$.

Algebra.TensorProduct.muldefMathlib.RingTheory.TensorProduct.Basic, function or constant

Wording

the product (from the name)

English

The product is a linear map of the set of tensor products of $A$ and $B$ and the set of linear maps of the set of tensor products of $A$ and $B$ and the set of tensor products of $A$ and $B$ defined as the map of the product of $R$ and $A$ and the product of $R$ and $B$.

Mathlib.RingTheory.TensorProduct.DirectLimitFG

Submodule.FG.directLimitdefMathlib.RingTheory.TensorProduct.DirectLimitFG, function or constant

Wording

the direct limit of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the direct limit of $R$ and $M$ is a linear equivalence of the set of direct limits of the function that maps $P$ to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {P}{x_{4}})}$ and the function that maps $P_{1}$, $Q$ and $h$ to the inclusion of $h$ and $M$.

Submodule.FG.lTensor.directLimitdefMathlib.RingTheory.TensorProduct.DirectLimitFG, function or constant

Wording

the direct limit of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the direct limit of $M$ and $N$ is a linear equivalence of the set of direct limits of the function that maps $Q$ to the set of tensor products of $M$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {Q}{x_{6}})}$ and the function that maps $x_{7}$, $x_{8}$ and $\mathrm{hPQ}$ to the tensor of $M$ and the inclusion of $\mathrm{hPQ}$ and the set of tensor products of $M$ and $N$ defined as the composition of the inverse of the right direct limit of the function that maps $x_{6}$ and $x_{7}$ to $\operatorname{inclusion}$ and $M$ and the tensor of $M$ and the direct limit of $R$ and $N$.

Submodule.FG.rTensor.directLimitdefMathlib.RingTheory.TensorProduct.DirectLimitFG, function or constant

Wording

the direct limit of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the direct limit of $M$ and $N$ is a linear equivalence of the set of direct limits of the function that maps $P$ to the set of tensor products of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {P}{x_{6}})}$ and $N$ and the function that maps $P_{1}$, $Q$ and $h$ to the tensor of $N$ and the inclusion of $h$ and the set of tensor products of $M$ and $N$ defined as the composition of the inverse of the left direct limit of the function that maps $P$ and $Q$ to $\operatorname{inclusion}$ and $N$ and the tensor of $N$ and the direct limit of $R$ and $M$.

Mathlib.RingTheory.TensorProduct.Free

Algebra.TensorProduct.basisdefMathlib.RingTheory.TensorProduct.Free, function or constant

Wording

the basis of A and b (from the name)

English

Let $A$ be a set. Let $b$ be a basis of $R$ and $M$. Then the basis of $A$ and $b$ is a basis of $A$ and the set of tensor products of $A$ and $M$.

Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Algebra.IsEffectivedefMathlib.RingTheory.TensorProduct.IncludeLeftSubRight, predicate

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{IsEffective}$ holds for $R$ and $S$, if $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to the linear map of $R$ and $S$ and $\operatorname{coe}$ applied to $\operatorname{includeLeftSubRight}$ applied to $R$ and $S$.

Algebra.TensorProduct.includeLeftSubRightdefMathlib.RingTheory.TensorProduct.IncludeLeftSubRight, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{includeLeftSubRight}$ applied to $R$ and $S$ is a linear map of $S$ and the set of tensor products of $S$ and $S$ defined as the difference between the linear map of $\operatorname{includeLeft}$ and the linear map of $\operatorname{includeRight}$.

Algebra.codRestrictEqLocusPushoutCoconedefMathlib.RingTheory.TensorProduct.IncludeLeftSubRight, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Then $\operatorname{codRestrictEqLocusPushoutCocone}$ applied to $R$ and $S$ is a ring homomorphism of $R$ and the set of carriers of $\operatorname{pt}$ applied to the equalizer fork of the left injection of the pushout cocone of $S$ and $S$ and the right injection of the pushout cocone of $S$ and $S$.

Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

IsBaseChange.basisdefMathlib.RingTheory.TensorProduct.IsBaseChangeFree, function or constant

Wording

the basis of b and ibc (from the docstring)

English

Let $b$ be a basis of $R$ and $V$. Assume that $x_{9}$ is a base change. Then the basis of $b$ and $\mathrm{ibc}$ is a basis of $S$ and $W$.

Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

IsBaseChange.endHomdefMathlib.RingTheory.TensorProduct.IsBaseChangeHom, function or constant

Wording

the end homomorphism of j (from the name)

English

Assume that $x_{8}$ is a base change. Then the end homomorphism of $j$ is a linear map of the set of linear maps of $M$ and $M$ and the set of linear maps of $P$ and $P$ defined as the composition of $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{flip}$ applied to $\operatorname{llcomp}$ applied to $S$, $P$, the set of tensor products of $S$ and $M$ and $P$ and $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of $j$ and the composition of $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{toLinearMap}$ applied to the lift base change equivalence of $S$ and the right composition of $R$ and $x_{8}$.

IsBaseChange.linearMapLeftRightHomdefMathlib.RingTheory.TensorProduct.IsBaseChangeHom, function or constant

Wording

the linear map left right homomorphism of j and x14 (from the name)

English

Assume that $x_{13}$ is a base change. Let $x_{14}$ be a linear map of $N$ and $Q$. Then the linear map left right homomorphism of $j$ and $x_{14}$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of $P$ and $Q$ defined as the composition of $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{flip}$ applied to $\operatorname{llcomp}$ applied to $S$, $P$, the set of tensor products of $S$ and $M$ and $Q$ and $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of $j$ and the composition of $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{toLinearMap}$ applied to the lift base change equivalence of $S$ and the right composition of $R$ and $x_{14}$.

IsBaseChange.linearMapRightBaseChangeEquivdefMathlib.RingTheory.TensorProduct.IsBaseChangeHom, function or constant

Wording

the linear map right base change equivalence of M and ibc (from the name)

English

Let $M$ be a set. Assume that $x_{10}$ is a base change. Then the linear map right base change equivalence of $M$ and $\mathrm{ibc}$ is a linear equivalence of the set of tensor products of $S$ and the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $P$.

IsBaseChange.linearMapRightBaseChangeHomdefMathlib.RingTheory.TensorProduct.IsBaseChangeHom, function or constant

Wording

the linear map right base change homomorphism of x10 (from the name)

English

Let $S$ and $M$ be sets. Let $x_{10}$ be a linear map of $N$ and $P$. Then the linear map right base change homomorphism of $x_{10}$ is a linear map of the set of tensor products of $S$ and the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $P$.

Mathlib.RingTheory.TensorProduct.Maps

Algebra.TensorProduct.algEquivOfLinearEquivTensorProductdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the algebra isomorphism of f (from the name)

English

Let $f$ be a linear equivalence of the set of tensor products of $A$ and $B$ and $C$ such that for all elements $x_{10}$ of $A$, for all elements $x_{11}$ of $A$, for all elements $x_{12}$ of $B$, for all elements $x_{13}$ of $B$, $\EqtMACRoH {f (\operatorname{tmul} (R , x_{10} \times x_{11} , x_{12} \times x_{13}))}{f (\operatorname{tmul} (R , x_{10} , x_{12}))\times f (\operatorname{tmul} (R , x_{11} , x_{13}))}$ and $\EqtMACRoH {f (\operatorname{tmul} (R , 1 , 1))}{1}$. Then the algebra isomorphism of $f$ is an algebra isomorphism of the set of tensor products of $A$ and $B$ and $C$.

Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProductdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the algebra isomorphism of f (from the name)

English

Let $f$ be a linear equivalence of the set of tensor products of the set of tensor products of $A$ and $B$ and $C$ and $D$ such that for all elements $x_{9}$ of $A$, for all elements $x_{10}$ of $A$, for all elements $x_{11}$ of $B$, for all elements $x_{12}$ of $B$, for all elements $x_{13}$ of $C$, for all elements $x_{14}$ of $C$, $\EqtMACRoH {f (\operatorname{tmul} (R , \operatorname{tmul} (R , x_{9} \times x_{10} , x_{11} \times x_{12}), x_{13} \times x_{14}))}{f (\operatorname{tmul} (R , \operatorname{tmul} (R , x_{9} , x_{11}), x_{13}))\times f (\operatorname{tmul} (R , \operatorname{tmul} (R , x_{10} , x_{12}), x_{14}))}$ and $\EqtMACRoH {f (\operatorname{tmul} (R , \operatorname{tmul} (R , 1 , 1), 1))}{1}$. Then the algebra isomorphism of $f$ is an algebra isomorphism of the set of tensor products of the set of tensor products of $A$ and $B$ and $C$ and $D$.

Algebra.TensorProduct.algHomOfLinearMapTensorProductdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the algebra homomorphism of f (from the name)

English

Let $f$ be a linear map of the set of tensor products of $A$ and $B$ and $C$ such that for all elements $x_{10}$ of $A$, for all elements $x_{11}$ of $A$, for all elements $x_{12}$ of $B$, for all elements $x_{13}$ of $B$, $\EqtMACRoH {f (\operatorname{tmul} (R , x_{10} \times x_{11} , x_{12} \times x_{13}))}{f (\operatorname{tmul} (R , x_{10} , x_{12}))\times f (\operatorname{tmul} (R , x_{11} , x_{13}))}$ and $\EqtMACRoH {f (\operatorname{tmul} (R , 1 , 1))}{1}$. Then the algebra homomorphism of $f$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and $C$ defined as the algebra homomorphism of $f$.

Algebra.TensorProduct.assocdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the associator of C and D (from the name)

English

Let $R$, $S$, $T$, $A$, $C$ and $D$ be sets. Then the associator of $C$ and $D$ is an algebra isomorphism of the set of tensor products of the set of tensor products of $A$ and $C$ and $D$ and the set of tensor products of $A$ and the set of tensor products of $C$ and $D$.

Algebra.TensorProduct.cancelBaseChangedefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.commdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.commRightdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.congrdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the congruence of f and g (from the name)

English

Let $f$ be an algebra isomorphism of $A$ and $C$. Let $g$ be an algebra isomorphism of $B$ and $D$. Then the congruence of $f$ and $g$ is an algebra isomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $C$ and $D$.

Algebra.TensorProduct.equivOfCompatibleSMuldefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the equivalence of A and B (from the name)

English

Let $R$, $S$, $T$, $A$ and $B$ be sets. Then the equivalence of $A$ and $B$ is an algebra isomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $A$ and $B$.

Algebra.TensorProduct.lTensordefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the tensor of A and g (from the name)

English

Let $A$ be a set. Let $g$ be an algebra homomorphism of $B$ and $D$. Then the tensor of $A$ and $g$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $A$ and $D$ defined as the map of the identity of $S$ and $A$ and $g$.

Algebra.TensorProduct.leftCommdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

Let $R$, $A$, $B$ and $C$ be sets. Then $\operatorname{leftComm}$ applied to $R$, $A$, $B$ and $C$ is an algebra isomorphism of the set of tensor products of $A$ and the set of tensor products of $B$ and $C$ and the set of tensor products of $B$ and the set of tensor products of $A$ and $C$ defined as the composition of the inverse of the associator of $B$ and $C$ and the composition of the congruence of $\operatorname{comm}$ applied to $R$, $A$ and $B$ and the identity and the associator of $A$ and $C$.

Algebra.TensorProduct.liddefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.lidOfCompatibleSMuldefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

Let $R$, $S$ and $A$ be sets. Then $\operatorname{lidOfCompatibleSMul}$ applied to $R$, $S$ and $A$ is an algebra isomorphism of the set of tensor products of $S$ and $A$ and $A$ defined as the composition of the inverse of the equivalence of $S$ and $A$ and $\operatorname{lid}$ applied to $S$ and $A$.

Algebra.TensorProduct.liftdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the lift of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $C$. Let $g$ be an algebra homomorphism of $B$ and $C$ such that for all elements $x_{11}$ of $A$, for all elements $y$ of $B$, $\mathrm{Commute}$ holds for $f$ applied to $x_{11}$ and $g$ applied to $y$. Then the lift of $f$ and $g$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and $C$.

Algebra.TensorProduct.liftEquivdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the lift equivalence (from the name)

English

The lift equivalence is an equivalence from $\SubtypeSet {\mathrm{fg}}{\mathrm{forall} (A , \lambda x_{11} . \mathrm{forall} (B , \lambda y . \mathrm{Commute} (\operatorname{fst} (\mathrm{fg} , x_{11}), \operatorname{snd} (\mathrm{fg} , y))))}$ to the set of algebra homomorphisms of the set of tensor products of $A$ and $B$ and $C$.

Algebra.TensorProduct.liftEquivRightdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the right lift equivalence of B and C (from the name)

English

Let $R$, $S$, $B$ and $C$ be sets. Then the right lift equivalence of $B$ and $C$ is an equivalence from the set of algebra homomorphisms of $B$ and $C$ to the set of algebra homomorphisms of the set of tensor products of $S$ and $B$ and $C$.

Algebra.TensorProduct.lmul'defMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{lmul'}$ applied to $R$ is an algebra homomorphism of the set of tensor products of $S$ and $S$ and $S$ defined as $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{lmul''}$ applied to $R$.

Algebra.TensorProduct.lmul''defMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{lmul''}$ applied to $R$ is an algebra homomorphism of the set of tensor products of $S$ and $S$ and $S$.

Algebra.TensorProduct.lmulEquivdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.mapdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the map 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 $D$. Then the map of $f$ and $g$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $C$ and $D$.

Algebra.TensorProduct.mapOfCompatibleSMuldefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the map of A and B (from the name)

English

Let $R$, $S$, $T$, $A$ and $B$ be sets. Then the map of $A$ and $B$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and the set of tensor products of $A$ and $B$.

Algebra.TensorProduct.mapRingHomdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the map ring homomorphism of fS and fT (from the name)

English

Let $\mathrm{fR}$ be a ring homomorphism of $R$ and $\mathrm{R'}$. Let $\mathrm{fS}$ be a ring homomorphism of $S$ and $\mathrm{S'}$. Let $\mathrm{fT}$ be a ring homomorphism of $T$ and $\mathrm{T'}$. Assume that the composition of $\mathrm{fS}$ and the algebra map of $R$ and $S$ is equal to the composition of the algebra map of $\mathrm{R'}$ and $\mathrm{S'}$ and $\mathrm{fR}$. Assume that the composition of $\mathrm{fT}$ and the algebra map of $R$ and $T$ is equal to the composition of the algebra map of $\mathrm{R'}$ and $\mathrm{T'}$ and $\mathrm{fR}$. Then the map ring homomorphism of $\mathrm{fS}$ and $\mathrm{fT}$ is a ring homomorphism of the set of tensor products of $S$ and $T$ and the set of tensor products of $\mathrm{S'}$ and $\mathrm{T'}$.

Algebra.TensorProduct.productLeftAlgHomdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the product left algebra homomorphism 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 product left algebra homomorphism of $f$ and $g$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and $C$.

Algebra.TensorProduct.productMapdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the product map of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $S$. Let $g$ be an algebra homomorphism of $B$ and $S$. Then the product map of $f$ and $g$ is an algebra homomorphism of the set of tensor products of $A$ and $B$ and $S$ defined as the product left algebra homomorphism of $f$ and $g$.

Algebra.TensorProduct.rTensordefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the tensor of B and f (from the name)

English

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

Algebra.TensorProduct.riddefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.tensorTensorTensorCommdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

no wording

English

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

Algebra.TensorProduct.uliftEquivdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the lift equivalence of A and B (from the name)

English

Let $R$, $S$, $A$ and $B$ be sets. Then the lift equivalence of $A$ and $B$ is an algebra isomorphism of $\mathrm{ULift}$ applied to the set of tensor products of $A$ and $B$ and the set of tensor products of $\mathrm{ULift}$ applied to $A$ and $\mathrm{ULift}$ applied to $B$ defined as the composition of the algebra isomorphism and the composition of the congruence of the inverse of the algebra isomorphism and the inverse of the algebra isomorphism and the equivalence of $\mathrm{ULift}$ applied to $A$ and $\mathrm{ULift}$ applied to $B$.

LinearMap.tensorProductdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the tensor product of M and N (from the name)

English

Let $R$, $A$, $M$ and $N$ be sets. Then the tensor product of $M$ and $N$ is a linear map of the set of tensor products of $A$ and the set of linear maps of $M$ and $N$ and the set of linear maps of the set of tensor products of $A$ and $M$ and the set of tensor products of $A$ and $N$.

LinearMap.tensorProductEnddefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the tensor product end of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the tensor product end of $A$ and $M$ is an algebra homomorphism of the set of tensor products of $A$ and the set of ends of $R$ and $M$ and the set of ends of $A$ and the set of tensor products of $A$ and $M$.

Module.End.lTensorAlgHomdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the tensor algebra homomorphism of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the tensor algebra homomorphism of $M$ and $N$ is an algebra homomorphism of the set of ends of $R$ and $M$ and the set of ends of $R$ and the set of tensor products of $N$ and $M$ defined as the algebra homomorphism of the tensor homomorphism of $N$.

Module.End.rTensorAlgHomdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the tensor algebra homomorphism of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the tensor algebra homomorphism of $M$ and $N$ is an algebra homomorphism of the set of ends of $R$ and $M$ and the set of ends of $R$ and the set of tensor products of $M$ and $N$ defined as the algebra homomorphism of the tensor homomorphism of $N$.

Module.endTensorEndAlgHomdefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

the end tensor end algebra homomorphism (from the name)

English

The end tensor end algebra homomorphism is an algebra homomorphism of the set of tensor products of the set of ends of $A$ and $M$ and the set of ends of $R$ and $N$ and the set of ends of $A$ and the set of tensor products of $M$ and $N$.

Subalgebra.baseChangedefMathlib.RingTheory.TensorProduct.Maps, function or constant

Wording

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

English

Let $B$ be a set. Let $C$ be a subalgebra of $R$ and $A$. Then the base change of $B$ and $C$ is a subalgebra of $B$ and the set of tensor products of $B$ and $A$ defined as the range of the map of the identity of $B$ and $B$ and the value of $C$.

Mathlib.RingTheory.TensorProduct.MonoidAlgebra

AddMonoidAlgebra.lTensorAlgEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

the tensor algebra isomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the tensor algebra isomorphism of $A$ and $B$ is an algebra isomorphism of the set of tensor products of the set of additive monoid algebras of $A$ and $M$ and $B$ and the set of additive monoid algebras of the set of tensor products of $A$ and $B$ and $M$ defined as the composition of $\operatorname{comm}$ applied to $R$, the set of additive monoid algebras of $A$ and $M$ and $B$ and the composition of the tensor equivalence algebra isomorphism of $B$ and $A$ and the map algebra isomorphism of $\operatorname{comm}$ applied to $R$, $B$ and $A$.

AddMonoidAlgebra.rTensorEquivAlgEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

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

English

Let $R$, $S$, $A$ and $B$ be sets. Then the tensor equivalence algebra isomorphism of $A$ and $B$ is an algebra isomorphism of the set of tensor products of $A$ and the set of additive monoid algebras of $B$ and $M$ and the set of additive monoid algebras of the set of tensor products of $A$ and $B$ and $M$.

AddMonoidAlgebra.scalarTensorEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the scalar tensor equivalence of $R$ and $A$ is an algebra isomorphism of the set of tensor products of $A$ and the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $A$ and $M$ defined as the composition of the tensor equivalence algebra isomorphism of $A$ and $R$ and the map algebra isomorphism of $\operatorname{rid}$ applied to $R$, $A$ and $A$.

AddMonoidAlgebra.tensorEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

the tensor equivalence of R (from the name)

English

Let $R$ be a set. Then the tensor equivalence of $R$ is a linear equivalence of the set of tensor products of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $N$ and the set of additive monoid algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ defined as the composition of the composition of the congruence of the coefficient linear equivalence of $R$ and the coefficient linear equivalence of $R$ and the finitely supported function tensor finitely supported function of $M$ and $N$ and the inverse of the coefficient linear equivalence of $R$.

MonoidAlgebra.lTensorAlgEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

the tensor algebra isomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the tensor algebra isomorphism of $A$ and $B$ is an algebra isomorphism of the set of tensor products of the set of monoid algebras of $A$ and $M$ and $B$ and the set of monoid algebras of the set of tensor products of $A$ and $B$ and $M$ defined as the composition of $\operatorname{comm}$ applied to $R$, the set of monoid algebras of $A$ and $M$ and $B$ and the composition of the tensor equivalence algebra isomorphism of $B$ and $A$ and the map algebra isomorphism of $\operatorname{comm}$ applied to $R$, $B$ and $A$.

MonoidAlgebra.rTensorEquivAlgEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

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

English

Let $R$, $S$, $A$ and $B$ be sets. Then the tensor equivalence algebra isomorphism of $A$ and $B$ is an algebra isomorphism of the set of tensor products of $A$ and the set of monoid algebras of $B$ and $M$ and the set of monoid algebras of the set of tensor products of $A$ and $B$ and $M$.

MonoidAlgebra.scalarTensorEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the scalar tensor equivalence of $R$ and $A$ is an algebra isomorphism of the set of tensor products of $A$ and the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $A$ and $M$ defined as the composition of the tensor equivalence algebra isomorphism of $A$ and $R$ and the map algebra isomorphism of $\operatorname{rid}$ applied to $R$, $A$ and $A$.

MonoidAlgebra.tensorEquivdefMathlib.RingTheory.TensorProduct.MonoidAlgebra, function or constant

Wording

the tensor equivalence of R (from the name)

English

Let $R$ be a set. Then the tensor equivalence of $R$ is a linear equivalence of the set of tensor products of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and $N$ and the set of monoid algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ defined as the composition of the composition of the congruence of the coefficient linear equivalence of $R$ and the coefficient linear equivalence of $R$ and the finitely supported function tensor finitely supported function of $M$ and $N$ and the inverse of the coefficient linear equivalence of $R$.

Mathlib.RingTheory.TensorProduct.MvPolynomial

MvPolynomial.algebraTensorAlgEquivdefMathlib.RingTheory.TensorProduct.MvPolynomial, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the algebra tensor algebra isomorphism of $R$ and $A$ is an algebra isomorphism of the set of tensor products of $A$ and the set of multivariate polynomials of $x_{1}$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $A$ defined as the scalar tensor equivalence of $R$ and $A$.

MvPolynomial.rTensorAlgEquivdefMathlib.RingTheory.TensorProduct.MvPolynomial, function or constant

Wording

the algebra morphism (from the docstring)

English

The algebra morphism is an algebra isomorphism of the set of tensor products of $S$ and the set of multivariate polynomials of $x_{1}$ and $N$ and the set of multivariate polynomials of $x_{1}$ and the set of tensor products of $S$ and $N$ defined as the tensor equivalence algebra isomorphism of $S$ and $N$.

MvPolynomial.scalarRTensorAlgEquivdefMathlib.RingTheory.TensorProduct.MvPolynomial, function or constant

Wording

the tensor product of the polynomial algebra by an algebra (from the docstring)

English

The tensor product of the polynomial algebra by an algebra is an algebra isomorphism of the set of tensor products of $N$ and the set of multivariate polynomials of $x_{1}$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $N$ defined as the scalar tensor equivalence of $R$ and $N$.

MvPolynomial.tensorEquivSumdefMathlib.RingTheory.TensorProduct.MvPolynomial, function or constant

Wording

the tensor equivalence sum of x2 and S (from the name)

English

Let $R$, $x_{1}$, $x_{2}$ and $S$ be sets. Then the tensor equivalence sum of $x_{2}$ and $S$ is an algebra isomorphism of the set of tensor products of the set of multivariate polynomials of $x_{1}$ and $S$ and the set of multivariate polynomials of $x_{2}$ and $R$ and the set of multivariate polynomials of $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ and $S$ defined as the composition of $\operatorname{restrictScalars}$ applied to $S$ and the algebra tensor algebra isomorphism of $R$ and the set of multivariate polynomials of $x_{1}$ and $S$ and the composition of the inverse of the sum algebra isomorphism of $x_{2}$ and $x_{1}$ and $\operatorname{renameEquiv}$ applied to $S$ and $\operatorname{sumComm}$ applied to $x_{2}$ and $x_{1}$.

Mathlib.RingTheory.TensorProduct.Pi

Algebra.TensorProduct.piRightdefMathlib.RingTheory.TensorProduct.Pi, function or constant

Wording

the right product of B (from the name)

English

Let $R$, $S$ and $A$ be sets. Let $B$ be a function from elements of $x_{6}$ to sets. Then the right product of $B$ is an algebra isomorphism of the set of tensor products of $A$ and the set of functions from elements $i$ of $x_{6}$ to elements of $B$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{6}$ to tensor products of $A$ and $B$ applied to $i_{1}$.

Algebra.TensorProduct.piRightHomdefMathlib.RingTheory.TensorProduct.Pi, function or constant

Wording

the product right homomorphism of B (from the name)

English

Let $R$, $S$ and $A$ be sets. Let $B$ be a function from elements of $x_{6}$ to sets. Then the product right homomorphism of $B$ is an algebra homomorphism of the set of tensor products of $A$ and the set of functions from elements $i$ of $x_{6}$ to elements of $B$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{6}$ to tensor products of $A$ and $B$ applied to $i_{1}$.

Algebra.TensorProduct.piScalarRightdefMathlib.RingTheory.TensorProduct.Pi, function or constant

Wording

the right product scalar of A and x6 (from the name)

English

Let $R$, $S$, $A$ and $x_{6}$ be sets. Then the right product scalar of $A$ and $x_{6}$ is an algebra isomorphism of the set of tensor products of $A$ and the set of functions from elements of $x_{6}$ to elements of $R$ and the set of functions from elements of $x_{6}$ to elements of $A$ defined as the composition of the right product of the function that maps $x_{9}$ to $R$ and the right product congruence of the function that maps $x_{10}$ to $\operatorname{rid}$ applied to $R$, $S$ and $A$.

Algebra.TensorProduct.prodRightdefMathlib.RingTheory.TensorProduct.Pi, function or constant

Wording

the right product of B and C (from the name)

English

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

Mathlib.RingTheory.TensorProduct.Quotient

Algebra.TensorProduct.quotIdealMapEquivQuotTensordefMathlib.RingTheory.TensorProduct.Quotient, function or constant

Wording

the quotient ideal map equivalence quotient tensor of B and I (from the name)

English

Let $B$ be a set. Let $I$ be an ideal of $A$. Then the quotient ideal map equivalence quotient tensor of $B$ and $I$ is an algebra isomorphism of the set of quotients of $B$ and the map of the algebra map of $A$ and $B$ and $I$ and the set of tensor products of the set of quotients of $A$ and $I$ and $B$.

Algebra.TensorProduct.quotIdealMapEquivTensorQuotdefMathlib.RingTheory.TensorProduct.Quotient, function or constant

Wording

the quotient ideal map equivalence tensor quotient of B and I (from the name)

English

Let $B$ be a set. Let $I$ be an ideal of $A$. Then the quotient ideal map equivalence tensor quotient of $B$ and $I$ is an algebra isomorphism of the set of quotients of $B$ and the map of the algebra map of $A$ and $B$ and $I$ and the set of tensor products of $B$ and the set of quotients of $A$ and $I$.

Algebra.TensorProduct.quotientTensorEquivdefMathlib.RingTheory.TensorProduct.Quotient, function or constant

Wording

the quotient tensor equivalence of I (from the name)

English

Let $S$, $T$ and $A$ be sets. Let $I$ be an ideal of $A$. Then the quotient tensor equivalence of $I$ is an algebra isomorphism of the set of tensor products of the set of quotients of $A$ and $I$ and $T$ and the set of quotients of the set of tensor products of $A$ and $T$ and the map of the algebra map of $A$ and the set of tensor products of $A$ and $T$ and $I$.

Algebra.TensorProduct.tensorQuotientEquivdefMathlib.RingTheory.TensorProduct.Quotient, function or constant

Wording

the tensor quotient equivalence of I (from the name)

English

Let $S$, $T$ and $A$ be sets. Let $I$ be an ideal of $T$. Then the tensor quotient equivalence of $I$ is an algebra isomorphism of the set of tensor products of $A$ and the set of quotients of $T$ and $I$ and the set of quotients of the set of tensor products of $A$ and $T$ and the map of $\operatorname{includeRight}$ and $I$.

Algebra.tensorQuotientTensorEquivdefMathlib.RingTheory.TensorProduct.Quotient, function or constant

Wording

the tensor quotient tensor equivalence of e and #2 (from the name)

English

Let $\mathrm{R''}$ be a set. Let $e$ be a tensor product of $\mathrm{R'}$ and $S$. Then the tensor quotient tensor equivalence of $\mathrm{R''}$ and $e$ is an algebra isomorphism of the set of tensor products of $\mathrm{R''}$ and the set of quotients of the set of tensor products of $\mathrm{R'}$ and $S$ and the span of $\operatorname{singleton}$ applied to $e$ and the set of quotients of the set of tensor products of $\mathrm{R''}$ and $S$ and the span of $\operatorname{singleton}$ applied to $\operatorname{rTensor}$ applied to $S$, the algebra of $\mathrm{R'}$ and $\mathrm{R''}$ and $e$.

Mathlib.RingTheory.TotallySplit

Algebra.IsFiniteSplitclassMathlib.RingTheory.TotallySplit, predicate

Wording

no wording

English

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

Algebra.IsFiniteSplit.algHomEquivPrimeSpectrumdefMathlib.RingTheory.TotallySplit, function or constant

Wording

the algebra homomorphism equivalence prime spectrum of k and R (from the name)

English

Let $k$ and $R$ be sets. Then the algebra homomorphism equivalence prime spectrum of $k$ and $R$ is an equivalence from the set of algebra homomorphisms of $R$ and $k$ to the set of prime spectra of $R$.

Mathlib.RingTheory.Trace.Basic

Algebra.embeddingsMatrixdefMathlib.RingTheory.Trace.Basic, function or constant

Wording

the embedding matrix of b (from the name)

English

Let $A$ and $C$ be sets. Let $b$ be a function from elements of $x$ to elements of $B$. Then the embedding matrix of $b$ is a matrix of the set of algebra homomorphisms of $B$ and $C$ and $C$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $x_{7}$ to $x_{7}$ applied to $b$ applied to $i_{1}$.

Algebra.embeddingsMatrixReindexdefMathlib.RingTheory.Trace.Basic, function or constant

Wording

the embedding matrix reindexing of b and e (from the name)

English

Let $A$ and $C$ be sets. Let $b$ be a function from elements of $x$ to elements of $B$. Let $e$ be an equivalence from $x$ to the set of algebra homomorphisms of $B$ and $C$. Then the embedding matrix reindexing of $b$ and $e$ is a matrix of $x$ and $C$ defined as $\operatorname{reindex}$ applied to the identity of $x$, the inverse of $e$ and the embedding matrix of $b$.

Algebra.traceMatrixdefMathlib.RingTheory.Trace.Basic, function or constant

Wording

the trace matrix of A and b (from the name)

English

Let $A$ be a set. Let $b$ be a function from elements of $x$ to elements of $B$. Then the trace matrix of $A$ and $b$ is a matrix of $x$ and $A$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\operatorname{coe}$ applied to the trace form of $A$ and $B$, $b$ applied to $i_{1}$ and $b$ applied to $j_{1}$.

Module.Basis.traceDualdefMathlib.RingTheory.Trace.Basic, function or constant

Wording

the dual basis of b (from the docstring)

English

Let $b$ be a basis of $K$ and $L$. Then the dual basis of $b$ is a basis of $K$ and $L$ defined as the dual basis of the trace form of $K$ and $L$ and $b$.

Mathlib.RingTheory.Trace.Defs

Algebra.tracedefMathlib.RingTheory.Trace.Defs, function or constant

Wording

the trace of R and S (from the docstring)

English

Let $R$ and $S$ be sets. Then the trace of $R$ and $S$ is a linear map of $S$ and $R$ defined as the composition of the trace of $R$ and $S$ and the linear map of $\operatorname{lmul}$ applied to $R$ and $S$.

Algebra.traceFormdefMathlib.RingTheory.Trace.Defs, function or constant

Wording

the trace form of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the trace form of $R$ and $S$ is a bilinear form of $R$ and $S$ defined as $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to the linear map of $\operatorname{lmul}$ applied to $R$ and $S$ and the trace of $R$ and $S$.

Mathlib.RingTheory.TwoSidedIdeal.Basic

TwoSidedIdealstructureMathlib.RingTheory.TwoSidedIdeal.Basic, type

Wording

no wording

English

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

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

Wording

the coercion into the ring of I (from the docstring)

English

Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then the coercion into the ring of $I$ is an additive monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ and $R$.

TwoSidedIdeal.coeOrderEmbeddingdefMathlib.RingTheory.TwoSidedIdeal.Basic, function or constant

Wording

the coercion order embedding (from the name)

English

The coercion order embedding is an order embedding of $\mathrm{TwoSidedIdeal}$ applied to $R$ and $\wp R$.

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

Wording

no wording

English

Let $\mathrm{carrier}$ be an element of $\wp R$ such that $0$ is an element of $\mathrm{carrier}$, for all elements $x_{4}$ of $R$, for all elements $y_{2}$ of $R$, if $x_{4}$ is an element of $\mathrm{carrier}$, then if $y_{2}$ is an element of $\mathrm{carrier}$, then $\MembershipmemMACRoT {\mathrm{carrier}}{x_{4} + y_{2}}$, for all elements $x_{3}$ of $R$, if $x_{3}$ is an element of $\mathrm{carrier}$, then $\MembershipmemMACRoT {\mathrm{carrier}}{\operatorname{neg} (x_{3})}$, for all elements $x_{2}$ of $R$, for all elements $y_{1}$ of $R$, if $y_{1}$ is an element of $\mathrm{carrier}$, then $\MembershipmemMACRoT {\mathrm{carrier}}{x_{2} \times y_{1}}$ and for all elements $x_{1}$ of $R$, for all elements $y$ of $R$, if $x_{1}$ is an element of $\mathrm{carrier}$, then $\MembershipmemMACRoT {\mathrm{carrier}}{x_{1} \times y}$. Then $\operatorname{mk'}$ applied to $\mathrm{carrier}$, $\mathrm{zero\_mem}$, $\mathrm{add\_mem}$, $\mathrm{neg\_mem}$, $\mathrm{mul\_mem\_left}$ and $\mathrm{mul\_mem\_right}$ is an element of $\mathrm{TwoSidedIdeal}$ applied to $R$.

TwoSidedIdeal.opdefMathlib.RingTheory.TwoSidedIdeal.Basic, function or constant

Wording

the opposite of I (from the name)

English

Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then the opposite of $I$ is an element of $\mathrm{TwoSidedIdeal}$ applied to the set of multiplicative opposites of $R$ defined as $\operatorname{ofRingCon}$ applied to the opposite of the ring congruence relation of $I$.

TwoSidedIdeal.opOrderIsodefMathlib.RingTheory.TwoSidedIdeal.Basic, function or constant

Wording

the opposite order isomorphism (from the name)

English

The opposite order isomorphism is an order isomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and $\mathrm{TwoSidedIdeal}$ applied to the set of multiplicative opposites of $R$.

TwoSidedIdeal.orderIsoRingCondefMathlib.RingTheory.TwoSidedIdeal.Basic, function or constant

Wording

the order isomorphism ring congruence relation (from the name)

English

The order isomorphism ring congruence relation is an order isomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and the set of ring congruence relations of $R$.

TwoSidedIdeal.ringCondefMathlib.RingTheory.TwoSidedIdeal.Basic, function or constant

Wording

the ring congruence relation of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then the ring congruence relation of $\mathrm{self}$ is a ring congruence relation of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

TwoSidedIdeal.unopdefMathlib.RingTheory.TwoSidedIdeal.Basic, function or constant

Wording

the opposite of I (from the name)

English

Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to the set of multiplicative opposites of $R$. Then the opposite of $I$ is an element of $\mathrm{TwoSidedIdeal}$ applied to $R$ defined as $\operatorname{ofRingCon}$ applied to the opposite of the ring congruence relation of $I$.

Mathlib.RingTheory.TwoSidedIdeal.Kernel

TwoSidedIdeal.kerdefMathlib.RingTheory.TwoSidedIdeal.Kernel, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be an element of $F$. Then the kernel of $f$ is an element of $\mathrm{TwoSidedIdeal}$ applied to $R$.

Mathlib.RingTheory.TwoSidedIdeal.Operations

Ideal.toTwoSideddefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

Let $I$ be an ideal of $R$. Then $\operatorname{toTwoSided}$ applied to $I$ is an element of $\mathrm{TwoSidedIdeal}$ applied to $R$.

RingEquiv.mapTwoSidedIdealdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then $\operatorname{mapTwoSidedIdeal}$ applied to $e$ is an order isomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and $\mathrm{TwoSidedIdeal}$ applied to $S$.

TwoSidedIdeal.asIdealdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

$\operatorname{asIdeal}$ is an order homomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and the set of ideals of $R$.

TwoSidedIdeal.asIdealOppositedefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

$\operatorname{asIdealOpposite}$ is an order homomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and the set of ideals of the set of multiplicative opposites of $R$.

TwoSidedIdeal.comapdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

the preimage of f (from the name)

English

Let $f$ be an element of $F$. Then the preimage of $f$ is an order homomorphism of $\mathrm{TwoSidedIdeal}$ applied to $S$ and $\mathrm{TwoSidedIdeal}$ applied to $R$.

TwoSidedIdeal.fromIdealdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

$\operatorname{fromIdeal}$ is an order homomorphism of the set of ideals of $R$ and $\mathrm{TwoSidedIdeal}$ applied to $R$.

TwoSidedIdeal.mapdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

the map of f and I (from the name)

English

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

TwoSidedIdeal.orderIsoIdealdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

the order isomorphism ideal (from the name)

English

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

TwoSidedIdeal.orderIsoIsTwoSideddefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

$\operatorname{orderIsoIsTwoSided}$ is an order isomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and $\SubtypeSet {I}{\operatorname{IsTwoSided} (I)}$.

TwoSidedIdeal.spandefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

the span of s (from the name)

English

Let $s$ be an element of $\wp R$. Then the span of $s$ is an element of $\mathrm{TwoSidedIdeal}$ applied to $R$ defined as $\operatorname{ofRingCon}$ applied to the ring congruence relation generator of the function that maps $a$ and $b$ to $\MembershipmemMACRoT {s}{(a - b)}$.

TwoSidedIdeal.subtypedefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

the subtype of I (from the name)

English

Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then the subtype of $I$ is a linear map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ and $R$.

TwoSidedIdeal.subtypeMopdefMathlib.RingTheory.TwoSidedIdeal.Operations, function or constant

Wording

no wording

English

Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then $\operatorname{subtypeMop}$ applied to $I$ is a linear map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ and the set of multiplicative opposites of $R$.

Mathlib.RingTheory.UniqueFactorizationDomain.Defs

UniqueFactorizationMonoidclassMathlib.RingTheory.UniqueFactorizationDomain.Defs, predicate

Wording

x is a unique factorization monoid (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a unique factorization monoid.

UniqueFactorizationMonoid.factorsdefMathlib.RingTheory.UniqueFactorizationDomain.Defs, function or constant

Wording

the factor of a (from the name)

English

Let $a$ be an element of $x$. Then the factor of $a$ is a multiset of $x$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {a}{0}$, the function that maps $h_{1}$ to $0$ and the function that maps $h_{2}$ to $\operatorname{choose}$ applied to $\mathrm{UniqueFactorizationMonoid\_\_exists\_prime\_factors}$ applied to $a$ and $h_{2}$.

WfDvdMonoiddefMathlib.RingTheory.UniqueFactorizationDomain.Defs, predicate

Wording

no wording

English

Let $x$ be a set. Then $\mathrm{WfDvdMonoid}$ holds for $x$, if $\mathrm{WellFounded}$ holds for $\mathrm{DvdNotUnit}$.

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Associates.BfactorSetMemdefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, predicate

Wording

no wording

English

Let $x_{2}$ be an element of $\SubtypeSet {a}{\mathrm{Irreducible} (a)}$. Let $x_{3}$ be a factor set of $x$. Then we can say that $\operatorname{BfactorSetMem}$ holds for $x_{2}$ and $x_{3}$.

Associates.FactorSetdefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, type

Wording

factor set of x (from the name)

English

Let $x$ be a set. Then a factor set of $x$ is an element of the function that maps $x$ to $\mathrm{WithTop}$ applied to the set of multisets of $\SubtypeSet {a}{\mathrm{Irreducible} (a)}$.

Associates.FactorSet.proddefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, function or constant

Wording

the product of x2 (from the name)

English

Let $x_{2}$ be a factor set of $x$. Then the product of $x_{2}$ is an associate of $x$.

Associates.FactorSetMemdefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, predicate

Wording

no wording

English

Let $s$ be a factor set of $x$. Let $p$ be an associate of $x$. Then $\operatorname{FactorSetMem}$ holds for $s$ and $p$, if $\mathrm{dite}$ holds for the proposition that $p$ is irreducible, the function that maps $\mathrm{hp}$ to $\operatorname{BfactorSetMem}$ applied to $p$ and $s$ and the function that maps $\mathrm{hp1}$ to the proposition that we have a contradiction.

Associates.bcountdefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, function or constant

Wording

no wording

English

Let $p$ be an element of $\SubtypeSet {a}{\mathrm{Irreducible} (a)}$. Let $x_{3}$ be a factor set of $x$. Then $\operatorname{bcount}$ applied to $p$ and $x_{3}$ is an element of $\Natural$.

Associates.countdefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, function or constant

Wording

the count of p and x4 (from the name)

English

Let $p$ be an associate of $x$. Let $x_{4}$ be a factor set of $x$. Then the count of $p$ and $x_{4}$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that $p$ is irreducible, the function that maps $\mathrm{hp}$ to $\operatorname{bcount}$ applied to $p$, the function that maps $\mathrm{hp1}$ to $0$ and $x_{4}$.

Associates.factorsdefMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, function or constant

Wording

the factor of a (from the name)

English

Let $a$ be an associate of $x$. Then the factor of $a$ is a factor set of $x$.

Associates.factors'defMathlib.RingTheory.UniqueFactorizationDomain.FactorSet, function or constant

Wording

the factor of a (from the name)

English

Let $a$ be an element of $x$. Then the factor of $a$ is a multiset of $\SubtypeSet {a_{1}}{\mathrm{Irreducible} (a_{1})}$ defined as $\operatorname{pmap}$ applied to the function that maps $a_{1}$ and $\mathrm{ha}$ to $\operatorname{mk}$ applied to $a_{1}$, the factor of $a$ and $\mathrm{UniqueFactorizationMonoid\_\_irreducible\_of\_factor}$.

Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

factorizationdefMathlib.RingTheory.UniqueFactorizationDomain.Finsupp, function or constant

Wording

the factorization of n (from the name)

English

Let $n$ be an element of $x$. Then the factorization of $n$ is an element of $\FinsuppMACRoQ {x}{\Natural}$ defined as $\operatorname{toFinsupp}$ applied to the normalized factor of $n$.

Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

UniqueFactorizationMonoid.moebiusdefMathlib.RingTheory.UniqueFactorizationDomain.Moebius, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{moebius}$ applied to $a$ is an element of $\Integer$ defined as $\iteMACRoG {\mathrm{Squarefree} (a)}{(\operatorname{neg} (1)^ {\operatorname{card} (\operatorname{factors} (a))})}{0}$.

Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

UniqueFactorizationMonoid.normalizedFactorsdefMathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors, function or constant

Wording

the normalized factor of a (from the name)

English

Let $a$ be an element of $x$. Then the normalized factor of $a$ is a multiset of $x$ defined as the map of $\mathrm{normalize}$ and the factor of $a$.

UniqueFactorizationMonoid.normalizedFactorsEquivdefMathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors, function or constant

Wording

the normalized factor equivalence of he and a (from the name)

English

Assume that for all elements $x_{8}$ of $x$, $\EqtMACRoH {\mathrm{normalize} (f (x_{8}))}{f (\mathrm{normalize} (x_{8}))}$. Let $a$ be an element of $x$. Then the normalized factor equivalence of $\mathrm{he}$ and $a$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{normalizedFactors} (a)}{x_{7}})})}{(\SubtypeSet {y}{(\MembershipmemMACRoT {\operatorname{normalizedFactors} (f (a))}{y})})}$.

Mathlib.RingTheory.Unramified.Basic

Algebra.FormallyUnramifiedclassMathlib.RingTheory.Unramified.Basic, predicate

Wording

A is formally unramified with respect to R (from the name)

English

generation took over the time limit

Algebra.UnramifiedclassMathlib.RingTheory.Unramified.Basic, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Unramified.Finite

Algebra.FormallyUnramified.elemdefMathlib.RingTheory.Unramified.Finite, function or constant

Wording

the element of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the element of $R$ and $S$ is a tensor product of $S$ and $S$.

Algebra.FormallyUnramified.secdefMathlib.RingTheory.Unramified.Finite, function or constant

Wording

no wording

English

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

Mathlib.RingTheory.Unramified.LocalStructure

HasStandardEtaleSurjectionOndefMathlib.RingTheory.Unramified.LocalStructure, predicate

Wording

no wording

English

Let $R$ be a set. Let $f$ be an element of $S$. Then $\mathrm{HasStandardEtaleSurjectionOn}$ holds for $R$ and $f$, if there exists a standard etale pair $P$ of $R$, such that there exists an algebra homomorphism $x_{3}$ of the set of rings of $P$ and $\operatorname{Away}$ applied to $f$, such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{3}$.

Mathlib.RingTheory.Unramified.Locus

Algebra.IsUnramifiedAtdefMathlib.RingTheory.Unramified.Locus, predicate

Wording

no wording

English

generation took over the time limit

Algebra.IsUnramifiedIndefMathlib.RingTheory.Unramified.Locus, predicate

Wording

no wording

English

Let $A$ be a set. Let $x_{3}$ be an ideal of $R$. Then $\operatorname{IsUnramifiedIn}$ holds for $A$ and $x_{3}$, if for all ideals $x_{4}$ of $A$, for all elements $h$ of $\mathrm{Proof}$ applied to the proposition that $x_{4}$ is prime, if $\operatorname{LiesOver}$ holds for $x_{4}$ and $x_{3}$, then $\operatorname{IsUnramifiedAt}$ holds for $R$ and $x_{4}$.

Algebra.unramifiedLocusdefMathlib.RingTheory.Unramified.Locus, function or constant

Wording

the unramified locus of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the unramified locus of $R$ and $A$ is an element of the power set of the set of prime spectra of $A$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\operatorname{IsUnramifiedAt}$ applied to $R$ and $\operatorname{asIdeal}$ applied to $p$.

Mathlib.RingTheory.Valuation.AlgebraInstances

ValuationSubring.equivdefMathlib.RingTheory.Valuation.AlgebraInstances, function or constant

Wording

the equivalence of v (from the name)

English

Let $v$ be a valuation of $K$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$. Let $L$ and $R$ be sets. Then the equivalence of $v$ is a ring isomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{valuationSubring} (v)}{x_{7}})}, L)}{x_{6}})}$ and $R$ defined as the ring isomorphism of the inverse of the equivalence of $L$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{valuationSubring} (v)}{x_{8}})}, L)}{x_{7}})}$.

Mathlib.RingTheory.Valuation.Basic

AddValuationdefMathlib.RingTheory.Valuation.Basic, type

Wording

additive valuation of R and x1 (from the name)

English

Let $R$ and $x_{1}$ be sets. Then an additive valuation of $R$ and $x_{1}$ is an element of the function that maps $R$ and $x_{1}$ to the set of valuations of $R$ and the set of multiplicatives of the set of order duals of $x_{1}$.

AddValuation.IsEquivdefMathlib.RingTheory.Valuation.Basic, predicate

Wording

no wording

English

Let $x_{5}$ be an additive valuation of $R$ and $x$. Let $x_{6}$ be an additive valuation of $R$ and $x_{1}$. Then $\operatorname{IsEquiv}$ holds for $x_{5}$ and $x_{6}$, if $\operatorname{IsEquiv}$ holds for $x_{5}$ and $x_{6}$.

AddValuation.comapdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the preimage of f and v (from the name)

English

Let $f$ be a ring homomorphism of $S$ and $R$. Let $v$ be an additive valuation of $R$ and $x$. Then the preimage of $f$ and $v$ is an additive valuation of $S$ and $x$ defined as the preimage of $f$ and $v$.

AddValuation.mapdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the map of f and v (from the name)

English

Let $f$ be an order additive monoid homomorphism of $x$ and $x_{1}$ such that $f$ applied to the top is equal to the top. Let $v$ be an additive valuation of $R$ and $x$. Then the map of $f$ and $v$ is an additive valuation of $R$ and $x_{1}$.

AddValuation.ofdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $R$ to elements of $x$ such that $f$ applied to $0$ is equal to the top, $\EqtMACRoH {f (1)}{0}$, for all elements $x_{4}$ of $R$, for all elements $y_{1}$ of $R$, $\MinminMACRoAG {f (x_{4})}{f (y_{1})}\leq f (x_{4} + y_{1})$ and for all elements $x_{3}$ of $R$, for all elements $y$ of $R$, $\EqtMACRoH {f (x_{3} \times y)}{f (x_{3})+ f (y)}$. Then $\operatorname{of}$ applied to $f$, $h_{0}$, $h_{1}$, $\mathrm{hadd}$ and $\mathrm{hmul}$ is an additive valuation of $R$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $h_{0}$, $h_{1}$ and $\mathrm{hmul}$ and $\mathrm{hadd}$.

AddValuation.ofValuationdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the additive valuation (from the name)

English

The additive valuation is an equivalence from the set of valuations of $R$ and the set of multiplicatives of the set of order duals of $x$ to the set of additive valuations of $R$ and $x$ defined as the identity of the set of valuations of $R$ and the set of multiplicatives of the set of order duals of $x$.

AddValuation.suppdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the support of v (from the docstring)

English

Let $v$ be an additive valuation of $R$ and $x$. Then the support of $v$ is an ideal of $R$ defined as the support of $v$.

AddValuation.toValuationdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the valuation (from the name)

English

The valuation is an equivalence from the set of additive valuations of $R$ and $x$ to the set of valuations of $R$ and the set of multiplicatives of the set of order duals of $x$ defined as the identity of the set of additive valuations of $R$ and $x$.

ValuationstructureMathlib.RingTheory.Valuation.Basic, type

Wording

valuation of R and x (from the name)

English

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

Valuation.IsEquivdefMathlib.RingTheory.Valuation.Basic, predicate

Wording

no wording

English

Let $x_{5}$ be a valuation of $R$ and $x$. Let $x_{6}$ be a valuation of $R$ and $x_{1}$. Then $\operatorname{IsEquiv}$ holds for $x_{5}$ and $x_{6}$, if for all elements $r$ and $s$ of $R$, $x_{5} (r)\leq x_{5} (s)$, if and only if $x_{6} (r)\leq x_{6} (s)$.

Valuation.IsEquiv.orderMonoidIsodefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the order monoid isomorphism of h (from the name)

English

Assume that $\operatorname{IsEquiv}$ holds for $v$ and $w$. Then the order monoid isomorphism of $h$ is an order monoid isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (v))}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (w))}{x_{6}})}$.

Valuation.IsEquiv.orderMonoidIso₀defMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the order monoid isomorphism of h (from the name)

English

Assume that $\operatorname{IsEquiv}$ holds for $v$ and $w$. Then the order monoid isomorphism of $h$ is an order monoid isomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $w$ defined as $\operatorname{withZero}$ applied to the order monoid isomorphism of $h$.

Valuation.IsEquiv.valueGroupFundefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the value group function of h and x5 (from the name)

English

Assume that $\operatorname{IsEquiv}$ holds for $v$ and $w$. Let $x_{5}$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (v))}{x_{7}})}$. Then the value group function of $h$ and $x_{5}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (w))}{x_{6}})}$.

Valuation.IsNontrivialclassMathlib.RingTheory.Valuation.Basic, predicate

Wording

v is nontrivial (from the docstring)

English

Let $v$ be a valuation of $R$ and $x$. Then we can say that $v$ is nontrivial.

Valuation.IsTrivialOnclassMathlib.RingTheory.Valuation.Basic, predicate

Wording

no wording

English

Let $A$ be a set. Let $v$ be a valuation of $B$ and $x$. Then we can say that $\operatorname{IsTrivialOn}$ holds for $A$ and $v$.

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

Wording

the preimage of f and v (from the name)

English

Let $f$ be a ring homomorphism of $S$ and $R$. Let $v$ be a valuation of $R$ and $x$. Then the preimage of $f$ and $v$ is a valuation of $S$ and $x$.

Valuation.congrdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the congruence of f (from the name)

English

Let $f$ be an order monoid isomorphism of $x$ and $x_{1}$. Then the congruence of $f$ is an equivalence from the set of valuations of $R$ and $x$ to the set of valuations of $R$ and $x_{1}$.

Valuation.leAddSubgroupdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $x_{3}$ be an element of $x$. Then $\operatorname{leAddSubgroup}$ applied to $v$ and $x_{3}$ is an additive subgroup of $R$.

Valuation.ltAddSubgroupdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $x_{3}$ be a unit of $x$. Then $\operatorname{ltAddSubgroup}$ applied to $v$ and $x_{3}$ is an additive subgroup of $R$.

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

Wording

the map of f and v (from the name)

English

Let $f$ be an order monoid with zero homomorphism of $x$ and $x_{1}$. Let $v$ be a valuation of $R$ and $x$. Then the map of $f$ and $v$ is a valuation of $R$ and $x_{1}$.

Valuation.ofAddValuationdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the valuation (from the name)

English

The valuation is an equivalence from the set of additive valuations of $R$ and the set of order duals of $\mathrm{Additive}$ applied to $x$ to the set of valuations of $R$ and $x$.

Valuation.restrictdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the restriction of v (from the docstring)

English

Let $v$ be a valuation of $R$ and $x$. Then the restriction of $v$ is a valuation of $R$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$.

Valuation.suppdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the support of v (from the docstring)

English

Let $v$ be a valuation of $R$ and $x$. Then the support of $v$ is an ideal of $R$.

Valuation.toAddValuationdefMathlib.RingTheory.Valuation.Basic, function or constant

Wording

the additive valuation (from the name)

English

The additive valuation is an equivalence from the set of valuations of $R$ and $x$ to the set of additive valuations of $R$ and the set of order duals of $\mathrm{Additive}$ applied to $x$.

ValuationClassclassMathlib.RingTheory.Valuation.Basic, predicate

Wording

no wording

English

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

Mathlib.RingTheory.Valuation.Discrete.Basic

Valuation.IsRankOneDiscreteclassMathlib.RingTheory.Valuation.Discrete.Basic, predicate

Wording

no wording

English

Let $v$ be a valuation of $A$ and $x$. Then we can say that $\operatorname{IsRankOneDiscrete}$ holds for $v$.

Valuation.IsRankOneDiscrete.generatordefMathlib.RingTheory.Valuation.Discrete.Basic, function or constant

Wording

the generator of v (from the name)

English

Let $v$ be a valuation of $A$ and $x$. Then the generator of $v$ is a unit of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{Valuation\_\_IsRankOneDiscrete\_\_exists\_generator\_lt\_one}$ applied to $v$.

Valuation.IsRankOneDiscrete.generator'defMathlib.RingTheory.Valuation.Discrete.Basic, function or constant

Wording

the generator of v (from the name)

English

Let $v$ be a valuation of $A$ and $x$. Then the generator of $v$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (v))}{x_{3}})}$ defined as the generator of $v$.

Valuation.IsUniformizerdefMathlib.RingTheory.Valuation.Discrete.Basic, predicate

Wording

no wording

English

Let $v$ be a valuation of $A$ and $x$. Let $x_{3}$ be an element of $A$. Then $\operatorname{IsUniformizer}$ holds for $v$ and $x_{3}$, if $v$ applied to $x_{3}$ is equal to the underlying value in the base of the generator of $v$.

Valuation.UniformizerstructureMathlib.RingTheory.Valuation.Discrete.Basic, type

Wording

uniformizer of v (from the name)

English

Let $v$ be a valuation of $A$ and $x$. Then the uniformizers of $v$ are a basic type.

Valuation.Uniformizer.mk'defMathlib.RingTheory.Valuation.Discrete.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{IsUniformizer}$ holds for $v$ and $x_{3}$. Then $\operatorname{mk'}$ applied to $\mathrm{hx}$ is a uniformizer of $v$ defined as $\operatorname{mk}$ applied to $x_{3}$ and $\mathrm{hx}$.

Valuation.Uniformizer.valdefMathlib.RingTheory.Valuation.Discrete.Basic, function or constant

Wording

the value of self (from the name)

English

Let $\mathrm{self}$ be a uniformizer of $v$. Then the value of $\mathrm{self}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{integer} (v)}{x_{3}})}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

IsDiscreteValuationRing.equivValuationSubringdefMathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing, function or constant

Wording

the equivalence valuation subring (from the name)

English

The equivalence valuation subring is a ring isomorphism of $A$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{valuationSubring} (\operatorname{valuation} (K , \operatorname{maximalIdeal} (A)))}{x_{3}})}$.

IsDiscreteValuationRing.maximalIdealdefMathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing, function or constant

Wording

the maximal ideal of A (from the docstring)

English

Let $A$ be a set. Then the maximal ideal of $A$ is a height one spectrum of $A$.

Mathlib.RingTheory.Valuation.Discrete.RankOne

Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulIntdefMathlib.RingTheory.Valuation.Discrete.RankOne, function or constant

Wording

the value group equivalence with zero multiplicative integer of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the value group equivalence with zero multiplicative integer of $v$ is an order monoid isomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$.

Mathlib.RingTheory.Valuation.ExtendToLocalization

Valuation.extendToLocalizationdefMathlib.RingTheory.Valuation.ExtendToLocalization, function or constant

Wording

no wording

English

Let $v$ be a valuation of $A$ and $x_{1}$ such that $S$ is less than or equal to the complement of the support of $v$. Let $B$ be a set. Then $\operatorname{extendToLocalization}$ applied to $v$, $\mathrm{hS}$ and $B$ is a valuation of $B$ and $x_{1}$.

Mathlib.RingTheory.Valuation.Extension

Valuation.HasExtensionclassMathlib.RingTheory.Valuation.Extension, predicate

Wording

no wording

English

Let $\mathrm{vR}$ be a valuation of $R$ and $x$. Let $\mathrm{vA}$ be a valuation of $A$ and $x_{1}$. Then we can say that $\operatorname{HasExtension}$ holds for $\mathrm{vR}$ and $\mathrm{vA}$.

Valuation.HasExtension.mapValueGroup₀defMathlib.RingTheory.Valuation.Extension, function or constant

Wording

the map value group of vR and vA (from the name)

English

Let $\mathrm{vR}$ be a valuation of $R$ and $x_{3}$. Let $\mathrm{vA}$ be a valuation of $A$ and $x_{4}$. Then the map value group of $\mathrm{vR}$ and $\mathrm{vA}$ is an order monoid with zero homomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $\mathrm{vR}$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $\mathrm{vA}$.

Mathlib.RingTheory.Valuation.Integers

Valuation.IntegersstructureMathlib.RingTheory.Valuation.Integers, predicate

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $O$ be a set. Then we can say that $\operatorname{Integers}$ holds for $v$ and $O$.

Valuation.integerdefMathlib.RingTheory.Valuation.Integers, function or constant

Wording

the integer of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the integer of $v$ is a subring of $R$.

Valuation.leIdealdefMathlib.RingTheory.Valuation.Integers, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $x_{3}$ be an element of $x$. Then $\operatorname{leIdeal}$ applied to $v$ and $x_{3}$ is an ideal of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{integer} (v)}{x_{4}})}$.

Valuation.leSubmoduledefMathlib.RingTheory.Valuation.Integers, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $x_{3}$ be an element of $x$. Then $\operatorname{leSubmodule}$ applied to $v$ and $x_{3}$ is a submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{integer} (v)}{x_{4}})}$ and $R$.

Valuation.ltIdealdefMathlib.RingTheory.Valuation.Integers, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $x_{3}$ be an element of $\UnitsMACRoAO {x}$. Then $\operatorname{ltIdeal}$ applied to $v$ and $x_{3}$ is an ideal of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{integer} (v)}{x_{4}})}$.

Valuation.ltSubmoduledefMathlib.RingTheory.Valuation.Integers, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Let $x_{3}$ be an element of $\UnitsMACRoAO {x}$. Then $\operatorname{ltSubmodule}$ applied to $v$ and $x_{3}$ is a submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{integer} (v)}{x_{4}})}$ and $R$.

Mathlib.RingTheory.Valuation.LocalSubring

ValuationSubring.toLocalSubringdefMathlib.RingTheory.Valuation.LocalSubring, function or constant

Wording

the local subring of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the local subring of $A$ is a local subring of $K$ defined as $\operatorname{mk}$ applied to $\operatorname{toSubring}$ applied to $A$.

Mathlib.RingTheory.Valuation.PrimeMultiplicity

multiplicity_addValuationdefMathlib.RingTheory.Valuation.PrimeMultiplicity, function or constant

Wording

the multiplicity additive valuation of hp (from the name)

English

Assume that $p$ is prime. Then the multiplicity additive valuation of $\mathrm{hp}$ is an additive valuation of $R$ and the set of natural numbers.

Mathlib.RingTheory.Valuation.Quotient

AddValuation.onQuotdefMathlib.RingTheory.Valuation.Quotient, function or constant

Wording

no wording

English

Let $v$ be an additive valuation of $R$ and $x$ such that $J$ is less than or equal to the support of $v$. Then $\operatorname{onQuot}$ applied to $v$ and $\mathrm{hJ}$ is an additive valuation of the set of quotients of $R$ and $J$ and $x$ defined as $\operatorname{onQuot}$ applied to $v$ and $\mathrm{hJ}$.

AddValuation.onQuotValdefMathlib.RingTheory.Valuation.Quotient, function or constant

Wording

no wording

English

Let $v$ be an additive valuation of $R$ and $x$ such that $J$ is less than or equal to the support of $v$. Let $x_{3}$ be a quotient of $R$ and $J$. Then $\operatorname{onQuotVal}$ applied to $v$, $\mathrm{hJ}$ and $x_{3}$ is an element of $x$ defined as $\operatorname{onQuotVal}$ applied to $v$, $\mathrm{hJ}$ and $x_{3}$.

Valuation.onQuotdefMathlib.RingTheory.Valuation.Quotient, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$ such that $J$ is less than or equal to the support of $v$. Then $\operatorname{onQuot}$ applied to $v$ and $\mathrm{hJ}$ is a valuation of the set of quotients of $R$ and $J$ and $x$.

Valuation.onQuotValdefMathlib.RingTheory.Valuation.Quotient, function or constant

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$ such that $J$ is less than or equal to the support of $v$. Let $x_{3}$ be a quotient of $R$ and $J$. Then $\operatorname{onQuotVal}$ applied to $v$, $\mathrm{hJ}$ and $x_{3}$ is an element of $x$.

Mathlib.RingTheory.Valuation.RamificationGroup

ValuationSubring.decompositionSubgroupdefMathlib.RingTheory.Valuation.RamificationGroup, function or constant

Wording

the decomposition subgroup of K and A (from the name)

English

Let $K$ be a set. Let $A$ be a valuation subring of $L$. Then the decomposition subgroup of $K$ and $A$ is a subgroup of the set of algebra isomorphisms of $L$ and $L$ defined as the stabilizer of the set of algebra isomorphisms of $L$ and $L$ and $A$.

ValuationSubring.inertiaSubgroupdefMathlib.RingTheory.Valuation.RamificationGroup, function or constant

Wording

the inertia subgroup of K and A (from the name)

English

Let $K$ be a set. Let $A$ be a valuation subring of $L$. Then the inertia subgroup of $K$ and $A$ is a subgroup of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{decompositionSubgroup} (K , A)}{x_{3}})}$ defined as the multiplicative kernel of the ring automorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{decompositionSubgroup} (K , A)}{x_{3}})}$ and the set of residue fields of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$.

ValuationSubring.subMulActiondefMathlib.RingTheory.Valuation.RamificationGroup, function or constant

Wording

the difference multiplicative action of K and A (from the name)

English

Let $K$ be a set. Let $A$ be a valuation subring of $L$. Then the difference multiplicative action of $K$ and $A$ is a difference multiplicative action of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{decompositionSubgroup} (K , A)}{x_{3}})}$ and $L$.

Mathlib.RingTheory.Valuation.RankOne

Valuation.RankLeOneclassMathlib.RingTheory.Valuation.RankOne, predicate

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Then we can say that $\operatorname{RankLeOne}$ holds for $v$.

Valuation.RankLeOne.hom'defMathlib.RingTheory.Valuation.RankOne, function or constant

Wording

the homomorphism of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the homomorphism of $v$ is a monoid with zero homomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$ and $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Valuation.RankOneclassMathlib.RingTheory.Valuation.RankOne, predicate

Wording

v is a rank one (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then we can say that $v$ is a rank one.

Valuation.RankOne.homdefMathlib.RingTheory.Valuation.RankOne, function or constant

Wording

the homomorphism of v (from the name)

English

Valuation.RankOne.rankLeOneStructdefMathlib.RingTheory.Valuation.RankOne, function or constant

Wording

no wording

English

Assume that the valuation of $R$ is a rank one. Then $\operatorname{rankLeOneStruct}$ applied to $e$ is an element of $\operatorname{RankLeOneStruct}$ applied to $R$.

Valuation.RankOne.unitdefMathlib.RingTheory.Valuation.RankOne, function or constant

Wording

the unit of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the unit of $v$ is a unit of $x$.

Mathlib.RingTheory.Valuation.ValuationRing

PreValuationRingclassMathlib.RingTheory.Valuation.ValuationRing, predicate

Wording

A is a valuation ring (from the name)

English

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

ValuationRingclassMathlib.RingTheory.Valuation.ValuationRing, predicate

Wording

A is a valuation ring (from the name)

English

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

ValuationRing.ValueGroupdefMathlib.RingTheory.Valuation.ValuationRing, type

Wording

value group of A and K (from the name)

English

Let $A$ and $K$ be sets. Then a value group of $A$ and $K$ is an element of the function that maps $A$ and $K$ to $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $\UnitsMACRoAO {A}$ and $K$.

ValuationRing.equivIntegerdefMathlib.RingTheory.Valuation.ValuationRing, function or constant

Wording

the equivalence integer of A and K (from the name)

English

Let $A$ and $K$ be sets. Then the equivalence integer of $A$ and $K$ is a ring isomorphism of $A$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{integer} (\operatorname{valuation} (A , K))}{x_{3}})}$.

ValuationRing.valuationdefMathlib.RingTheory.Valuation.ValuationRing, function or constant

Wording

the valuation of A and K (from the name)

English

Let $A$ and $K$ be sets. Then the valuation of $A$ and $K$ is a valuation of $K$ and the set of value groups of $A$ and $K$.

Mathlib.RingTheory.Valuation.ValuationSubring

Valuation.valuationSubringdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the valuation subring of v (from the name)

English

Let $v$ be a valuation of $K$ and $x_{1}$. Then the valuation subring of $v$ is a valuation subring of $K$.

ValuationSubringstructureMathlib.RingTheory.Valuation.ValuationSubring, type

Wording

valuation subring of K (from the name)

English

Let $K$ be a set. Then the valuation subrings of $K$ are a basic type.

ValuationSubring.ValueGroupdefMathlib.RingTheory.Valuation.ValuationSubring, type

Wording

value group of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then a value group of $A$ is an element of the function that maps $A$ to the set of value groups of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and $K$.

ValuationSubring.comapdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the preimage of A and f (from the name)

English

Let $A$ be a valuation subring of $L$. Let $f$ be a ring homomorphism of $K$ and $L$. Then the preimage of $A$ and $f$ is a valuation subring of $K$.

ValuationSubring.idealOfLEdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the ideal of R and S (from the name)

English

Let $R$ and $S$ be valuation subrings of $K$ such that $R \leq S$. Then the ideal of $R$ and $S$ is an ideal of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {R}{x_{1}})}$ defined as the preimage of the maximal ideal of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ under the inclusion of $R$ and $S$.

ValuationSubring.inclusiondefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the inclusion of R and S (from the name)

English

Let $R$ and $S$ be valuation subrings of $K$ such that $R \leq S$. Then the inclusion of $R$ and $S$ is a ring homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {R}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ defined as the inclusion of $h$.

ValuationSubring.mapOfLEdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the map of R and S (from the name)

English

Let $R$ and $S$ be valuation subrings of $K$ such that $R \leq S$. Then the map of $R$ and $S$ is a monoid with zero homomorphism of the set of value groups of $R$ and the set of value groups of $S$.

ValuationSubring.nonunitsdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

no wording

English

Let $A$ be a valuation subring of $K$. Then $\operatorname{nonunits}$ applied to $A$ is a non unital subring of $K$.

ValuationSubring.nonunitsOrderEmbeddingdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

no wording

English

$\operatorname{nonunitsOrderEmbedding}$ is an order embedding of the set of valuation subrings of $K$ and the set of order duals of the set of non unital subrings of $K$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $A$ to $\operatorname{nonunits}$ applied to $A$ and $\mathrm{ValuationSubring\_\_nonunits\_injective}$ and the function that maps $\mathrm{\_A}$ and $\mathrm{\_B}$ to $\mathrm{ValuationSubring\_\_nonunits\_le\_nonunits}$.

ValuationSubring.ofLEdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the valuation subring of R and S (from the name)

English

Let $R$ be a valuation subring of $K$. Let $S$ be a subring of $K$ such that $\operatorname{toSubring} (R)\leq S$. Then the valuation subring of $R$ and $S$ is a valuation subring of $K$.

ValuationSubring.ofPrimedefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the coarsening of A and P (from the docstring)

English

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

ValuationSubring.ofSubringdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the valuation subring of R and hR (from the name)

English

Let $R$ be a subring of $K$ such that for all elements $x_{1}$ of $K$, $x_{1}$ is an element of $R$ or $\MembershipmemMACRoT {R}{\operatorname{inv} (x_{1})}$. Then the valuation subring of $R$ and $\mathrm{hR}$ is a valuation subring of $K$ defined as $\operatorname{mk}$ applied to $R$ and $\mathrm{hR}$.

ValuationSubring.primeSpectrumEquivdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the prime spectrum equivalence of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the prime spectrum equivalence of $A$ is an equivalence from the set of prime spectra of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ to $\SubtypeSet {S}{\mathrm{Leq} (A , S)}$.

ValuationSubring.primeSpectrumOrderEquivdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the prime spectrum order equivalence of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the prime spectrum order equivalence of $A$ is an order isomorphism of the set of order duals of the set of prime spectra of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and $\SubtypeSet {S}{\mathrm{Leq} (A , S)}$.

ValuationSubring.principalUnitGroupdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the principal unit group of A (from the docstring)

English

Let $A$ be a valuation subring of $K$. Then the principal unit group of $A$ is a subgroup of $\UnitsMACRoAO {K}$.

ValuationSubring.principalUnitGroupEquivdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the principal unit group equivalence of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the principal unit group equivalence of $A$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{principalUnitGroup} (A)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{map} (\operatorname{toMonoidHom} (\operatorname{residue} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}))))}{x_{2}})}$.

ValuationSubring.principalUnitGroupOrderEmbeddingdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the principal unit group order embedding (from the name)

English

The principal unit group order embedding is an order embedding of the set of valuation subrings of $K$ and the set of order duals of the set of subgroups of $\UnitsMACRoAO {K}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $A$ to the principal unit group of $A$ and $\mathrm{ValuationSubring\_\_principalUnitGroup\_injective}$ and the function that maps $\mathrm{\_A}$ and $\mathrm{\_B}$ to $\mathrm{ValuationSubring\_\_principalUnitGroup\_le\_principalUnitGroup}$.

ValuationSubring.subtypedefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the subtype of R (from the name)

English

Let $R$ be a valuation subring of $K$. Then the subtype of $R$ is a ring homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {R}{x_{1}})}$ and $K$ defined as the subtype of $\operatorname{toSubring}$ applied to $R$.

ValuationSubring.unitGroupdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the unit group of A (from the docstring)

English

Let $A$ be a valuation subring of $K$. Then the unit group of $A$ is a subgroup of $\UnitsMACRoAO {K}$ defined as the multiplicative kernel of the composition of the monoid homomorphism of $\operatorname{toMonoidWithZeroHom}$ applied to the valuation of $A$ and the coercion homomorphism of $K$.

ValuationSubring.unitGroupMulEquivdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the unit group multiplicative equivalence of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the unit group multiplicative equivalence of $A$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{unitGroup} (A)}{x_{1}})}$ and $\UnitsMACRoAO {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})})}$.

ValuationSubring.unitGroupOrderEmbeddingdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the unit group order embedding (from the name)

English

The unit group order embedding is an order embedding of the set of valuation subrings of $K$ and the set of subgroups of $\UnitsMACRoAO {K}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $A$ to the unit group of $A$ and $\mathrm{ValuationSubring\_\_unitGroup\_injective}$ and the function that maps $\mathrm{\_A}$ and $\mathrm{\_B}$ to $\mathrm{ValuationSubring\_\_unitGroup\_le\_unitGroup}$.

ValuationSubring.unitGroupToResidueFieldUnitsdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the unit group to residue field unit of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the unit group to residue field unit of $A$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{unitGroup} (A)}{x_{1}})}$ and $\UnitsMACRoAO {\operatorname{ResidueField} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})})}$ defined as the composition of the map of $\operatorname{toMonoidHom}$ applied to $\operatorname{mk}$ applied to the maximal ideal of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and the monoid homomorphism of the unit group multiplicative equivalence of $A$.

ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnitsdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

no wording

English

Let $A$ be a valuation subring of $K$. Then $\operatorname{unitsModPrincipalUnitsEquivResidueFieldUnits}$ applied to $A$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{unitGroup} (A)}{x_{1}})}$ and the preimage of the subtype of the unit group of $A$ and the principal unit group of $A$ and $\UnitsMACRoAO {\operatorname{ResidueField} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})})}$.

ValuationSubring.valuationdefMathlib.RingTheory.Valuation.ValuationSubring, function or constant

Wording

the valuation of A (from the name)

English

Let $A$ be a valuation subring of $K$. Then the valuation of $A$ is a valuation of $K$ and the set of value groups of $A$ defined as the valuation of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and $K$.

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Valuation.CompatibleclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

v is compatible (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then we can say that $v$ is compatible.

ValuativeExtensionclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

no wording

English

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

ValuativeExtension.mapPosSubmonoiddefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the map positive part submonoid of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the map positive part submonoid of $A$ and $B$ is a monoid homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (A)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (B)}{x_{6}})}$.

ValuativeExtension.mapValueGroupWithZerodefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the map value group with zero of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the map value group with zero of $A$ and $B$ is a monoid with zero homomorphism of the set of value groups with zero of $A$ and the set of value groups with zero of $B$ defined as the composition of the embedding and the monoid with zero homomorphism of $\operatorname{toMulEquiv}$ applied to the order monoid isomorphism of the preimage of the algebra map of $A$ and $B$ and the valuation of $B$.

ValuativePreorderclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

R is a valuative preorder (from the name)

English

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

ValuativeRelclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

R is a valuative relation (from the name)

English

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

ValuativeRel.IsDiscreteclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

R is discrete (from the docstring)

English

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

ValuativeRel.IsNontrivialclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

R is nontrivial (from the name)

English

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

ValuativeRel.IsRankLeOneclassMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

no wording

English

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

ValuativeRel.RankLeOneStruct.embdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the embedding of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{RankLeOneStruct}$ applied to $R$. Then the embedding of $\mathrm{self}$ is a monoid with zero homomorphism of the set of value groups with zero of $R$ and $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ValuativeRel.ValueGroupWithZerodefMathlib.RingTheory.Valuation.ValuativeRel.Basic, type

Wording

value group with zero of R (from the name)

English

Let $R$ be a set. Then a value group with zero of $R$ is an element of the function that maps $R$ to $\mathrm{Quotient}$ applied to $\operatorname{valueSetoid}$ applied to $R$.

ValuativeRel.ValueGroupWithZero.embeddefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the embed of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the embed of $v$ is a monoid with zero homomorphism of the set of value groups with zero of $R$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$.

ValuativeRel.ValueGroupWithZero.liftdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the lift of f and t (from the name)

English

Let $f$ be a function from elements of $R$ and elements of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{8}})}$ to elements of $x_{2}$ such that for all elements $x_{3}$ and $y$ of $R$, for all elements $t_{1}$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{5}})}$, for all elements $s$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{4}})}$, if $\operatorname{vle}$ holds for $x_{3} \times t_{1}$ and $y \times s$, then if $\operatorname{vle}$ holds for $y \times s$ and $x_{3} \times t_{1}$, then $\EqtMACRoH {f (x_{3} , s)}{f (y , t_{1})}$. Let $t$ be a value group with zero of $R$. Then the lift of $f$ and $t$ is an element of $x_{2}$.

ValuativeRel.ValueGroupWithZero.lift₂defMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the lift of x3 and x4 (from the name)

English

Let $f$ be a function from elements of $R$ and elements of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{15}})}$ and elements of $R$ and elements of $\SubtypeSet {x_{14}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{14}})}$ to elements of $x_{2}$ such that for all elements $x_{5}$, $y$, $z$ and $w$ of $R$, for all elements $t$ of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{9}})}$, for all elements $s$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{8}})}$, for all elements $u$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{7}})}$, for all elements $v$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{6}})}$, if $\operatorname{vle}$ holds for $x_{5} \times t$ and $y \times s$, then if $\operatorname{vle}$ holds for $y \times s$ and $x_{5} \times t$, then if $\operatorname{vle}$ holds for $z \times u$ and $w \times v$, then if $\operatorname{vle}$ holds for $w \times v$ and $z \times u$, then $\EqtMACRoH {f (x_{5} , s , z , v)}{f (y , t , w , u)}$. Let $x_{3}$ and $x_{4}$ be value groups with zero of $R$. Then the lift of $x_{3}$ and $x_{4}$ is an element of $x_{2}$.

ValuativeRel.ValueGroupWithZero.mkdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $R$. Let $y$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{posSubmonoid} (R)}{x_{3}})}$. Then $\operatorname{mk}$ applied to $x_{2}$ and $y$ is a value group with zero of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{valueSetoid}$ applied to $R$ and $\ProdmkMACRoU {x_{2}}{y}$.

ValuativeRel.ValueGroupWithZero.orderMonoidIsodefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the order monoid isomorphism of v (from the name)

English

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

ValuativeRel.WithPreorderdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\operatorname{WithPreorder}$ applied to $R$ is an element of the function that maps $R$ to $R$.

ValuativeRel.posSubmonoiddefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the positive part submonoid of R (from the name)

English

Let $R$ be a set. Then the positive part submonoid of $R$ is a submonoid of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\operatorname{vlt}$ applied to $0$ and $x_{2}$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{ValuativeRel\_\_zero\_vlt\_mul}$ and $\mathrm{ValuativeRel\_\_zero\_vlt\_one}$.

ValuativeRel.suppdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the support of the valuation on R (from the docstring)

English

Let $R$ be a set. Then the support of the valuation on $R$ is an ideal of $R$.

ValuativeRel.uniformizerdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the uniformizer of R (from the name)

English

Let $R$ be a set. Then the uniformizer of $R$ is a value group with zero of $R$ defined as $\operatorname{choose}$ applied to $\mathrm{ValuativeRel\_\_IsDiscrete\_\_has\_maximal\_element}$.

ValuativeRel.valuationdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, function or constant

Wording

the valuation of R (from the name)

English

Let $R$ be a set. Then the valuation of $R$ is a valuation of $R$ and the set of value groups with zero of $R$.

ValuativeRel.veqdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $R$. Then $\operatorname{veq}$ holds for $x_{2}$ and $x_{3}$, if $\mathrm{AntisymmRel}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{vle}$ applied to $x_{2}$ and $x_{3}$, $x_{2}$ and $x_{3}$.

ValuativeRel.vledefMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be elements of $R$. Then $\operatorname{vle}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$ and $x_{2}$.

ValuativeRel.vltdefMathlib.RingTheory.Valuation.ValuativeRel.Basic, predicate

Wording

no wording

English

Let $x_{2}$ and $y$ be elements of $R$. Then $\operatorname{vlt}$ holds for $x_{2}$ and $y$, if it is not the case that $\operatorname{vle}$ holds for $y$ and $x_{2}$.

Mathlib.RingTheory.WittVector.Basic

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

Wording

the constant coefficient (from the name)

English

The constant coefficient is a ring homomorphism of the set of Witt vectors of $p$ and $R$ and $R$.

WittVector.ghostComponentdefMathlib.RingTheory.WittVector.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{ghostComponent}$ applied to $n$ is a ring homomorphism of the set of Witt vectors of $p$ and $R$ and $R$ defined as the composition of the evaluation ring homomorphism of the function that maps $x_{1}$ to $R$ and $n$ and $\operatorname{ghostMap}$.

WittVector.ghostEquivdefMathlib.RingTheory.WittVector.Basic, function or constant

Wording

no wording

English

Let $p$ be a natural number. Let $R$ be a set. Then $\operatorname{ghostEquiv}$ applied to $p$ and $R$ is a ring isomorphism of the set of Witt vectors of $p$ and $R$ and the set of functions from natural numbers to elements of $R$.

WittVector.ghostMapdefMathlib.RingTheory.WittVector.Basic, function or constant

Wording

no wording

English

$\operatorname{ghostMap}$ is a ring homomorphism of the set of Witt vectors of $p$ and $R$ and the set of functions from natural numbers to elements of $R$.

WittVector.mapdefMathlib.RingTheory.WittVector.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 Witt vectors of $p$ and $R$ and the set of Witt vectors of $p$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mapFun}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{one}$ applied to $f$ and $\operatorname{mul}$ applied to $f$, $\operatorname{zero}$ applied to $f$ and $\operatorname{add}$ applied to $f$.

WittVector.mapFundefMathlib.RingTheory.WittVector.Basic, function or constant

Wording

the map function of f and x2 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a Witt vector of $p$ and $x$. Then the map function of $f$ and $x_{2}$ is a Witt vector of $p$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $p$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{coeff}$ applied to $x_{2}$.

Mathlib.RingTheory.WittVector.Compare

TruncatedWittVector.zmodEquivTruncdefMathlib.RingTheory.WittVector.Compare, function or constant

Wording

the integer modulo equivalence truncation of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the integer modulo equivalence truncation of $p$ and $n$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $p ^ {n}$ and the set of truncated Witt vectors of $n$ and $\mathrm{ZMod}$ applied to $p$ defined as the ring isomorphism of the set of truncated Witt vectors of $n$ and $\mathrm{ZMod}$ applied to $p$ and $\mathrm{TruncatedWittVector\_\_card\_zmod}$ applied to $p$ and $n$.

WittVector.equivdefMathlib.RingTheory.WittVector.Compare, function or constant

Wording

the equivalence of p (from the name)

English

Let $p$ be a natural number. Then the equivalence of $p$ is a ring isomorphism of the set of Witt vectors of $p$ and $\mathrm{ZMod}$ applied to $p$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$.

WittVector.fromPadicIntdefMathlib.RingTheory.WittVector.Compare, function or constant

Wording

no wording

English

Let $p$ be a natural number. Then $\operatorname{fromPadicInt}$ applied to $p$ is a ring homomorphism of the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ and the set of Witt vectors of $p$ and $\mathrm{ZMod}$ applied to $p$ defined as the lift of the function that maps $k$ to the composition of the ring homomorphism of the integer modulo equivalence truncation of $p$ and $k$ and $\operatorname{toZModPow}$ applied to $k$ and $\mathrm{WittVector\_\_zmodEquivTrunc\_compat}$ applied to $p$.

WittVector.toPadicIntdefMathlib.RingTheory.WittVector.Compare, function or constant

Wording

the p-adic number integer of p (from the name)

English

Let $p$ be a natural number. Then the number integer ['\'p-adic_Adj\''] of $p$ is a ring homomorphism of the set of Witt vectors of $p$ and $\mathrm{ZMod}$ applied to $p$ and the set of number integers ['\'\\\'p-adic_Adj\\\'\''] of $p$ defined as the lift of $\mathrm{WittVector\_\_toZModPow\_compat}$ applied to $p$.

WittVector.toZModPowdefMathlib.RingTheory.WittVector.Compare, function or constant

Wording

no wording

English

Let $p$ and $k$ be natural numbers. Then $\operatorname{toZModPow}$ applied to $p$ and $k$ is a ring homomorphism of the set of Witt vectors of $p$ and $\mathrm{ZMod}$ applied to $p$ and $\mathrm{ZMod}$ applied to $p ^ {k}$ defined as the composition of the ring homomorphism of the inverse of the integer modulo equivalence truncation of $p$ and $k$ and $\operatorname{truncate}$ applied to $k$.

Mathlib.RingTheory.WittVector.Complete

WittVector.quotientPEquivdefMathlib.RingTheory.WittVector.Complete, function or constant

Wording

the quotient equivalence (from the name)

English

The quotient equivalence is a ring isomorphism of the set of quotients of the set of Witt vectors of $p$ and $k$ and the span of $\operatorname{singleton}$ applied to $p$ and $k$.

Mathlib.RingTheory.WittVector.Defs

WittVectorstructureMathlib.RingTheory.WittVector.Defs, type

Wording

Witt vector of p and R (from the name)

English

Let $p$ be a natural number. Let $R$ be a set. Then the Witt vectors of $p$ and $R$ are a basic type.

WittVector.coeffdefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the coefficient of self and x (from the name)

English

Let $\mathrm{self}$ be a Witt vector of $p$ and $R$. Let $x$ be a natural number. Then the coefficient of $\mathrm{self}$ and $x$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

WittVector.evaldefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the evaluation of x1 and x2 (from the name)

English

Let $x_{1}$ be a function from natural numbers to multivariate polynomials of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $k$ and $\Natural$ and $\Integer$. Let $x_{2}$ be a function from elements of $\mathrm{Fin}$ applied to $k$ to Witt vectors of $p$ and $R$. Then the evaluation of $x_{1}$ and $x_{2}$ is a Witt vector of $p$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $n$ to $\operatorname{peval}$ applied to $x_{1}$ applied to $n$ and the function that maps $i$ to $\operatorname{coeff}$ applied to $x_{2}$ applied to $i$.

WittVector.wittAdddefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

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

English

Let $p$ and $x$ be natural numbers. Then the Witt sum of $p$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\operatorname{X} (0)+ \operatorname{X} (1)$ and $x$.

WittVector.wittMuldefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the Witt product of p and x (from the name)

English

Let $p$ and $x$ be natural numbers. Then the Witt product of $p$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\operatorname{X} (0)\times \operatorname{X} (1)$ and $x$.

WittVector.wittNSMuldefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

no wording

English

Let $p$, $n$ and $x$ be natural numbers. Then $\operatorname{wittNSMul}$ applied to $p$, $n$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $1$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\HSMulhSMulMACRoAL {n}{\operatorname{X} (0)}$ and $x$.

WittVector.wittNegdefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the Witt negation of p and x (from the name)

English

Let $p$ and $x$ be natural numbers. Then the Witt negation of $p$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $1$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\operatorname{neg}$ applied to $\operatorname{X}$ applied to $0$ and $x$.

WittVector.wittOnedefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the Witt one of p and x (from the name)

English

Let $p$ and $x$ be natural numbers. Then the Witt one of $p$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $0$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $1$ and $x$.

WittVector.wittPowdefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the Witt power of n and x (from the name)

English

Let $p$, $n$ and $x$ be natural numbers. Then the Witt power of $n$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $1$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\operatorname{X} (0)^ {n}$ and $x$.

WittVector.wittSubdefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the Witt difference of p and x (from the name)

English

Let $p$ and $x$ be natural numbers. Then the Witt difference of $p$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\operatorname{X} (0)- \operatorname{X} (1)$ and $x$.

WittVector.wittZSMuldefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

no wording

English

Let $p$ and $x$ be natural numbers. Let $n$ be an integer. Then $\operatorname{wittZSMul}$ applied to $p$, $n$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $1$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $\HSMulhSMulMACRoAL {n}{\operatorname{X} (0)}$ and $x$.

WittVector.wittZerodefMathlib.RingTheory.WittVector.Defs, function or constant

Wording

the Witt zero of p and x (from the name)

English

Let $p$ and $x$ be natural numbers. Then the Witt zero of $p$ and $x$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $0$ and $\Natural$ and $\Integer$ defined as the Witt structure integer of $0$ and $x$.

Mathlib.RingTheory.WittVector.DiscreteValuationRing

WittVector.inverseCoeffdefMathlib.RingTheory.WittVector.DiscreteValuationRing, function or constant

Wording

the inverse coefficient of A and x1 (from the name)

English

Let $a$ be a unit of $k$. Let $A$ be a Witt vector of $p$ and $k$. Let $x_{1}$ be a natural number. Then the inverse coefficient of $A$ and $x_{1}$ is an element of $k$.

WittVector.mkUnitdefMathlib.RingTheory.WittVector.DiscreteValuationRing, function or constant

Wording

the unit of hA (from the name)

English

Assume that the coefficient of $A$ and $0$ is equal to the underlying value in the base of $a$. Then the unit of $\mathrm{hA}$ is a unit of the set of Witt vectors of $p$ and $k$.

WittVector.succNthValUnitsdefMathlib.RingTheory.WittVector.DiscreteValuationRing, function or constant

Wording

the successor nth value unit of A and bs (from the name)

English

Let $n$ be a natural number. Let $a$ be a unit of $k$. Let $A$ be a Witt vector of $p$ and $k$. Let $\mathrm{bs}$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $k$. Then the successor nth value unit of $A$ and $\mathrm{bs}$ is an element of $k$ defined as the product of $\operatorname{neg}$ applied to the underlying value in the base of $\operatorname{inv} (a)^ {p ^ {(n + 1)}}$ and the sum of the product of the coefficient of $A$ and $n + 1$ and the underlying value in the base of $\operatorname{inv} (a)^ {p ^ {(n + 1)}}$ and the nth remainder of the truncate function of $n + 1$ and $A$ and $\mathrm{bs}$.

Mathlib.RingTheory.WittVector.Domain

WittVector.shiftdefMathlib.RingTheory.WittVector.Domain, function or constant

Wording

the shift of x and n (from the name)

English

Let $x$ be a Witt vector of $p$ and $R$. Let $n$ be a natural number. Then the shift of $x$ and $n$ is a Witt vector of $p$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $i$ to the coefficient of $x$ and $n + i$.

Mathlib.RingTheory.WittVector.Frobenius

WittVector.frobeniusdefMathlib.RingTheory.WittVector.Frobenius, function or constant

Wording

no wording

English

$\operatorname{frobenius}$ is a ring homomorphism of the set of Witt vectors of $p$ and $R$ and the set of Witt vectors of $p$ and $R$.

WittVector.frobeniusEquivdefMathlib.RingTheory.WittVector.Frobenius, function or constant

Wording

the Frobenius equivalence of p and R (from the name)

English

Let $p$ be a natural number. Let $R$ be a set. Then the Frobenius equivalence of $p$ and $R$ is a ring isomorphism of the set of Witt vectors of $p$ and $R$ and the set of Witt vectors of $p$ and $R$.

WittVector.frobeniusFundefMathlib.RingTheory.WittVector.Frobenius, function or constant

Wording

the Frobenius function of x1 (from the name)

English

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

WittVector.frobeniusPolydefMathlib.RingTheory.WittVector.Frobenius, function or constant

Wording

the Frobenius polynomial of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the Frobenius polynomial of $p$ and $n$ is a multivariate polynomial of $\Natural$ and $\Integer$ defined as $\operatorname{X} (n)^ {p}+ \operatorname{C} (p)\times \operatorname{frobeniusPolyAux} (p , n)$.

WittVector.frobeniusPolyRatdefMathlib.RingTheory.WittVector.Frobenius, function or constant

Wording

the Frobenius polynomial rational number of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the Frobenius polynomial rational number of $p$ and $n$ is a multivariate polynomial of $\Natural$ and $\Rational$ defined as $\mathrm{MvPolynomial\_\_bind\_u2081\_\_\_app}$ applied to $\operatorname{comp}$ applied to $\mathrm{wittPolynomial}$ applied to $p$ and the function that maps $n_{1}$ to $n_{1} + 1$ and $\mathrm{xInTermsOfW}$ applied to $p$, $\Rational$ and $n$.

Mathlib.RingTheory.WittVector.FrobeniusFractionField

WittVector.RecursionBase.solutiondefMathlib.RingTheory.WittVector.FrobeniusFractionField, function or constant

Wording

the solution of x1 and x2 (from the name)

English

Let $p$ be a natural number. Let $x_{1}$ and $x_{2}$ be Witt vectors of $p$ and $k$. Then the solution of $x_{1}$ and $x_{2}$ is an element of $k$ defined as $\operatorname{choose}$ applied to $\mathrm{WittVector\_\_RecursionBase\_\_solution\_pow}$ applied to $p$, $x_{1}$ and $x_{2}$.

WittVector.RecursionMain.succNthDefiningPolydefMathlib.RingTheory.WittVector.FrobeniusFractionField, function or constant

Wording

no wording

English

Let $p$ and $n$ be elements of $\Natural$. Let $x_{1}$ and $x_{2}$ be Witt vectors of $p$ and $k$. Let $\mathrm{bs}$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $k$. Then $\operatorname{succNthDefiningPoly}$ applied to $p$, $n$, $x_{1}$, $x_{2}$ and $\mathrm{bs}$ is a polynomial of $k$ defined as the sum of the difference between the product of $\operatorname{X} ^ {p}$ and $\operatorname{C}$ applied to the exponentiation of the coefficient of $x_{1}$ and $0$ to $p ^ {(n + 1)}$ and the product of $\operatorname{X}$ and $\operatorname{C}$ applied to the exponentiation of the coefficient of $x_{2}$ and $0$ to $p ^ {(n + 1)}$ and $\operatorname{C}$ applied to the difference between the difference between the sum of the product of the coefficient of $x_{1}$ and $n + 1$ and $(\mathrm{bs} (0)^ {p})^ {p ^ {(n + 1)}}$ and the nth remainder of the function that maps $v$ to $\mathrm{bs} (v)^ {p}$ and the truncate function of $n + 1$ and $x_{1}$ and the product of the coefficient of $x_{2}$ and $n + 1$ and $\mathrm{bs} (0)^ {p ^ {(n + 1)}}$ and the nth remainder of $\mathrm{bs}$ and the truncate function of $n + 1$ and $x_{2}$.

WittVector.RecursionMain.succNthValdefMathlib.RingTheory.WittVector.FrobeniusFractionField, function or constant

Wording

the successor nth value of x2 and bs (from the name)

English

Let $p$ and $n$ be natural numbers. Let $x_{1}$ and $x_{2}$ be Witt vectors of $p$ and $k$. Let $\mathrm{bs}$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $k$. Assume that the coefficient of $x_{1}$ and $0$ is distinct from $0$. Assume that the coefficient of $x_{2}$ and $0$ is distinct from $0$. Then the successor nth value of $x_{2}$ and $\mathrm{bs}$ is an element of $k$ defined as $\operatorname{choose}$ applied to $\mathrm{WittVector\_\_RecursionMain\_\_root\_exists}$ applied to $p$, $n$, $x_{1}$, $x_{2}$, $\mathrm{bs}$, $h_{2}$ and $h_{3}$.

WittVector.frobeniusRotationdefMathlib.RingTheory.WittVector.FrobeniusFractionField, function or constant

Wording

the Frobenius rotation of p (from the name)

English

Let $p$ be a natural number. Assume that the coefficient of $x_{1}$ and $0$ is distinct from $0$. Assume that the coefficient of $x_{2}$ and $0$ is distinct from $0$. Then the Frobenius rotation of $p$ is a Witt vector of $p$ and $k$ defined as $\operatorname{mk}$ applied to $p$ and $\operatorname{frobeniusRotationCoeff}$ applied to $p$.

WittVector.frobeniusRotationCoeffdefMathlib.RingTheory.WittVector.FrobeniusFractionField, function or constant

Wording

the Frobenius rotation coefficient of p and x3 (from the name)

English

Let $p$ and $x_{3}$ be natural numbers. Assume that the coefficient of $x_{1}$ and $0$ is distinct from $0$. Assume that the coefficient of $x_{2}$ and $0$ is distinct from $0$. Then the Frobenius rotation coefficient of $p$ and $x_{3}$ is an element of $k$.

Mathlib.RingTheory.WittVector.InitTail

WittVector.initdefMathlib.RingTheory.WittVector.InitTail, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $x_{1}$ be a Witt vector of $p$ and $R$. Then $\operatorname{init}$ applied to $n$ and $x_{1}$ is a Witt vector of $p$ and $R$ defined as $\operatorname{select}$ applied to the function that maps $i$ to $\mathrm{Lt} (i , n)$ and $x_{1}$.

WittVector.initRingdefMathlib.RingTheory.WittVector.InitTail, function or constant

Wording

no wording

English

generation took over the time limit

WittVector.selectdefMathlib.RingTheory.WittVector.InitTail, function or constant

Wording

no wording

English

Let $P$ be a function from elements of $\Natural$ to propositions. Let $x_{1}$ be a Witt vector of $p$ and $R$. Then $\operatorname{select}$ applied to $P$ and $x_{1}$ is a Witt vector of $p$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $n$ to $\iteMACRoG {P (n)}{\operatorname{coeff} (x_{1} , n)}{0}$.

WittVector.selectPolydefMathlib.RingTheory.WittVector.InitTail, function or constant

Wording

no wording

English

Let $P$ be a function from natural numbers to propositions. Let $n$ be a natural number. Then $\operatorname{selectPoly}$ applied to $P$ and $n$ is a multivariate polynomial of $\Natural$ and $\Integer$ defined as $\iteMACRoG {P (n)}{\operatorname{X} (n)}{0}$.

WittVector.taildefMathlib.RingTheory.WittVector.InitTail, function or constant

Wording

the tail of n and x1 (from the name)

English

Let $n$ be a natural number. Let $x_{1}$ be a Witt vector of $p$ and $R$. Then the tail of $n$ and $x_{1}$ is a Witt vector of $p$ and $R$ defined as $\operatorname{select}$ applied to the function that maps $i$ to $\mathrm{Leq} (n , i)$ and $x_{1}$.

Mathlib.RingTheory.WittVector.IsPoly

WittVector.IsPolyclassMathlib.RingTheory.WittVector.IsPoly, predicate

Wording

no wording

English

Let $p$ be a natural number. Let $f$ be a function from sets $R$ and elements of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and Witt vectors of $p$ and $R$ to Witt vectors of $p$ and $R$. Then we can say that $\operatorname{IsPoly}$ holds for $p$, $R$ and $f$.

WittVector.IsPoly₂classMathlib.RingTheory.WittVector.IsPoly, predicate

Wording

no wording

English

Let $p$ be a natural number. Let $f$ be a function from sets $R$ and elements of $\mathrm{Proof}$ applied to the proposition that $R$ is a commutative ring and Witt vectors of $p$ and $R$ and Witt vectors of $p$ and $R$ to Witt vectors of $p$ and $R$. Then we can say that $\mathrm{WittVector\_\_IsPoly\_u2082\_}$ holds for $p$, $R$ and $f$.

WittVector.onePolydefMathlib.RingTheory.WittVector.IsPoly, function or constant

Wording

the one polynomial of n (from the name)

English

Let $n$ be a natural number. Then the one polynomial of $n$ is a multivariate polynomial of $\Natural$ and $\Integer$ defined as $\iteMACRoG {\mathrm{Eq} (n , 0)}{1}{0}$.

Mathlib.RingTheory.WittVector.Isocrystal

WittVector.FractionRing.frobeniusdefMathlib.RingTheory.WittVector.Isocrystal, function or constant

Wording

no wording

English

Let $p$ be a natural number. Let $k$ be a set. Then $\operatorname{frobenius}$ applied to $p$ and $k$ is a ring isomorphism of the set of fraction rings of the set of Witt vectors of $p$ and $k$ and the set of fraction rings of the set of Witt vectors of $p$ and $k$ defined as the ring isomorphism of the Frobenius equivalence of $p$ and $k$.

WittVector.FractionRing.frobeniusRingHomdefMathlib.RingTheory.WittVector.Isocrystal, function or constant

Wording

the Frobenius ring homomorphism of p and k (from the name)

English

Let $p$ be a natural number. Let $k$ be a set. Then the Frobenius ring homomorphism of $p$ and $k$ is a ring homomorphism of the set of fraction rings of the set of Witt vectors of $p$ and $k$ and the set of fraction rings of the set of Witt vectors of $p$ and $k$ defined as the ring homomorphism of $\operatorname{frobenius}$ applied to $p$ and $k$.

WittVector.IsocrystalclassMathlib.RingTheory.WittVector.Isocrystal, predicate

Wording

p is isocrystal (from the docstring)

English

Let $p$ be a natural number. Let $k$ and $V$ be sets. Then we can say that $p$ is isocrystal.

WittVector.Isocrystal.frobdefMathlib.RingTheory.WittVector.Isocrystal, function or constant

Wording

no wording

English

$\operatorname{frob}$ is a linear equivalence of $V$ and $V$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

WittVector.Isocrystal.frobeniusdefMathlib.RingTheory.WittVector.Isocrystal, function or constant

Wording

no wording

English

Let $p$ be a natural number. Let $k$ be a set. Then $\operatorname{frobenius}$ applied to $p$ and $k$ is a linear equivalence of $V$ and $V$ defined as $\operatorname{frob}$.

WittVector.IsocrystalEquivstructureMathlib.RingTheory.WittVector.Isocrystal, type

Wording

isocrystal equivalence of V and x3 (from the name)

English

Let $p$ be a natural number. Let $k$, $V$ and $x_{3}$ be sets. Then the isocrystal equivalences of $V$ and $x_{3}$ are a basic type.

WittVector.IsocrystalHomstructureMathlib.RingTheory.WittVector.Isocrystal, type

Wording

isocrystal homomorphism of V and x3 (from the name)

English

Let $p$ be a natural number. Let $k$, $V$ and $x_{3}$ be sets. Then the isocrystal homomorphisms of $V$ and $x_{3}$ are a basic type.

WittVector.StandardOneDimIsocrystaldefMathlib.RingTheory.WittVector.Isocrystal, type

Wording

no wording

English

Let $p$ be a natural number. Let $k$ be a set. Let $\mathrm{\_m}$ be an integer. Then an element of $\operatorname{StandardOneDimIsocrystal}$ applied to $p$, $k$ and $\mathrm{\_m}$ is an element of the function that maps $p$, $k$ and $\mathrm{\_m}$ to the set of fraction rings of the set of Witt vectors of $p$ and $k$.

Mathlib.RingTheory.WittVector.MulCoeff

WittVector.nthRemainderdefMathlib.RingTheory.WittVector.MulCoeff, function or constant

Wording

the nth remainder of x1 and x2 (from the name)

English

Let $p$ and $n$ be natural numbers. Let $x_{1}$ and $x_{2}$ be functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $k$. Then the nth remainder of $x_{1}$ and $x_{2}$ is an element of $k$ defined as $\operatorname{choose}$ applied to $\mathrm{WittVector\_\_nth\_mul\_coeff}$ applied to $p$, $k$ and $n$, $x_{1}$ and $x_{2}$.

WittVector.polyOfInterestdefMathlib.RingTheory.WittVector.MulCoeff, function or constant

Wording

the polynomial of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the polynomial of $p$ and $n$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and the set of integers defined as the difference between the difference between the sum of the Witt product of $p$ and $n + 1$ and $p ^ {(n + 1)}\times \operatorname{X} (\ProdmkMACRoU {0}{(n + 1)})\times \operatorname{X} (\ProdmkMACRoU {1}{(n + 1)})$ and the product of $\operatorname{X}$ applied to $\ProdmkMACRoU {0}{(n + 1)}$ and $\operatorname{rename}$ applied to $\ProdmkMACRoU {1}$ and the Witt polynomial of $p$ and $n + 1$ and the product of $\operatorname{X}$ applied to $\ProdmkMACRoU {1}{(n + 1)}$ and $\operatorname{rename}$ applied to $\ProdmkMACRoU {0}$ and the Witt polynomial of $p$ and $n + 1$.

WittVector.remainderdefMathlib.RingTheory.WittVector.MulCoeff, function or constant

Wording

the remainder of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the remainder of $p$ and $n$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and $\Integer$ defined as $\FinsetSum {\FinsetrangeMACRoN {(n + 1)}}{x}{\operatorname{rename} (\ProdmkMACRoU {0}, \operatorname{monomial} (\FinsuppsingleMACRoS {x}{(p ^ {(n + 1 - x)})}, p ^ {x}))}\times \FinsetSum {\FinsetrangeMACRoN {(n + 1)}}{x_{1}}{\operatorname{rename} (\ProdmkMACRoU {1}, \operatorname{monomial} (\FinsuppsingleMACRoS {x_{1}}{(p ^ {(n + 1 - x_{1})})}, p ^ {x_{1}}))}$.

WittVector.wittPolyProddefMathlib.RingTheory.WittVector.MulCoeff, function or constant

Wording

the Witt polynomial product of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the Witt polynomial product of $p$ and $n$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and $\Integer$ defined as the product of $\operatorname{rename}$ applied to $\ProdmkMACRoU {0}$ and the Witt polynomial of $p$ and $n$ and $\operatorname{rename}$ applied to $\ProdmkMACRoU {1}$ and the Witt polynomial of $p$ and $n$.

WittVector.wittPolyProdRemainderdefMathlib.RingTheory.WittVector.MulCoeff, function or constant

Wording

the Witt polynomial product remainder of p and n (from the name)

English

Let $p$ and $n$ be elements of $\Natural$. Then the Witt polynomial product remainder of $p$ and $n$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $2$ and $\Natural$ and $\Integer$ defined as $\FinsetSum {\FinsetrangeMACRoN {n}}{i}{(p ^ {i}\times \operatorname{wittMul} (p , i)^ {p ^ {(n - i)}})}$.

Mathlib.RingTheory.WittVector.MulP

WittVector.wittMulNdefMathlib.RingTheory.WittVector.MulP, function or constant

Wording

the Witt multiplicative of x and x1 (from the name)

English

Let $p$, $x$ and $x_{1}$ be natural numbers. Then the Witt multiplicative of $x$ and $x_{1}$ is a multivariate polynomial of $\Natural$ and $\Integer$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{WittVector\_\_wittMulN\_\_\_f}$ applied to $p$ and $x_{1}$.

Mathlib.RingTheory.WittVector.StructurePolynomial

wittStructureIntdefMathlib.RingTheory.WittVector.StructurePolynomial, function or constant

Wording

the Witt structure integer of x and n (from the name)

English

Let $p$ and $n$ be natural numbers. Let $x$ be a multivariate polynomial of $\mathrm{idx}$ and $\Integer$. Then the Witt structure integer of $x$ and $n$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{idx}$ and $\Natural$ and $\Integer$.

wittStructureRatdefMathlib.RingTheory.WittVector.StructurePolynomial, function or constant

Wording

the Witt structure rational number of x and n (from the name)

English

Let $p$ and $n$ be natural numbers. Let $x$ be a multivariate polynomial of $\mathrm{idx}$ and $\Rational$. Then the Witt structure rational number of $x$ and $n$ is a multivariate polynomial of $\mathrm{Prod}$ applied to $\mathrm{idx}$ and $\Natural$ and $\Rational$ defined as $\mathrm{MvPolynomial\_\_bind\_u2081\_\_\_app}$ applied to the function that maps $k_{1}$ to $\mathrm{MvPolynomial\_\_bind\_u2081\_\_\_app}$ applied to the function that maps $i$ to $\operatorname{rename}$ applied to $\ProdmkMACRoU {i}$ and the Witt polynomial of $p$ and $k_{1}$ and $x$ and $\mathrm{xInTermsOfW}$ applied to $p$, $\Rational$ and $n$.

Mathlib.RingTheory.WittVector.Teichmuller

WittVector.teichmullerdefMathlib.RingTheory.WittVector.Teichmuller, function or constant

Wording

the Teichmuller of p (from the name)

English

Let $p$ be a natural number. Then the Teichmuller of $p$ is a monoid homomorphism of $R$ and the set of Witt vectors of $p$ and $R$.

WittVector.teichmullerFundefMathlib.RingTheory.WittVector.Teichmuller, function or constant

Wording

the underlying function of the monoid hom of p and r (from the docstring)

English

Let $p$ be a natural number. Let $r$ be an element of $R$. Then the underlying function of the monoid hom of $p$ and $r$ is a Witt vector of $p$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $n$ to $\iteMACRoG {\mathrm{Eq} (n , 0)}{r}{0}$.

Mathlib.RingTheory.WittVector.Truncated

TruncatedWittVectordefMathlib.RingTheory.WittVector.Truncated, type

Wording

truncated Witt vector of n and R (from the name)

English

Let $x$ and $n$ be natural numbers. Let $R$ be a set. Then a truncated Witt vector of $n$ and $R$ is an element of the function that maps $x$, $n$ and $R$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$.

TruncatedWittVector.coeffdefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

the coefficient of i and x (from the name)

English

Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Let $x$ be a truncated Witt vector of $n$ and $R$. Then the coefficient of $i$ and $x$ is an element of $R$ defined as $x$ applied to $i$.

TruncatedWittVector.mkdefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

no wording

English

Let $p$ be a natural number. Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$. Then there is a truncated Witt vector of $n$ and $R$. Proof. Let $p$ be arbitrary. Let $x$ be arbitrary. By x.

TruncatedWittVector.outdefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

no wording

English

Let $x_{1}$ be a truncated Witt vector of $n$ and $R$. Then $\operatorname{out}$ applied to $x_{1}$ is a Witt vector of $p$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $i$ to $\mathrm{dite}$ applied to $\mathrm{Lt} (i , n)$, the function that maps $h$ to the coefficient of $\operatorname{mk}$ applied to $i$ and $h$ and $x_{1}$ and the function that maps $h_{1}$ to $0$.

TruncatedWittVector.truncatedefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

no wording

English

Assume that $n \leq m$. Then $\operatorname{truncate}$ applied to $\mathrm{hm}$ is a ring homomorphism of the set of truncated Witt vectors of $m$ and $R$ and the set of truncated Witt vectors of $n$ and $R$ defined as $\operatorname{liftOfRightInverse}$ applied to $\operatorname{truncate}$ applied to $m$, $\operatorname{out}$, $\mathrm{TruncatedWittVector\_\_truncateFun\_out}$ and $\operatorname{truncate}$ applied to $n$.

WittVector.liftdefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

the lift of f and k (from the name)

English

Let $f$ be a function from natural numbers $k$ to ring homomorphisms of $S$ and the set of truncated Witt vectors of $k$ and $R$ such that for all natural numbers $x_{2}$ and $x_{3}$, for all elements $\mathrm{hk}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{2} , x_{3})$, the composition of $\operatorname{truncate}$ applied to $\mathrm{hk}$ and $f$ applied to $x_{3}$ is equal to $f$ applied to $x_{2}$. Then the lift of $k$ and $f$ is a ring homomorphism of $S$ and the set of Witt vectors of $p$ and $R$.

WittVector.liftEquivdefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

the lift equivalence (from the name)

English

The lift equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{forall} (\Natural , \lambda x_{2} . \mathrm{forall} (\Natural , \lambda x_{3} . \mathrm{forall} (\mathrm{Proof} (\mathrm{Leq} (x_{2} , x_{3})), \lambda \mathrm{hk} . \EqtMACRoH {\operatorname{comp} (\operatorname{truncate} (\mathrm{hk}), f (x_{3}))}{f (x_{2})})))})}{\mathrm{RingHom} (S , \mathrm{WittVector} (p , R))}$.

WittVector.liftFundefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

the lift function of f and k (from the name)

English

Let $f$ be a function from natural numbers $k$ to ring homomorphisms of $S$ and the set of truncated Witt vectors of $k$ and $R$. Let $s$ be an element of $S$. Then the lift function of $k$ and $f$ is a Witt vector of $p$ and $R$ defined as the function that maps $s$ to $\operatorname{mk}$ applied to $p$, the function that maps $k$ to the coefficient of $\operatorname{last}$ applied to $k$ and $k$ applied to $k + 1$ and $f$ and $s$.

WittVector.truncatedefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{truncate}$ applied to $n$ is a ring homomorphism of the set of Witt vectors of $p$ and $R$ and the set of truncated Witt vectors of $n$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{truncateFun}$ applied to $n$ and $\mathrm{WittVector\_\_truncateFun\_one}$ applied to $p$, $n$ and $R$ and $\mathrm{WittVector\_\_truncateFun\_mul}$ applied to $n$, $\mathrm{WittVector\_\_truncateFun\_zero}$ applied to $p$, $n$ and $R$ and $\mathrm{WittVector\_\_truncateFun\_add}$ applied to $n$.

WittVector.truncateFundefMathlib.RingTheory.WittVector.Truncated, function or constant

Wording

the truncate function of n and x (from the name)

English

Let $n$ be a natural number. Let $x$ be a Witt vector of $p$ and $R$. Then the truncate function of $n$ and $x$ is a truncated Witt vector of $n$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $i$ to the coefficient of $x$ and $\operatorname{val}$ applied to $i$.

Mathlib.RingTheory.WittVector.Verschiebung

WittVector.verschiebungdefMathlib.RingTheory.WittVector.Verschiebung, function or constant

Wording

no wording

English

$\operatorname{verschiebung}$ is an additive monoid homomorphism of the set of Witt vectors of $p$ and $R$ and the set of Witt vectors of $p$ and $R$.

WittVector.verschiebungFundefMathlib.RingTheory.WittVector.Verschiebung, function or constant

Wording

no wording

English

Let $x_{1}$ be a Witt vector of $p$ and $R$. Then $\operatorname{verschiebungFun}$ applied to $x_{1}$ is a Witt vector of $p$ and $R$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $n$ to $\iteMACRoG {\mathrm{Eq} (n , 0)}{0}{\operatorname{coeff} (x_{1} , n - 1)}$.

WittVector.verschiebungPolydefMathlib.RingTheory.WittVector.Verschiebung, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{verschiebungPoly}$ applied to $n$ is a multivariate polynomial of $\Natural$ and $\Integer$ defined as $\iteMACRoG {\mathrm{Eq} (n , 0)}{0}{\operatorname{X} (n - 1)}$.

Mathlib.RingTheory.WittVector.WittPolynomial

wittPolynomialdefMathlib.RingTheory.WittVector.WittPolynomial, function or constant

Wording

the Witt polynomial of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Let $R$ be a set. Then the Witt polynomial of $p$ and $n$ is a multivariate polynomial of $\Natural$ and $R$ defined as $\FinsetSum {\FinsetrangeMACRoN {(n + 1)}}{i}{\operatorname{monomial} (\FinsuppsingleMACRoS {i}{(p ^ {(n - i)})}, p ^ {i})}$.

xInTermsOfWdefMathlib.RingTheory.WittVector.WittPolynomial, function or constant

Wording

no wording

English

Let $p$ and $x_{2}$ be natural numbers. Let $R$ be a set. Then $\mathrm{xInTermsOfW}$ applied to $p$, $R$ and $x_{2}$ is a multivariate polynomial of $\Natural$ and $R$.

Mathlib.RingTheory.ZariskisMainTheorem

Algebra.ZariskisMainPropertydefMathlib.RingTheory.ZariskisMainTheorem, predicate

Wording

no wording

English

Let $R$ be a set. Let $p$ be an ideal of $S$. Then $\operatorname{ZariskisMainProperty}$ holds for $R$ and $p$, if there exists an element $r$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{integralClosure} (R , S)}{x_{3}})}$, such that it is not the case that $\MembershipmemMACRoT {p}{r}$ and $\operatorname{coe}$ applied to $\operatorname{awayMap}$ applied to $\operatorname{toRingHom}$ applied to the value of the integral closure of $R$ and $S$ and $r$ is bijective.