Definitions: Mathlib.Algebra, part 1 of 17

AddConstMapstructureMathlib.Algebra.AddConstMap.Basic, type

Wording

additive constant map of a and b (from the name)

English

Let $G$ and $H$ be sets. Let $a$ be an element of $G$. Let $b$ be an element of $H$. Then the additive constant maps of $a$ and $b$ are a basic type.

AddConstMap.addLeftHomdefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

the additive left homomorphism (from the name)

English

The additive left homomorphism is a monoid homomorphism of the set of multiplicatives of $G$ and the set of additive constant maps of $a$ and $a$.

AddConstMap.compdefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be an additive constant map of $b$ and $c$. Let $f$ be an additive constant map of $a$ and $b$. Then the composition of $g$ and $f$ is an additive constant map of $a$ and $c$.

AddConstMap.conjNegdefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

the conjugate negation (from the name)

English

The conjugate negation is an equivalence from the set of additive constant maps of $a$ and $b$ to the set of additive constant maps of $a$ and $b$.

AddConstMap.iddefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

the identity map (from the docstring)

English

The identity map is an additive constant map of $a$ and $a$.

AddConstMap.mkFractdefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $G$. Then $\operatorname{mkFract}$ applied to $a$ is an equivalence from the set of functions from elements of $\operatorname{Ico}$ applied to $0$ and $1$ to elements of $G$ to the set of additive constant maps of $1$ and $a$.

AddConstMap.replaceConstsdefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

no wording

English

Let $f$ be an additive constant map of $a$ and $b$. Let $\mathrm{a'}$ be an element of $G$. Let $\mathrm{b'}$ be an element of $H$. Assume that $\EqtMACRoH {a}{\mathrm{a'}}$. Assume that $\EqtMACRoH {b}{\mathrm{b'}}$. Then $\operatorname{replaceConsts}$ applied to $f$, $\mathrm{a'}$, $\mathrm{b'}$, $\mathrm{ha}$ and $\mathrm{hb}$ is an additive constant map of $\mathrm{a'}$ and $\mathrm{b'}$.

AddConstMap.smuldefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

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

English

Let $c$ be an element of $K$. Let $f$ be an additive constant map of $a$ and $b$. Then the scalar multiple of $c$ and $f$ is an additive constant map of $a$ and $\HSMulhSMulMACRoAL {c}{b}$.

AddConstMap.toEnddefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

the end (from the name)

English

The end is a monoid homomorphism of the set of additive constant maps of $a$ and $a$ and the set of ends of $G$.

AddConstMap.toFundefMathlib.Algebra.AddConstMap.Basic, function or constant

Wording

the additive constant map of self and x2 (from the name)

English

Let $\mathrm{self}$ be an additive constant map of $a$ and $b$. Let $x_{2}$ be an element of $G$. Then the additive constant map of $\mathrm{self}$ and $x_{2}$ is an element of $H$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

AddConstMapClassclassMathlib.Algebra.AddConstMap.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $G$ and $H$ be elements of $\mathrm{outParam}$ applied to the set of sets. Let $a$ be an element of $\mathrm{outParam}$ applied to $G$. Let $b$ be an element of $\mathrm{outParam}$ applied to $H$. Then we can say that $\mathrm{AddConstMapClass}$ holds for $F$, $G$, $H$, $a$ and $b$.

Mathlib.Algebra.AddConstMap.Equiv

AddConstEquivstructureMathlib.Algebra.AddConstMap.Equiv, type

Wording

additive constant equivalence of a and b (from the name)

English

Let $G$ and $H$ be sets. Let $a$ be an element of $G$. Let $b$ be an element of $H$. Then the additive constant equivalences of $a$ and $b$ are a basic type.

AddConstEquiv.equivUnitsdefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the equivalence unit (from the name)

English

The equivalence unit is a multiplicative equivalence of the set of additive constant equivalences of $a$ and $a$ and the set of units of the set of additive constant maps of $a$ and $a$.

AddConstEquiv.refldefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the identity map of a (from the docstring)

English

Let $a$ be an element of $G$. Then the identity map of $a$ is an additive constant equivalence of $a$ and $a$.

AddConstEquiv.symmdefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be an additive constant equivalence of $a$ and $b$. Then the inverse of $e$ is an additive constant equivalence of $b$ and $a$.

AddConstEquiv.toAddConstMapdefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the additive constant map of self (from the name)

English

Let $\mathrm{self}$ be an additive constant equivalence of $a$ and $b$. Then the additive constant map of $\mathrm{self}$ is an additive constant map of $a$ and $b$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{AddConstEquiv\_\_map\_add\_const'}$ applied to $\mathrm{self}$.

AddConstEquiv.toAddConstMapHomdefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the additive constant map homomorphism (from the name)

English

The additive constant map homomorphism is a monoid homomorphism of the set of additive constant equivalences of $a$ and $a$ and the set of additive constant maps of $a$ and $a$.

AddConstEquiv.toPermdefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the permutation (from the name)

English

The permutation is a monoid homomorphism of the set of additive constant equivalences of $a$ and $a$ and the set of permutations of $G$.

AddConstEquiv.transdefMathlib.Algebra.AddConstMap.Equiv, function or constant

Wording

the composition of x3 and x4 (from the name)

English

Let $x_{3}$ be an additive constant equivalence of $a$ and $b$. Let $x_{4}$ be an additive constant equivalence of $b$ and $c$. Then the composition of $x_{3}$ and $x_{4}$ is an additive constant equivalence of $a$ and $c$.

Mathlib.Algebra.AffineMonoid.Basic

IsAffineAddMonoidclassMathlib.Algebra.AffineMonoid.Basic, predicate

Wording

M is a affine additive monoid (from the name)

English

Let $M$ be a set. Then we can say that $M$ is an affine additive monoid.

IsAffineMonoidclassMathlib.Algebra.AffineMonoid.Basic, predicate

Wording

M is a affine monoid (from the name)

English

Let $M$ be a set. Then we can say that $M$ is an affine monoid.

Mathlib.Algebra.AffineMonoid.Embedding

AffineAddMonoid.dimdefMathlib.Algebra.AffineMonoid.Embedding, function or constant

Wording

the dimension of M (from the docstring)

English

Let $M$ be a set. Then the dimension of $M$ is a natural number defined as the rank of $\Integer$ and the set of Grothendieck additive groups of $M$.

AffineAddMonoid.embeddingdefMathlib.Algebra.AffineMonoid.Embedding, function or constant

Wording

the embedding of M (from the name)

English

Let $M$ be a set. Then the embedding of $M$ is an additive monoid homomorphism of $M$ and the set of free Abelian groups of $\mathrm{Fin}$ applied to the dimension of $M$ defined as the composition of the additive monoid homomorphism of the inverse of the equivalence finitely supported function of $\mathrm{Fin}$ applied to the dimension of $M$ and the composition of the additive monoid homomorphism of $\operatorname{toLinearMap}$ applied to the representation of the finite basis of $\Integer$ and the set of Grothendieck additive groups of $M$ and the additive monoid homomorphism of the additive monoid of the top.

Mathlib.Algebra.Algebra.Basic

Algebra.algebraMapSubmonoiddefMathlib.Algebra.Algebra.Basic, function or constant

Wording

the algebra map submonoid of S and M (from the name)

English

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

LinearEquiv.extendScalarsOfSurjectivedefMathlib.Algebra.Algebra.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Let $f$ be a linear equivalence of $M$ and $N$. Then $\operatorname{extendScalarsOfSurjective}$ applied to $h_{2}$ and $f$ is a linear equivalence of $M$ and $N$.

LinearMap.extendScalarsOfSurjectivedefMathlib.Algebra.Algebra.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Let $l$ be a linear map of $M$ and $N$. Then $\operatorname{extendScalarsOfSurjective}$ applied to $h_{2}$ and $l$ is a linear map of $M$ and $N$ defined as $\operatorname{extendScalarsOfSurjectiveEquiv}$ applied to $h_{2}$ and $l$.

LinearMap.extendScalarsOfSurjectiveEquivdefMathlib.Algebra.Algebra.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then $\operatorname{extendScalarsOfSurjectiveEquiv}$ applied to $h_{2}$ is a linear equivalence of the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $N$.

Mathlib.Algebra.Algebra.Bilinear

Algebra.lmuldefMathlib.Algebra.Algebra.Bilinear, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{lmul}$ applied to $R$ and $A$ is an algebra homomorphism of $A$ and the set of ends of $R$ and $A$.

LinearMap.muldefMathlib.Algebra.Algebra.Bilinear, function or constant

Wording

the product of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the product of $R$ and $A$ is a linear map of $A$ and the set of linear maps of $A$ and $A$.

LinearMap.mul'defMathlib.Algebra.Algebra.Bilinear, function or constant

Wording

the product of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the product of $R$ and $A$ is a linear map of the set of tensor products of $A$ and $A$ and $A$ defined as the lift of the product of $R$ and $A$.

LinearMap.mul''defMathlib.Algebra.Algebra.Bilinear, function or constant

Wording

the product of R and A (from the name)

English

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

NonUnitalAlgHom.lmuldefMathlib.Algebra.Algebra.Bilinear, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{lmul}$ applied to $R$ and $A$ is a non unital algebra homomorphism of $A$ and the set of ends of $R$ and $A$.

Mathlib.Algebra.Algebra.Defs

AlgebraclassMathlib.Algebra.Algebra.Defs, predicate

Wording

no wording

English

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

Algebra.algebraMapdefMathlib.Algebra.Algebra.Defs, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the algebra map of $R$ and $A$ is a ring homomorphism of $R$ and $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Algebra.castdefMathlib.Algebra.Algebra.Defs, function or constant

Wording

the cast of x3 (from the name)

English

Let $x_{3}$ be an element of $R$. Then the cast of $x_{3}$ is an element of $A$ defined as the coercion of the algebra map of $R$ and $A$ and $x_{3}$.

Algebra.linearMapdefMathlib.Algebra.Algebra.Defs, function or constant

Wording

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

English

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

Mathlib.Algebra.Algebra.Epi

Algebra.IsEpiclassMathlib.Algebra.Algebra.Epi, predicate

Wording

no wording

English

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

TensorProduct.lid'defMathlib.Algebra.Algebra.Epi, function or constant

Wording

no wording

English

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

Mathlib.Algebra.Algebra.Equiv

AlgEquivstructureMathlib.Algebra.Algebra.Equiv, type

Wording

algebra isomorphism of A and B (from the name)

English

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

AlgEquiv.algHomUnitsEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra homomorphism unit equivalence of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the algebra homomorphism unit equivalence of $R$ and $S$ is a multiplicative equivalence of the set of units of the set of algebra homomorphisms of $S$ and $S$ and the set of algebra isomorphisms of $S$ and $S$.

AlgEquiv.arrowCongrdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the arrow congruence of x13 and x14 (from the name)

English

Let $x_{13}$ be an algebra isomorphism of $x$ and $x_{2}$. Let $x_{14}$ be an algebra isomorphism of $x_{1}$ and $x_{3}$. Then the arrow congruence of $x_{13}$ and $x_{14}$ is an equivalence from the set of algebra homomorphisms of $x$ and $x_{1}$ to the set of algebra homomorphisms of $x_{2}$ and $x_{3}$.

AlgEquiv.autCongrdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the automorphism congruence of x7 (from the name)

English

Let $x_{7}$ be an algebra isomorphism of $x$ and $x_{1}$. Then the automorphism congruence of $x_{7}$ is a multiplicative equivalence of the set of algebra isomorphisms of $x$ and $x$ and the set of algebra isomorphisms of $x_{1}$ and $x_{1}$.

AlgEquiv.castdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the cast of h (from the name)

English

Assume that $\EqtMACRoH {i}{j}$. Then the cast of $h$ is an algebra isomorphism of $A$ applied to $i$ and $A$ applied to $j$.

AlgEquiv.equivCongrdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the equivalence congruence of e and #2 (from the name)

English

Let $e$ be an algebra isomorphism of $x$ and $x_{1}$. Let $\mathrm{e'}$ be an algebra isomorphism of $x_{2}$ and $x_{3}$. Then the equivalence congruence of $e$ and $\mathrm{e'}$ is an equivalence from the set of algebra isomorphisms of $x$ and $x_{2}$ to the set of algebra isomorphisms of $x_{1}$ and $x_{3}$.

AlgEquiv.ofAlgHomdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

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

English

Let $f$ be an algebra homomorphism of $x$ and $x_{1}$. Let $g$ be an algebra homomorphism of $x_{1}$ and $x$ such that the composition of $f$ and $g$ is equal to the identity of $R$ and $x_{1}$ and the composition of $g$ and $f$ is equal to the identity of $R$ and $x$. Then the algebra isomorphism of $f$ and $g$ is an algebra isomorphism of $x$ and $x_{1}$.

AlgEquiv.ofBijectivedefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

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

English

Let $f$ be an algebra homomorphism of $x$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the algebra isomorphism of $f$ and $\mathrm{hf}$ is an algebra isomorphism of $x$ and $x_{1}$.

AlgEquiv.ofClassdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra isomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the algebra isomorphism of $f$ is an algebra isomorphism of $A$ and $B$.

AlgEquiv.ofLinearEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra isomorphism of l (from the name)

English

Let $l$ be a linear equivalence of $x$ and $x_{1}$ such that $\EqtMACRoH {l (1)}{1}$ and for all elements $x_{7}$ of $x$, for all elements $y$ of $x$, $\EqtMACRoH {l (x_{7} \times y)}{l (x_{7})\times l (y)}$. Then the algebra isomorphism of $l$ is an algebra isomorphism of $x$ and $x_{1}$.

AlgEquiv.ofRingEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra isomorphism of hf (from the name)

English

Assume that for all elements $x_{7}$ of $R$, $\EqtMACRoH {f (\operatorname{algebraMap} (R , x , x_{7}))}{\operatorname{algebraMap} (R , x_{1} , x_{7})}$. Then the algebra isomorphism of $\mathrm{hf}$ is an algebra isomorphism of $x$ and $x_{1}$.

AlgEquiv.refldefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the identity (from the name)

English

The identity is an algebra isomorphism of $x$ and $x$.

AlgEquiv.symmdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be an algebra isomorphism of $x$ and $x_{1}$. Then the inverse of $e$ is an algebra isomorphism of $x_{1}$ and $x$.

AlgEquiv.toAddEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the additive equivalence of self (from the name)

English

Let $\mathrm{self}$ be an algebra isomorphism of $A$ and $B$. Then the additive equivalence of $\mathrm{self}$ is an additive equivalence of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{AlgEquiv\_\_map\_add'}$ applied to $\mathrm{self}$.

AlgEquiv.toAlgHomdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra homomorphism of e (from the name)

English

Let $e$ be an algebra isomorphism of $x$ and $x_{1}$. Then the algebra homomorphism of $e$ is an algebra homomorphism of $x$ and $x_{1}$.

AlgEquiv.toAlgHomHomdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the algebra homomorphism homomorphism of $R$ and $A$ is a monoid homomorphism of the set of algebra isomorphisms of $A$ and $A$ and the set of algebra homomorphisms of $A$ and $A$.

AlgEquiv.toLinearEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the linear equivalence of e (from the name)

English

Let $e$ be an algebra isomorphism of $x$ and $x_{1}$. Then the linear equivalence of $e$ is a linear equivalence of $x$ and $x_{1}$.

AlgEquiv.toLinearMapdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the linear map of e (from the name)

English

Let $e$ be an algebra isomorphism of $x$ and $x_{1}$. Then the linear map of $e$ is a linear map of $x$ and $x_{1}$ defined as $\operatorname{toLinearMap}$ applied to the linear equivalence of $e$.

AlgEquiv.toLinearMapHomdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the linear map homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the linear map homomorphism of $R$ and $A$ is a monoid homomorphism of the set of algebra isomorphisms of $A$ and $A$ and the set of ends of $R$ and $A$ defined as the composition of the end and the algebra homomorphism homomorphism of $R$ and $A$.

AlgEquiv.toMulEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the multiplicative equivalence of self (from the name)

English

Let $\mathrm{self}$ be an algebra isomorphism of $A$ and $B$. Then the multiplicative equivalence of $\mathrm{self}$ is a multiplicative equivalence of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{AlgEquiv\_\_map\_mul'}$ applied to $\mathrm{self}$.

AlgEquiv.toRingEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the ring isomorphism of self (from the name)

English

Let $\mathrm{self}$ be an algebra isomorphism of $A$ and $B$. Then the ring isomorphism of $\mathrm{self}$ is a ring isomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$, $\mathrm{AlgEquiv\_\_map\_mul'}$ applied to $\mathrm{self}$ and $\mathrm{AlgEquiv\_\_map\_add'}$ applied to $\mathrm{self}$.

AlgEquiv.transdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be an algebra isomorphism of $x$ and $x_{1}$. Let $x_{11}$ be an algebra isomorphism of $x_{1}$ and $x_{2}$. Then the composition of $x_{10}$ and $x_{11}$ is an algebra isomorphism of $x$ and $x_{2}$.

AlgEquivClassclassMathlib.Algebra.Algebra.Equiv, predicate

Wording

no wording

English

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

AlgHom.uliftdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the lift of f (from the name)

English

Let $f$ be an algebra homomorphism of $S$ and $T$. Then the lift of $f$ is an algebra homomorphism of $\mathrm{ULift}$ applied to $S$ and $\mathrm{ULift}$ applied to $T$.

LinearEquiv.algEquivOfRingdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra isomorphism of e (from the name)

English

Let $e$ be a linear equivalence of $R$ and $A$. Then the algebra isomorphism of $e$ is an algebra isomorphism of $R$ and $A$.

LinearEquiv.conjAlgEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the conjugate algebra isomorphism of R and e (from the name)

English

Let $R$ be a set. Let $e$ be a linear equivalence of $x$ and $x_{1}$. Then the conjugate algebra isomorphism of $R$ and $e$ is an algebra isomorphism of the set of ends of $S$ and $x$ and the set of ends of $S$ and $x_{1}$.

MulSemiringAction.toAlgAutdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

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

English

Let $G$, $R$ and $A$ be sets. Then the algebra automorphism of $R$ and $A$ is a monoid homomorphism of $G$ and the set of algebra isomorphisms of $A$ and $A$.

MulSemiringAction.toAlgEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra isomorphism of g (from the name)

English

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

RingEquiv.equivIntAlgEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the equivalence integer algebra isomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the equivalence integer algebra isomorphism of $R$ and $S$ is an equivalence from the set of ring isomorphisms of $R$ and $S$ to the set of algebra isomorphisms of $R$ and $S$.

RingEquiv.equivNatAlgEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the equivalence natural algebra isomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the equivalence natural algebra isomorphism of $R$ and $S$ is an equivalence from the set of ring isomorphisms of $R$ and $S$ to the set of algebra isomorphisms of $R$ and $S$.

RingEquiv.toIntAlgEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the integer algebra isomorphism of f (from the name)

English

Let $f$ be a ring isomorphism of $R$ and $S$. Then the integer algebra isomorphism of $f$ is an algebra isomorphism of $R$ and $S$.

RingEquiv.toNatAlgEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the natural algebra isomorphism of f (from the name)

English

Let $f$ be a ring isomorphism of $R$ and $S$. Then the natural algebra isomorphism of $f$ is an algebra isomorphism of $R$ and $S$.

ULift.algEquivdefMathlib.Algebra.Algebra.Equiv, function or constant

Wording

the algebra isomorphism (from the name)

English

The algebra isomorphism is an algebra isomorphism of $\mathrm{ULift}$ applied to $A$ and $A$.

Mathlib.Algebra.Algebra.Hom

AlgHomstructureMathlib.Algebra.Algebra.Hom, type

Wording

algebra homomorphism of A and B (from the name)

English

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

AlgHom.compdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the composition of x7 and x8 (from the name)

English

Let $x_{7}$ be an algebra homomorphism of $B$ and $C$. Let $x_{8}$ be an algebra homomorphism of $A$ and $B$. Then the composition of $x_{7}$ and $x_{8}$ is an algebra homomorphism of $A$ and $C$.

AlgHom.iddefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the identity of R and A (from the name)

English

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

AlgHom.mk'defMathlib.Algebra.Algebra.Hom, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $A$ and $B$ such that for all elements $c$ of $R$, for all elements $x_{5}$ of $A$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {c}{x_{5}})}{\HSMulhSMulMACRoAL {c}{f (x_{5})}}$. Then $\operatorname{mk'}$ applied to $f$ and $h$ is an algebra homomorphism of $A$ and $B$.

AlgHom.ofClassdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the algebra homomorphism of f (from the name)

English

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

AlgHom.ofLinearMapdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the algebra homomorphism of f (from the name)

English

Let $f$ be a linear map of $A$ and $B$ such that $\EqtMACRoH {f (1)}{1}$ and for all elements $x_{5}$ of $A$, for all elements $y$ of $A$, $\EqtMACRoH {f (x_{5} \times y)}{f (x_{5})\times f (y)}$. Then the algebra homomorphism of $f$ is an algebra homomorphism of $A$ and $B$.

AlgHom.toAddMonoidHom'defMathlib.Algebra.Algebra.Hom, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $A$ and $B$ defined as the additive monoid homomorphism of the ring homomorphism of $f$.

AlgHom.toEnddefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the end (from the name)

English

The end is a monoid homomorphism of the set of algebra homomorphisms of $A$ and $A$ and the set of ends of $R$ and $A$.

AlgHom.toLinearMapdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the linear map of x5 (from the name)

English

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

AlgHom.toMonoidHom'defMathlib.Algebra.Algebra.Hom, function or constant

Wording

the monoid homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the monoid homomorphism of $f$ is a monoid homomorphism of $A$ and $B$ defined as the monoid homomorphism of the ring homomorphism of $f$.

AlgHomClassclassMathlib.Algebra.Algebra.Hom, predicate

Wording

no wording

English

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

Algebra.algHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the algebra homomorphism of S and A (from the name)

English

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

Algebra.ofIddefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the algebra of R and A (from the name)

English

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

IsScalarTower.toAlgHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the algebra homomorphism of S and A (from the name)

English

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

MulSemiringAction.toAlgHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the algebra homomorphism of m (from the name)

English

Let $R$ and $A$ be sets. Let $m$ be an element of $M$. Then the algebra homomorphism of $m$ is an algebra homomorphism of $A$ and $A$.

RingHom.equivIntAlgHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the equivalence integer algebra homomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the equivalence integer algebra homomorphism of $R$ and $S$ is an equivalence from the set of ring homomorphisms of $R$ and $S$ to the set of algebra homomorphisms of $R$ and $S$.

RingHom.equivNatAlgHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the equivalence natural algebra homomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the equivalence natural algebra homomorphism of $R$ and $S$ is an equivalence from the set of ring homomorphisms of $R$ and $S$ to the set of algebra homomorphisms of $R$ and $S$.

RingHom.toIntAlgHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the integer algebra homomorphism of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the integer algebra homomorphism of $f$ is an algebra homomorphism of $R$ and $S$.

RingHom.toNatAlgHomdefMathlib.Algebra.Algebra.Hom, function or constant

Wording

the natural algebra homomorphism of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the natural algebra homomorphism of $f$ is an algebra homomorphism of $R$ and $S$.

Mathlib.Algebra.Algebra.Hom.Rat

RingEquiv.equivRatAlgEquivdefMathlib.Algebra.Algebra.Hom.Rat, function or constant

Wording

the equivalence rational number algebra isomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the equivalence rational number algebra isomorphism of $R$ and $S$ is an equivalence from the set of ring isomorphisms of $R$ and $S$ to the set of algebra isomorphisms of $R$ and $S$.

RingEquiv.toRatAlgEquivdefMathlib.Algebra.Algebra.Hom.Rat, function or constant

Wording

the rational number algebra isomorphism of f (from the name)

English

Let $f$ be a ring isomorphism of $R$ and $S$. Then the rational number algebra isomorphism of $f$ is an algebra isomorphism of $R$ and $S$.

RingHom.equivRatAlgHomdefMathlib.Algebra.Algebra.Hom.Rat, function or constant

Wording

the equivalence rational number algebra homomorphism of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the equivalence rational number algebra homomorphism of $R$ and $S$ is an equivalence from the set of ring homomorphisms of $R$ and $S$ to the set of algebra homomorphisms of $R$ and $S$.

RingHom.toRatAlgHomdefMathlib.Algebra.Algebra.Hom.Rat, function or constant

Wording

the rational number algebra homomorphism of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the rational number algebra homomorphism of $f$ is an algebra homomorphism of $R$ and $S$.

Mathlib.Algebra.Algebra.NonUnitalHom

AlgHom.toNonUnitalAlgHomdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the non unital algebra homomorphism of f (from the name)

English

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

NonUnitalAlgHomstructureMathlib.Algebra.Algebra.NonUnitalHom, type

Wording

non unital algebra homomorphism of A and B (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $R$ and $S$. Let $A$ and $B$ be sets. Then the non unital algebra homomorphisms of $A$ and $B$ are a basic type.

NonUnitalAlgHom.compdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a non unital algebra homomorphism of $B$ and $C$. Let $g$ be a non unital algebra homomorphism of $A$ and $B$. Then the composition of $f$ and $g$ is a non unital algebra homomorphism of $A$ and $C$.

NonUnitalAlgHom.fstdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the first component of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the first component of $A$ and $B$ is a non unital algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$.

NonUnitalAlgHom.iddefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

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

English

Let $R$ and $A$ be sets. Then the identity map of $R$ and $A$ is a non unital algebra homomorphism of $A$ and $A$.

NonUnitalAlgHom.inldefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the left injection of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the left injection of $A$ and $B$ is a non unital algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of $1$ and $0$.

NonUnitalAlgHom.inrdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the right injection of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the right injection of $A$ and $B$ is a non unital algebra homomorphism of $B$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of $0$ and $1$.

NonUnitalAlgHom.inversedefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a non unital algebra homomorphism of $A$ and $x_{3}$. Let $g$ be a function from elements of $x_{3}$ to elements of $A$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$ and $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is a non unital algebra homomorphism of $x_{3}$ and $A$.

NonUnitalAlgHom.inverse'defMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Let $g$ be a function from elements of $B$ to elements of $A$. Assume that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $x_{7}$ and $\operatorname{coe}$ applied to $x_{2}$. Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Assume that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is a non unital algebra homomorphism of $B$ and $A$.

NonUnitalAlgHom.proddefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Let $g$ be a non unital algebra homomorphism of $A$ and $C$. Then the product of $f$ and $g$ is a non unital algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

NonUnitalAlgHom.prodEquivdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the product equivalence (from the name)

English

The product equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of non unital algebra homomorphisms of $A$ and $B$ and the set of non unital algebra homomorphisms of $A$ and $C$ to the set of non unital algebra homomorphisms of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

NonUnitalAlgHom.restrictScalarsdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a non unital algebra homomorphism of $A$ and $B$.

NonUnitalAlgHom.snddefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the second component of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the second component of $A$ and $B$ is a non unital algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$.

NonUnitalAlgHom.toMulHomdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the multiplicative homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a non unital algebra homomorphism of $A$ and $B$. Then the multiplicative homomorphism of $\mathrm{self}$ is a multiplicative homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toMulActionHom}$ applied to $\operatorname{toDistribMulActionHom}$ applied to $\mathrm{self}$ and $\mathrm{NonUnitalAlgHom\_\_map\_mul'}$ applied to $\mathrm{self}$.

NonUnitalAlgHomClassdefMathlib.Algebra.Algebra.NonUnitalHom, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$, $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{NonUnitalAlgHomClass}$ holds for $F$, $R$, $A$ and $B$, if $\mathrm{NonUnitalAlgSemiHomClass}$ holds for $F$, the identity map of $R$, $A$ and $B$.

NonUnitalAlgHomClass.toNonUnitalAlgHomdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the non unital algebra homomorphism of f (from the name)

English

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

NonUnitalAlgHomClass.toNonUnitalAlgSemiHomdefMathlib.Algebra.Algebra.NonUnitalHom, function or constant

Wording

the non unital algebra semi homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the non unital algebra semi homomorphism of $f$ is a non unital algebra homomorphism of $A$ and $B$.

NonUnitalAlgSemiHomClassclassMathlib.Algebra.Algebra.NonUnitalHom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of monoid homomorphisms of $R$ and $S$. Let $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{NonUnitalAlgSemiHomClass}$ holds for $F$, $x_{2}$, $A$ and $B$.

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

NonUnitalAlgHom.codRestrictdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

no wording

English

Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Let $S$ be a non unital subalgebra of $R$ and $B$ such that for all elements $x_{6}$ of $A$, $\MembershipmemMACRoT {S}{f (x_{6})}$. Then $\operatorname{codRestrict}$ applied to $f$, $S$ and $\mathrm{hf}$ is a non unital algebra homomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$.

NonUnitalAlgHom.equalizerdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the equalizer of x5 and x6 (from the name)

English

Let $x_{5}$ and $x_{6}$ be non unital algebra homomorphisms of $A$ and $B$. Then the equalizer of $x_{5}$ and $x_{6}$ is a non unital subalgebra of $R$ and $A$.

NonUnitalAlgHom.rangedefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the range of x5 (from the name)

English

Let $x_{5}$ be a non unital algebra homomorphism of $A$ and $B$. Then the range of $x_{5}$ is a non unital subalgebra of $R$ and $B$.

NonUnitalAlgHom.rangeRestrictdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

no wording

English

Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a non unital algebra homomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$ defined as $\operatorname{codRestrict}$ applied to $f$, the range of $f$ and $\mathrm{NonUnitalAlgHom\_\_mem\_range\_self}$ applied to $f$.

NonUnitalAlgebra.adjoindefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $s$ be an element of $\wp A$. Then $\operatorname{adjoin}$ applied to $R$ and $s$ is a non unital subalgebra of $R$ and $A$.

NonUnitalAlgebra.gidefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

no wording

English

$\operatorname{gi}$ is a Galois insertion of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{instSetLike}$.

NonUnitalAlgebra.toTopdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the top (from the name)

English

The top is a non unital algebra homomorphism of $A$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$.

NonUnitalSubalgebrastructureMathlib.Algebra.Algebra.NonUnitalSubalgebra, type

Wording

non unital subalgebra of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the non unital subalgebras of $R$ and $A$ are a basic type.

NonUnitalSubalgebra.centerdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the center of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the center of $R$ and $A$ is a non unital subalgebra of $R$ and $A$ defined as $\operatorname{mk}$ applied to the center of $A$ and $\mathrm{Set\_\_smul\_mem\_center}$.

NonUnitalSubalgebra.centralizerdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the centralizer of R and s (from the docstring)

English

Let $R$ be a set. Let $s$ be an element of $\wp A$. Then the centralizer of $R$ and $s$ is a non unital subalgebra of $R$ and $A$ defined as $\operatorname{mk}$ applied to the centralizer of $s$ and $\mathrm{Set\_\_smul\_mem\_centralizer}$.

NonUnitalSubalgebra.comapdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the preimage of f and S (from the name)

English

Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Let $S$ be a non unital subalgebra of $R$ and $B$. Then the preimage of $f$ and $S$ is a non unital subalgebra of $R$ and $A$.

NonUnitalSubalgebra.copydefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the copy of S and s (from the name)

English

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

NonUnitalSubalgebra.iSupLiftdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the supremum lift of f and hf (from the name)

English

Let $K$ be a function from elements of $x_{5}$ to non unital subalgebras of $R$ and $A$ such that $\mathrm{Directed}$ holds for the function that maps $x_{9}$ and $x_{10}$ to $\mathrm{Leq} (x_{9} , x_{10})$ and $K$. Let $f$ be a function from elements $i_{1}$ of $x_{5}$ to non unital algebra homomorphisms of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {K (i_{1})}{x_{8}})}$ and $B$ such that for all elements $i$ and $j$ of $x_{5}$, for all elements $h_{3}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (K (i), K (j))$, $f$ applied to $i$ is equal to the composition of $f$ applied to $j$ and the inclusion of $h_{3}$. Let $T$ be a non unital subalgebra of $R$ and $A$ such that $T$ is equal to the supremum of $K$. Then the supremum lift of $i_{1}$ and $\mathrm{hf}$ is a non unital algebra homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {T}{x_{6}})}$ and $B$.

NonUnitalSubalgebra.inclusiondefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the inclusion of h (from the name)

English

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

NonUnitalSubalgebra.mapdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the map of f and S (from the name)

English

Let $f$ be a non unital algebra homomorphism of $A$ and $B$. Let $S$ be a non unital subalgebra of $R$ and $A$. Then the map of $f$ and $S$ is a non unital subalgebra of $R$ and $B$.

NonUnitalSubalgebra.ofClassdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subalgebra of s (from the name)

English

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

NonUnitalSubalgebra.proddefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the product of S and x5 (from the name)

English

Let $S$ be a non unital subalgebra of $R$ and $A$. Let $x_{5}$ be a non unital subalgebra of $R$ and $B$. Then the product of $S$ and $x_{5}$ is a non unital subalgebra of $R$ and $\mathrm{Prod}$ applied to $A$ and $B$.

NonUnitalSubalgebra.toNonUnitalSubringdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subring of S (from the name)

English

Let $S$ be a non unital subalgebra of $R$ and $A$. Then the non unital subring of $S$ is a non unital subring of $A$.

NonUnitalSubalgebra.toNonUnitalSubring'defMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subring (from the name)

English

The non unital subring is an order embedding of the set of non unital subalgebras of $R$ and $A$ and the set of non unital subrings of $A$.

NonUnitalSubalgebra.toNonUnitalSubsemiring'defMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subsemiring (from the name)

English

The non unital subsemiring is an order embedding of the set of non unital subalgebras of $R$ and $A$ and the set of non unital subsemirings of $A$.

NonUnitalSubalgebra.toSubmoduledefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the submodule of self (from the name)

English

Let $\mathrm{self}$ be a non unital subalgebra of $R$ and $A$. Then the submodule of $\mathrm{self}$ is a submodule of $R$ and $A$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddSubmonoid}$ applied to $\operatorname{toNonUnitalSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{NonUnitalSubalgebra\_\_smul\_mem'}$ applied to $\mathrm{self}$.

NonUnitalSubalgebra.toSubmodule'defMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the submodule (from the name)

English

The submodule is an order embedding of the set of non unital subalgebras of $R$ and $A$ and the set of submodules of $R$ and $A$.

NonUnitalSubalgebra.toSubmoduleEquivdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the submodule equivalence of S (from the name)

English

Let $S$ be a non unital subalgebra of $R$ and $A$. Then the submodule equivalence of $S$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toSubmodule} (S)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$.

NonUnitalSubalgebraClass.subtypedefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the subtype of s (from the name)

English

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

Submodule.toNonUnitalSubalgebradefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subalgebra of p and h_mul (from the name)

English

Let $p$ be a submodule of $R$ and $A$ such that for all elements $x_{3}$ and $y$ of $A$, if $x_{3}$ is an element of $p$, then if $y$ is an element of $p$, then $x_{3} \times y$ is an element of $p$. Then the non unital subalgebra of $p$ and $\mathrm{h\_mul}$ is a non unital subalgebra of $R$ and $A$.

nonUnitalSubalgebraOfNonUnitalSubringdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subalgebra of S (from the name)

English

Let $S$ be a non unital subring of $R$. Then the non unital subalgebra of $S$ is a non unital subalgebra of $\Integer$ and $R$.

nonUnitalSubalgebraOfNonUnitalSubsemiringdefMathlib.Algebra.Algebra.NonUnitalSubalgebra, function or constant

Wording

the non unital subalgebra of S (from the name)

English

Let $S$ be a non unital subsemiring of $R$. Then the non unital subalgebra of $S$ is a non unital subalgebra of $\Natural$ and $R$.

Mathlib.Algebra.Algebra.Operations

Submodule.equivOppositedefMathlib.Algebra.Algebra.Operations, function or constant

Wording

the equivalence opposite (from the name)

English

The equivalence opposite is a ring isomorphism of the set of submodules of $R$ and the set of multiplicative opposites of $A$ and the set of multiplicative opposites of the set of submodules of $R$ and $A$.

Submodule.mapHomdefMathlib.Algebra.Algebra.Operations, function or constant

Wording

the map homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $\mathrm{A'}$. Then the map homomorphism of $f$ is a ring homomorphism of the set of submodules of $R$ and $A$ and the set of submodules of $R$ and $\mathrm{A'}$.

Submodule.span.ringHomdefMathlib.Algebra.Algebra.Operations, function or constant

Wording

the ring homomorphism (from the name)

English

The ring homomorphism is a ring homomorphism of the set of set semirings of $A$ and the set of submodules of $R$ and $A$.

Submodule.spanSingletondefMathlib.Algebra.Algebra.Operations, function or constant

Wording

the span singleton of R (from the name)

English

Let $R$ be a set. Then the span singleton of $R$ is a monoid with zero homomorphism of $A$ and the set of submodules of $R$ and $A$.

Mathlib.Algebra.Algebra.Opposite

AlgEquiv.moduleEndSelfdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the module end self of R (from the name)

English

Let $R$ be a set. Then the module end self of $R$ is an algebra isomorphism of the set of multiplicative opposites of $A$ and the set of ends of $A$ and $A$.

AlgEquiv.moduleEndSelfOpdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the module end self opposite of R (from the name)

English

Let $R$ be a set. Then the module end self opposite of $R$ is an algebra isomorphism of $A$ and the set of ends of the set of multiplicative opposites of $A$ and $A$.

AlgEquiv.opdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of algebra isomorphisms of $A$ and $B$ to the set of algebra isomorphisms of the set of multiplicative opposites of $A$ and the set of multiplicative opposites of $B$.

AlgEquiv.opCommdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

no wording

English

$\operatorname{opComm}$ is an equivalence from the set of algebra isomorphisms of $A$ and the set of multiplicative opposites of $B$ to the set of algebra isomorphisms of the set of multiplicative opposites of $A$ and $B$ defined as the composition of the opposite and the equivalence congruence of the identity and the inverse of the opposite opposite of $R$ and $B$.

AlgEquiv.opOpdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite opposite of R and A (from the name)

English

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

AlgEquiv.toOppositedefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite of R and A (from the name)

English

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

AlgEquiv.unopdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of algebra isomorphisms of the set of multiplicative opposites of $A$ and the set of multiplicative opposites of $B$ to the set of algebra isomorphisms of $A$ and $B$ defined as the inverse of the opposite.

AlgHom.fromOppositedefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

no wording

English

Let $f$ be an algebra homomorphism of $A$ and $B$ such that for all elements $x_{5}$ and $y$ of $A$, $\mathrm{Commute}$ holds for $f$ applied to $x_{5}$ and $f$ applied to $y$. Then $\operatorname{fromOpposite}$ applied to $f$ and $\mathrm{hf}$ is an algebra homomorphism of the set of multiplicative opposites of $A$ and $B$.

AlgHom.opdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of algebra homomorphisms of $A$ and $B$ to the set of algebra homomorphisms of the set of multiplicative opposites of $A$ and the set of multiplicative opposites of $B$.

AlgHom.opCommdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

no wording

English

$\operatorname{opComm}$ is an equivalence from the set of algebra homomorphisms of $A$ and the set of multiplicative opposites of $B$ to the set of algebra homomorphisms of the set of multiplicative opposites of $A$ and $B$ defined as the composition of the opposite and the arrow congruence of the identity and the inverse of the opposite opposite of $R$ and $B$.

AlgHom.toOppositedefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite of f and hf (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$ such that for all elements $x_{5}$ and $y$ of $A$, $\mathrm{Commute}$ holds for $f$ applied to $x_{5}$ and $f$ applied to $y$. Then the opposite of $f$ and $\mathrm{hf}$ is an algebra homomorphism of $A$ and the set of multiplicative opposites of $B$.

AlgHom.unopdefMathlib.Algebra.Algebra.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of algebra homomorphisms of the set of multiplicative opposites of $A$ and the set of multiplicative opposites of $B$ to the set of algebra homomorphisms of $A$ and $B$ defined as the inverse of the opposite.

Mathlib.Algebra.Algebra.Pi

AlgEquiv.funUniquedefMathlib.Algebra.Algebra.Pi, function or constant

Wording

no wording

English

Let $R$, $x$ and $S$ be sets. Then $\operatorname{funUnique}$ applied to $R$, $x$ and $S$ is an algebra isomorphism of the set of functions from elements of $x$ to elements of $S$ and $S$.

AlgEquiv.piCongrLeftdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the left product congruence of x1 and e (from the name)

English

Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Let $e$ be an equivalence from $x_{5}$ to $x$. Then the left product congruence of $x_{1}$ and $e$ is an algebra isomorphism of the set of functions from elements $i$ of $x_{5}$ to elements of $x_{1}$ applied to $e$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ defined as the inverse of the left product congruence of $x_{1}$ and the inverse of $e$.

AlgEquiv.piCongrLeft'defMathlib.Algebra.Algebra.Pi, function or constant

Wording

the left product congruence of x1 and e (from the name)

English

Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Let $e$ be an equivalence from $x$ to $x_{5}$. Then the left product congruence of $x_{1}$ and $e$ is an algebra isomorphism of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{5}$ to elements of $x_{1}$ applied to $\operatorname{symm}$ applied to $e$ and $i_{1}$.

AlgEquiv.piCongrRightdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the right product congruence of e (from the name)

English

Let $e$ be a function from elements $i_{2}$ of $x$ to algebra isomorphisms of $x_{1}$ applied to $i_{2}$ and $x_{2}$ applied to $i_{2}$. Then the right product congruence of $i_{2}$ is an algebra isomorphism of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$.

AlgEquiv.piMulOppositedefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the opposite of R and x1 (from the docstring)

English

Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Then the opposite of $R$ and $x_{1}$ is an algebra isomorphism of the set of multiplicative opposites of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to multiplicative opposites of $x_{1}$ applied to $i_{1}$.

AlgEquiv.sumArrowEquivProdArrowdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the sum arrow equivalence product arrow of R and S (from the name)

English

Let $x$, $x_{1}$, $R$ and $S$ be sets. Then the sum arrow equivalence product arrow of $R$ and $S$ is an algebra isomorphism of the set of functions from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to elements of $S$ and $\mathrm{Prod}$ applied to the set of functions from elements of $x$ to elements of $S$ and the set of functions from elements of $x_{1}$ to elements of $S$.

AlgHom.compLeftdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the left composition of f and x5 (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $x_{5}$ be a set. Then the left composition of $f$ and $x_{5}$ is an algebra homomorphism of the set of functions from elements of $x_{5}$ to elements of $A$ and the set of functions from elements of $x_{5}$ to elements of $B$.

AlgHom.pidefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the product of g (from the name)

English

Let $g$ be a function from elements $i_{1}$ of $x$ to algebra homomorphisms of $B$ and $A$ applied to $i_{1}$. Then the product of $i_{1}$ is an algebra homomorphism of $B$ and the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$.

Pi.algebraMapdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

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

English

Let $x$, $R$ and $A$ be sets. Then the algebra map of $R$ and $A$ is a linear map of the set of functions from elements of $x$ to elements of $R$ and the set of functions from elements of $x$ to elements of $A$.

Pi.constAlgHomdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the constant algebra homomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the constant algebra homomorphism of $A$ and $B$ is an algebra homomorphism of $B$ and the set of functions from elements of $A$ to elements of $B$.

Pi.evalAlgHomdefMathlib.Algebra.Algebra.Pi, function or constant

Wording

the evaluation algebra homomorphism of A and i (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then the evaluation algebra homomorphism of $A$ and $i$ is an algebra homomorphism of the set of functions from elements $i_{1}$ of $x$ to elements of $A$ applied to $i_{1}$ and $A$ applied to $i$.

Mathlib.Algebra.Algebra.Prod

AlgEquiv.prodCongrdefMathlib.Algebra.Algebra.Prod, function or constant

Wording

the product congruence of l and r (from the name)

English

Let $l$ be an algebra isomorphism of $S$ and $A$. Let $r$ be an algebra isomorphism of $T$ and $B$. Then the product congruence of $l$ and $r$ is an algebra isomorphism of $\mathrm{Prod}$ applied to $S$ and $T$ and $\mathrm{Prod}$ applied to $A$ and $B$.

AlgEquiv.prodUniquedefMathlib.Algebra.Algebra.Prod, function or constant

Wording

no wording

English

$\operatorname{prodUnique}$ is an algebra isomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$.

AlgEquiv.uniqueProddefMathlib.Algebra.Algebra.Prod, function or constant

Wording

the unique product (from the name)

English

The unique product is an algebra isomorphism of $\mathrm{Prod}$ applied to $B$ and $A$ and $A$.

AlgHom.fstdefMathlib.Algebra.Algebra.Prod, function or constant

Wording

the first component of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the first component of $A$ and $B$ is an algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$.

AlgHom.proddefMathlib.Algebra.Algebra.Prod, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $g$ be an algebra homomorphism of $A$ and $C$. Then the product of $f$ and $g$ is an algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

AlgHom.prodEquivdefMathlib.Algebra.Algebra.Prod, function or constant

Wording

the product equivalence (from the name)

English

The product equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of algebra homomorphisms of $A$ and $B$ and the set of algebra homomorphisms of $A$ and $C$ to the set of algebra homomorphisms of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

AlgHom.prodMapdefMathlib.Algebra.Algebra.Prod, function or constant

Wording

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

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $g$ be an algebra homomorphism of $C$ and $D$. Then the product map of $f$ and $g$ is an algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $C$ and $\mathrm{Prod}$ applied to $B$ and $D$.

AlgHom.snddefMathlib.Algebra.Algebra.Prod, function or constant

Wording

the second component of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the second component of $A$ and $B$ is an algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$.

Mathlib.Algebra.Algebra.RestrictScalars

RestrictScalarsdefMathlib.Algebra.Algebra.RestrictScalars, type

Wording

no wording

English

Let $\mathrm{\_R}$, $\mathrm{\_S}$ and $M$ be sets. Then an element of $\mathrm{RestrictScalars}$ applied to $\mathrm{\_R}$, $\mathrm{\_S}$ and $M$ is an element of the function that maps $\mathrm{\_R}$, $\mathrm{\_S}$ and $M$ to $M$.

RestrictScalars.addEquivdefMathlib.Algebra.Algebra.RestrictScalars, function or constant

Wording

the additive equivalence of S and M (from the name)

English

Let $R$, $S$ and $M$ be sets. Then the additive equivalence of $S$ and $M$ is an additive equivalence of $\mathrm{RestrictScalars}$ applied to $R$, $S$ and $M$ and $M$ defined as the identity map of $M$.

RestrictScalars.lsmuldefMathlib.Algebra.Algebra.RestrictScalars, function or constant

Wording

no wording

English

Let $R$, $S$ and $M$ be sets. Then $\operatorname{lsmul}$ applied to $R$, $S$ and $M$ is an algebra homomorphism of $S$ and the set of ends of $R$ and $\mathrm{RestrictScalars}$ applied to $R$, $S$ and $M$ defined as $\operatorname{lsmul}$ applied to $R$, $R$ and $\mathrm{RestrictScalars}$ applied to $R$, $S$ and $M$.

RestrictScalars.ringEquivdefMathlib.Algebra.Algebra.RestrictScalars, function or constant

Wording

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

English

Let $R$, $S$ and $A$ be sets. Then the ring isomorphism of $S$ and $A$ is a ring isomorphism of $\mathrm{RestrictScalars}$ applied to $R$, $S$ and $A$ and $A$ defined as the identity map of $\mathrm{RestrictScalars}$ applied to $R$, $S$ and $A$.

Mathlib.Algebra.Algebra.Shrink

Shrink.algEquivdefMathlib.Algebra.Algebra.Shrink, function or constant

Wording

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

English

Let $R$ and $x$ be sets. Then the algebra isomorphism of $R$ and $x$ is an algebra isomorphism of the set of shrinks of $x$ and $x$ defined as the algebra isomorphism of $R$ and the inverse of the equivalence shrink of $x$.

Mathlib.Algebra.Algebra.Spectrum.Basic

IsUnit.subInvSMuldefMathlib.Algebra.Algebra.Spectrum.Basic, function or constant

Wording

the difference inverse product of h (from the name)

English

Assume that $\HSMulhSMulMACRoAL {r}{\operatorname{algebraMap} (R , A , s)}- a$ is a unit. Then the difference inverse product of $h$ is a unit of $A$.

resolventdefMathlib.Algebra.Algebra.Spectrum.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $A$. Let $r$ be an element of $R$. Then $\mathrm{resolvent}$ applied to $a$ and $r$ is an element of $A$ defined as the inverse of $\operatorname{algebraMap} (R , A , r)- a$.

resolventSetdefMathlib.Algebra.Algebra.Spectrum.Basic, function or constant

Wording

the resolvent set of R and a (from the name)

English

Let $R$ be a set. Let $a$ be an element of $A$. Then the resolvent set of $R$ and $a$ is an element of $\wp R$ defined as $\operatorname{ofPred}$ applied to the function that maps $r$ to the proposition that $\operatorname{algebraMap} (R , A , r)- a$ is a unit.

spectrumdefMathlib.Algebra.Algebra.Spectrum.Basic, function or constant

Wording

the spectrum of R and a (from the name)

English

Let $R$ be a set. Let $a$ be an element of $A$. Then the spectrum of $R$ and $a$ is an element of $\wp R$ defined as the complement of the resolvent set of $R$ and $a$.

Mathlib.Algebra.Algebra.Spectrum.Pi

PreQuasiregular.toPidefMathlib.Algebra.Algebra.Spectrum.Pi, function or constant

Wording

the product of x1 (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to sets. Then the product of $x_{1}$ is a multiplicative equivalence of $\mathrm{PreQuasiregular}$ applied to the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $\mathrm{PreQuasiregular}$ applied to $x_{1}$ applied to $i_{1}$.

PreQuasiregular.toProddefMathlib.Algebra.Algebra.Spectrum.Pi, function or constant

Wording

the product of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the product of $A$ and $B$ is a multiplicative equivalence of $\mathrm{PreQuasiregular}$ applied to $\mathrm{Prod}$ applied to $A$ and $B$ and $\mathrm{Prod}$ applied to $\mathrm{PreQuasiregular}$ applied to $A$ and $\mathrm{PreQuasiregular}$ applied to $B$.

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

IsQuasiregulardefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, predicate

Wording

x1 is quasiregular (from the name)

English

Let $x_{1}$ be an element of $R$. Then $x_{1}$ is quasiregular, if there exists a unit $u$ of $\mathrm{PreQuasiregular}$ applied to $R$, such that $\operatorname{symm}$ applied to the equivalence and the underlying value in the base of $u$ is equal to $x_{1}$.

NonnegSpectrumClassclassMathlib.Algebra.Algebra.Spectrum.Quasispectrum, predicate

Wording

no wording

English

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

PreQuasiregularstructureMathlib.Algebra.Algebra.Spectrum.Quasispectrum, type

Wording

no wording

English

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

PreQuasiregular.equivdefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an element of $\EquivMACRoAE {R}{\mathrm{PreQuasiregular} (R)}$.

PreQuasiregular.valdefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, function or constant

Wording

the value of self (from the name)

English

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

QuasispectrumRestrictsstructureMathlib.Algebra.Algebra.Spectrum.Quasispectrum, predicate

Wording

no wording

English

Let $a$ be an element of $A$. Let $f$ be a function from elements of $S$ to elements of $R$. Then we can say that $\mathrm{QuasispectrumRestricts}$ holds for $a$ and $f$.

SpectrumRestrictsdefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, predicate

Wording

no wording

English

Let $a$ be an element of $A$. Let $f$ be a function from elements of $S$ to elements of $R$. Then $\mathrm{SpectrumRestricts}$ holds for $a$ and $f$, if $\mathrm{QuasispectrumRestricts}$ holds for $a$ and $f$.

Unitization.unitsFstOnedefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, function or constant

Wording

the unit first component one of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the unit first component one of $R$ and $A$ is a subgroup of the set of units of the set of unitizations of $R$ and $A$.

Unitization.unitsFstOne_mulEquiv_quasiregulardefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\mathrm{Unitization\_\_unitsFstOne\_mulEquiv\_quasiregular}$ applied to $R$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{unitsFstOne} (R , A)}{x_{3}})}$ and $\UnitsMACRoAO {\mathrm{PreQuasiregular} (A)}$.

quasispectrumdefMathlib.Algebra.Algebra.Spectrum.Quasispectrum, function or constant

Wording

the quasispectrum of R and a (from the name)

English

Let $R$ be a set. Let $a$ be an element of $A$. Then the quasispectrum of $R$ and $a$ is an element of $\wp R$ defined as $\operatorname{ofPred}$ applied to the function that maps $r$ to the proposition that for all elements $\mathrm{hr}$ of $\mathrm{Proof}$ applied to the proposition that $r$ is a unit, $\operatorname{neg}$ applied to $\HSMulhSMulMACRoAL {\operatorname{inv} (\operatorname{unit} (\mathrm{hr}))}{a}$ is not quasiregular.

Mathlib.Algebra.Algebra.StrictPositivity

IsStrictlyPositivedefMathlib.Algebra.Algebra.StrictPositivity, predicate

Wording

a is strictly positive (from the docstring)

English

generation took over the time limit

Mathlib.Algebra.Algebra.Subalgebra.Basic

AlgEquiv.ofInjectivedefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

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

English

Let $f$ be an algebra homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the algebra isomorphism of $f$ and $\mathrm{hf}$ is an algebra isomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$.

AlgEquiv.ofInjectiveFielddefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the algebra isomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $E$ and $F$. Then the algebra isomorphism of $f$ is an algebra isomorphism of $E$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$.

AlgEquiv.ofLeftInversedefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the algebra isomorphism of h (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the algebra isomorphism of $h$ is an algebra isomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$.

AlgEquiv.subalgebraMapdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra map of e and S (from the name)

English

Let $e$ be an algebra isomorphism of $A$ and $B$. Let $S$ be a subalgebra of $R$ and $A$. Then the subalgebra map of $e$ and $S$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toAlgHom} (e), S)}{x_{6}})}$.

AlgHom.codRestrictdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

no wording

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $S$ be a subalgebra of $R$ and $B$ such that for all elements $x_{6}$ of $A$, $\MembershipmemMACRoT {S}{f (x_{6})}$. Then $\operatorname{codRestrict}$ applied to $f$, $S$ and $\mathrm{hf}$ is an algebra homomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$.

AlgHom.equalizerdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the equalizer of x5 and x6 (from the name)

English

Let $x_{5}$ and $x_{6}$ be algebra homomorphisms of $A$ and $B$. Then the equalizer of $x_{5}$ and $x_{6}$ is a subalgebra of $R$ and $A$.

AlgHom.rangedefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the range of x5 (from the name)

English

Let $x_{5}$ be an algebra homomorphism of $A$ and $B$. Then the range of $x_{5}$ is a subalgebra of $R$ and $B$.

AlgHom.rangeRestrictdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

no wording

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then $\operatorname{rangeRestrict}$ applied to $f$ is an algebra homomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$ defined as $\operatorname{codRestrict}$ applied to $f$, the range of $f$ and $\mathrm{AlgHom\_\_mem\_range\_self}$ applied to $f$.

AlgHom.subalgebraMapdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra map of S and f (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Let $f$ be an algebra homomorphism of $A$ and $B$. Then the subalgebra map of $S$ and $f$ is an algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{map} (f , S)}{x_{6}})}$.

NonUnitalSubalgebra.toSubalgebradefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra of S and h1 (from the name)

English

Let $S$ be a non unital subalgebra of $R$ and $A$ such that $1$ is an element of $S$. Then the subalgebra of $S$ and $h_{1}$ is a subalgebra of $R$ and $A$.

SubalgebrastructureMathlib.Algebra.Algebra.Subalgebra.Basic, type

Wording

subalgebra of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the subalgebras of $R$ and $A$ are a basic type.

Subalgebra.centerdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the center of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the center of $R$ and $A$ is a subalgebra of $R$ and $A$ defined as $\operatorname{mk}$ applied to the center of $A$ and $\mathrm{Set\_\_algebraMap\_mem\_center}$.

Subalgebra.centralizerdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the centralizer of R and s (from the docstring)

English

Let $R$ be a set. Let $s$ be an element of $\wp A$. Then the centralizer of $R$ and $s$ is a subalgebra of $R$ and $A$ defined as $\operatorname{mk}$ applied to the centralizer of $s$ and $\mathrm{Set\_\_algebraMap\_mem\_centralizer}$.

Subalgebra.comapdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the preimage of f and S (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $S$ be a subalgebra of $R$ and $B$. Then the preimage of $f$ and $S$ is a subalgebra of $R$ and $A$.

Subalgebra.copydefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the copy of S and s (from the name)

English

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

Subalgebra.equivMapOfInjectivedefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

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

English

Let $S$ be a subalgebra of $R$ and $A$. Let $f$ be an algebra homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $S$ and $f$ is an algebra isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{map} (f , S)}{x_{6}})}$.

Subalgebra.equivOfEqdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the equivalence of S and T (from the name)

English

Let $S$ and $T$ be subalgebras of $R$ and $A$ such that $\EqtMACRoH {S}{T}$. Then the equivalence of $S$ and $T$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {T}{x_{4}})}$.

Subalgebra.inclusiondefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $S \leq T$. Then the inclusion of $h$ is an algebra homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {T}{x_{4}})}$.

Subalgebra.mapdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the map of f and S (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $S$ be a subalgebra of $R$ and $A$. Then the map of $f$ and $S$ is a subalgebra of $R$ and $B$.

Subalgebra.ofClassdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra of s (from the name)

English

Let $s$ be an element of $S$. Then the subalgebra of $s$ is a subalgebra of $R$ and $A$.

Subalgebra.toAddSubmonoiddefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the additive submonoid of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the additive submonoid of $S$ is an additive submonoid of $A$ defined as the additive submonoid of $\operatorname{toSubsemiring}$ applied to $S$.

Subalgebra.toNonUnitalSubalgebradefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the non unital subalgebra of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the non unital subalgebra of $S$ is a non unital subalgebra of $R$ and $A$.

Subalgebra.toSubmoduledefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the submodule (from the name)

English

The submodule is an order embedding of the set of subalgebras of $R$ and $A$ and the set of submodules of $R$ and $A$.

Subalgebra.toSubmoduleEquivdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the submodule equivalence of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the submodule equivalence of $S$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toSubmodule} (S)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$.

Subalgebra.toSubringdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subring of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the subring of $S$ is a subring of $A$ defined as $\operatorname{mk}$ applied to $\operatorname{toSubsemiring}$ applied to $S$ and the function that maps $x_{3}$ to $\mathrm{Subalgebra\_\_neg\_mem}$ applied to $S$.

Subalgebra.valdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the value of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the value of $S$ is an algebra homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and $A$.

SubalgebraClass.valdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the value of s (from the name)

English

Let $s$ be an element of $S$. Then the value of $s$ is an algebra homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ and $A$.

Submodule.toSubalgebradefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra of p (from the name)

English

Let $p$ be a submodule of $R$ and $A$ such that $1$ is an element of $p$ and for all elements $x_{3}$ of $A$, for all elements $y$ of $A$, if $x_{3}$ is an element of $p$, then if $y$ is an element of $p$, then $x_{3} \times y$ is an element of $p$. Then the subalgebra of $p$ is a subalgebra of $R$ and $A$.

subalgebraOfSubringdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra of S (from the name)

English

Let $S$ be a subring of $R$. Then the subalgebra of $S$ is a subalgebra of $\Integer$ and $R$.

subalgebraOfSubsemiringdefMathlib.Algebra.Algebra.Subalgebra.Basic, function or constant

Wording

the subalgebra of S (from the name)

English

Let $S$ be a subsemiring of $R$. Then the subalgebra of $S$ is a subalgebra of $\Natural$ and $R$.

Mathlib.Algebra.Algebra.Subalgebra.Directed

Subalgebra.iSupLiftdefMathlib.Algebra.Algebra.Subalgebra.Directed, function or constant

Wording

the supremum lift of f and hf (from the name)

English

Let $K$ be a function from elements of $x_{5}$ to subalgebras of $R$ and $A$ such that $\mathrm{Directed}$ holds for the function that maps $x_{9}$ and $x_{10}$ to $\mathrm{Leq} (x_{9} , x_{10})$ and $K$. Let $f$ be a function from elements $i_{1}$ of $x_{5}$ to algebra homomorphisms of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {K (i_{1})}{x_{8}})}$ and $B$ such that for all elements $i$ and $j$ of $x_{5}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (K (i), K (j))$, $f$ applied to $i$ is equal to the composition of $f$ applied to $j$ and the inclusion of $h_{1}$. Let $T$ be a subalgebra of $R$ and $A$ such that $T$ is less than or equal to the supremum of $K$. Then the supremum lift of $i_{1}$ and $\mathrm{hf}$ is an algebra homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {T}{x_{6}})}$ and $B$.

Mathlib.Algebra.Algebra.Subalgebra.Lattice

Algebra.adjoindefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

no wording

English

Let $R$ be a set. Let $s$ be an element of $\wp A$. Then $\operatorname{adjoin}$ applied to $R$ and $s$ is a subalgebra of $R$ and $A$.

Algebra.botEquivdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

the bottom subalgebra of F and R (from the docstring)

English

Let $F$ and $R$ be sets. Then the bottom subalgebra of $F$ and $R$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{3}})}$ and $F$.

Algebra.botEquivOfInjectivedefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

the bottom subalgebra of h (from the docstring)

English

Assume that $\operatorname{coe}$ applied to the algebra map of $R$ and $A$ is injective. Then the bottom subalgebra of $h$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{3}})}$ and $R$.

Algebra.gidefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

no wording

English

$\operatorname{gi}$ is a Galois insertion of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{instSetLike}$.

Algebra.subalgebra_adjoindefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

no wording

English

generation took over the time limit

Algebra.toTopdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

the top (from the name)

English

The top is an algebra homomorphism of $A$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$.

Subalgebra.saturationdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

the saturation of s and M (from the name)

English

Let $s$ be a subalgebra of $R$ and $S$. Let $M$ be a submonoid of $S$ such that $M \leq \operatorname{toSubmonoid} (\operatorname{toSubsemiring} (s))$. Then the saturation of $s$ and $M$ is a subalgebra of $R$ and $S$.

Subalgebra.toNonUnitalSubalgebraOrderEmbeddingdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

the non unital subalgebra order embedding (from the name)

English

The non unital subalgebra order embedding is an order embedding of the set of subalgebras of $R$ and $A$ and the set of non unital subalgebras of $R$ and $A$.

Subalgebra.topEquivdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

the top subalgebra (from the docstring)

English

The top subalgebra is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$ and $A$.

Subring.closureEquivAdjoinIntdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp R$. Then $\operatorname{closureEquivAdjoinInt}$ applied to $s$ is an algebra isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{closure} (s)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\Integer , s)}{x_{2}})}$.

Subsemiring.closureEquivAdjoinNatdefMathlib.Algebra.Algebra.Subalgebra.Lattice, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp R$. Then $\operatorname{closureEquivAdjoinNat}$ applied to $s$ is an algebra isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{closure} (s)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{adjoin} (\Natural , s)}{x_{2}})}$.

Mathlib.Algebra.Algebra.Subalgebra.Matrix

Subalgebra.matrixdefMathlib.Algebra.Algebra.Subalgebra.Matrix, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the matrix of $S$ is a subalgebra of $R$ and the set of matrixes of $n$ and $A$.

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Subalgebra.algEquivOpMopdefMathlib.Algebra.Algebra.Subalgebra.MulOpposite, function or constant

Wording

no wording

English

Let $S$ be a subalgebra of $R$ and $A$. Then $\operatorname{algEquivOpMop}$ applied to $S$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and the set of multiplicative opposites of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{4}})}$.

Subalgebra.linearEquivOpdefMathlib.Algebra.Algebra.Subalgebra.MulOpposite, function or constant

Wording

the linear equivalence opposite of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the linear equivalence opposite of $S$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{4}})}$.

Subalgebra.mopAlgEquivOpdefMathlib.Algebra.Algebra.Subalgebra.MulOpposite, function or constant

Wording

no wording

English

Let $S$ be a subalgebra of $R$ and $A$. Then $\operatorname{mopAlgEquivOp}$ applied to $S$ is an algebra isomorphism of the set of multiplicative opposites of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{4}})}$.

Subalgebra.opdefMathlib.Algebra.Algebra.Subalgebra.MulOpposite, function or constant

Wording

the opposite of S (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Then the opposite of $S$ is a subalgebra of $R$ and the set of multiplicative opposites of $A$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{toSubsemiring}$ applied to $S$ and $\mathrm{Subalgebra\_\_algebraMap\_mem}$ applied to $S$.

Subalgebra.opEquivdefMathlib.Algebra.Algebra.Subalgebra.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

The opposite equivalence is an order isomorphism of the set of subalgebras of $R$ and $A$ and the set of subalgebras of $R$ and the set of multiplicative opposites of $A$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{op}$, $\operatorname{unop}$, $\mathrm{Subalgebra\_\_unop\_op}$ and $\mathrm{Subalgebra\_\_op\_unop}$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Subalgebra\_\_op\_le\_op\_iff}$.

Subalgebra.unopdefMathlib.Algebra.Algebra.Subalgebra.MulOpposite, function or constant

Wording

the opposite of S (from the name)

English

Let $S$ be a subalgebra of $R$ and the set of multiplicative opposites of $A$. Then the opposite of $S$ is a subalgebra of $R$ and $A$.

Mathlib.Algebra.Algebra.Subalgebra.Operations

FixedPoints.subalgebradefMathlib.Algebra.Algebra.Subalgebra.Operations, function or constant

Wording

the subalgebra of G and #3 (from the name)

English

Let $A$, $\mathrm{B'}$ and $G$ be sets. Then the subalgebra of $\mathrm{B'}$ and $G$ is a subalgebra of $A$ and $\mathrm{B'}$.

FixedPoints.subringdefMathlib.Algebra.Algebra.Subalgebra.Operations, function or constant

Wording

the subring of B and G (from the name)

English

Let $B$ and $G$ be sets. Then the subring of $B$ and $G$ is a subring of $B$.

FixedPoints.subsemiringdefMathlib.Algebra.Algebra.Subalgebra.Operations, function or constant

Wording

the subsemiring of G and #2 (from the name)

English

Let $\mathrm{B'}$ and $G$ be sets. Then the subsemiring of $\mathrm{B'}$ and $G$ is a subsemiring of $\mathrm{B'}$.

Mathlib.Algebra.Algebra.Subalgebra.Pi

Subalgebra.pidefMathlib.Algebra.Algebra.Subalgebra.Pi, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be an element of $\wp x$. Let $t$ be a function from elements $i_{1}$ of $x$ to subalgebras of $R$ and $S$ applied to $i_{1}$. Then the product of $s$ and $i_{1}$ is a subalgebra of $R$ and the set of functions from elements $i$ of $x$ to elements of $S$ applied to $i$.

Mathlib.Algebra.Algebra.Subalgebra.Prod

Subalgebra.proddefMathlib.Algebra.Algebra.Subalgebra.Prod, function or constant

Wording

the product of S and x5 (from the name)

English

Let $S$ be a subalgebra of $R$ and $A$. Let $x_{5}$ be a subalgebra of $R$ and $B$. Then the product of $S$ and $x_{5}$ is a subalgebra of $R$ and $\mathrm{Prod}$ applied to $A$ and $B$.

Mathlib.Algebra.Algebra.Subalgebra.Tower

Subalgebra.ofRestrictScalarsdefMathlib.Algebra.Algebra.Subalgebra.Tower, function or constant

Wording

the subalgebra of U and f (from the name)

English

Let $R$ be a set. Let $U$ be a subalgebra of $S$ and $A$. Let $f$ be an algebra homomorphism of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {U}{x_{10}})}$ and $B$. Then the subalgebra of $U$ and $f$ is an algebra homomorphism of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{restrictScalars} (R , U)}{x_{9}})}$ and $B$ defined as $\operatorname{restrictScalars}$ applied to $R$ and $f$.

Subalgebra.restrictScalarsdefMathlib.Algebra.Algebra.Subalgebra.Tower, function or constant

Wording

no wording

English

Let $R$ be a set. Let $U$ be a subalgebra of $S$ and $A$. Then $\operatorname{restrictScalars}$ applied to $R$ and $U$ is a subalgebra of $R$ and $A$.

Mathlib.Algebra.Algebra.Subalgebra.Unitization

NonUnitalStarSubalgebra.unitizationdefMathlib.Algebra.Algebra.Subalgebra.Unitization, function or constant

Wording

the unitization of s (from the name)

English

Let $s$ be an element of $S$. Then the unitization of $s$ is a star algebra homomorphism of the set of unitizations of $R$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and $A$ defined as $\operatorname{starLift}$ applied to the subtype of $s$.

NonUnitalStarSubalgebra.unitizationStarAlgEquivdefMathlib.Algebra.Algebra.Subalgebra.Unitization, function or constant

Wording

the unitization star algebra isomorphism of s and h11 (from the name)

English

Let $s$ be an element of $S$ such that $1$ is not an element of $s$. Then the unitization star algebra isomorphism of $s$ and $h_{11}$ is a star algebra isomorphism of the set of unitizations of $R$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , s)}{x_{7}})}$.

NonUnitalSubalgebra.unitizationdefMathlib.Algebra.Algebra.Subalgebra.Unitization, function or constant

Wording

the unitization of s (from the name)

English

Let $s$ be an element of $S$. Then the unitization of $s$ is an algebra homomorphism of the set of unitizations of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ and $A$ defined as $\operatorname{lift}$ applied to the subtype of $s$.

NonUnitalSubalgebra.unitizationAlgEquivdefMathlib.Algebra.Algebra.Subalgebra.Unitization, function or constant

Wording

the unitization algebra isomorphism of s and h1 (from the name)

English

Let $s$ be an element of $S$ such that $1$ is not an element of $s$. Then the unitization algebra isomorphism of $s$ and $h_{1}$ is an algebra isomorphism of the set of unitizations of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{adjoin} (R , s)}{x_{5}})}$.

NonUnitalSubring.unitizationdefMathlib.Algebra.Algebra.Subalgebra.Unitization, function or constant

Wording

the unitization of s (from the name)

English

Let $s$ be an element of $S$. Then the unitization of $s$ is an algebra homomorphism of the set of unitizations of $\Integer$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $R$ defined as the unitization of $s$.

NonUnitalSubsemiring.unitizationdefMathlib.Algebra.Algebra.Subalgebra.Unitization, function or constant

Wording

the unitization of s (from the name)

English

Let $s$ be an element of $S$. Then the unitization of $s$ is an algebra homomorphism of the set of unitizations of $\Natural$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $R$ defined as the unitization of $s$.

Mathlib.Algebra.Algebra.Tower

AlgEquiv.extendScalarsHomOfSurjectivedefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then $\operatorname{extendScalarsHomOfSurjective}$ applied to $h_{1}$ is a multiplicative equivalence of the set of algebra isomorphisms of $A$ and $A$ and the set of algebra isomorphisms of $A$ and $A$.

AlgEquiv.extendScalarsOfSurjectivedefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then $\operatorname{extendScalarsOfSurjective}$ applied to $h_{2}$ is an equivalence from the set of algebra isomorphisms of $A$ and $B$ to the set of algebra isomorphisms of $A$ and $B$.

AlgEquiv.restrictScalarsdefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be an algebra isomorphism of $A$ and $B$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is an algebra isomorphism of $A$ and $B$.

AlgEquiv.restrictScalarsHomdefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{restrictScalarsHom}$ applied to $R$ is a monoid homomorphism of the set of algebra isomorphisms of $A$ and $A$ and the set of algebra isomorphisms of $A$ and $A$ defined as the algebra automorphism of $R$ and $A$.

AlgHom.extendScalarsHomOfSurjectivedefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then $\operatorname{extendScalarsHomOfSurjective}$ applied to $h_{1}$ is a multiplicative equivalence of the set of algebra homomorphisms of $A$ and $A$ and the set of algebra homomorphisms of $A$ and $A$.

AlgHom.extendScalarsOfSurjectivedefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then $\operatorname{extendScalarsOfSurjective}$ applied to $h_{2}$ is an equivalence from the set of algebra homomorphisms of $A$ and $B$ to the set of algebra homomorphisms of $A$ and $B$.

AlgHom.restrictScalarsdefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be an algebra homomorphism of $A$ and $B$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is an algebra homomorphism of $A$ and $B$.

Algebra.lsmuldefMathlib.Algebra.Algebra.Tower, function or constant

Wording

no wording

English

Let $R$, $B$ and $M$ be sets. Then $\operatorname{lsmul}$ applied to $R$, $B$ and $M$ is an algebra homomorphism of $A$ and the set of ends of $B$ and $M$.

Submodule.orderIsoOfAlgebraMapSurjectivedefMathlib.Algebra.Algebra.Tower, function or constant

Wording

the order isomorphism of h1 (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the algebra map of $R$ and $S$. Then the order isomorphism of $h_{1}$ is an order isomorphism of the set of submodules of $S$ and $M$ and the set of submodules of $R$ and $M$.

Mathlib.Algebra.Algebra.TransferInstance

Equiv.algEquivdefMathlib.Algebra.Algebra.TransferInstance, function or constant

Wording

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

English

Let $R$ be a set. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the algebra isomorphism of $R$ and $e$ is an algebra isomorphism of $x$ and $x_{1}$.

Mathlib.Algebra.Algebra.Unitization

NonUnitalAlgHom.toAlgHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the algebra homomorphism of x5 (from the name)

English

Let $x_{5}$ be a non unital algebra homomorphism of $A$ and $C$. Then the algebra homomorphism of $x_{5}$ is an algebra homomorphism of the set of unitizations of $R$ and $A$ and $C$.

UnitizationstructureMathlib.Algebra.Algebra.Unitization, type

Wording

unitization of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the unitizations of $R$ and $A$ are a basic type.

Unitization.addEquivdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the additive equivalence of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the additive equivalence of $R$ and $A$ is an additive equivalence of the set of unitizations of $R$ and $A$ and $\mathrm{Prod}$ applied to $R$ and $A$.

Unitization.equivdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence from the set of unitizations of $R$ and $A$ to $\mathrm{Prod}$ applied to $R$ and $A$ defined as $\operatorname{mk}$ applied to $\operatorname{toProd}$, $\operatorname{mk}$, $\mathrm{Unitization\_\_mk\_toProd}$ and $\mathrm{Unitization\_\_toProd\_mk}$.

Unitization.fstHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the first component homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the first component homomorphism of $R$ and $A$ is an algebra homomorphism of the set of unitizations of $R$ and $A$ and $R$.

Unitization.inldefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the left injection of r (from the name)

English

Let $r$ be an element of $R$. Then the left injection of $r$ is a unitization of $R$ and $A$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {r}{0}$.

Unitization.inlRingHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the canonical inclusion of rings of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the canonical inclusion of rings of $R$ and $A$ is a ring homomorphism of $R$ and the set of unitizations of $R$ and $A$.

Unitization.inrdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the right injection of a (from the name)

English

Let $a$ be an element of $A$. Then the right injection of $a$ is a unitization of $R$ and $A$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {0}{a}$.

Unitization.inrHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the right injection homomorphism of R and A (from the name)

English

Let $S$, $R$ and $A$ be sets. Then the right injection homomorphism of $R$ and $A$ is a linear map of $A$ and the set of unitizations of $R$ and $A$.

Unitization.inrNonUnitalAlgHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the right injection non unital algebra homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the right injection non unital algebra homomorphism of $R$ and $A$ is a non unital algebra homomorphism of $A$ and the set of unitizations of $R$ and $A$.

Unitization.inrNonUnitalStarAlgHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the right injection non unital star algebra homomorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the right injection non unital star algebra homomorphism of $R$ and $A$ is a non unital star algebra homomorphism of $A$ and the set of unitizations of $R$ and $A$.

Unitization.inrRangeEquivdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the right injection range equivalence of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the right injection range equivalence of $R$ and $A$ is a star algebra isomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{inrNonUnitalStarAlgHom} (R , A))}{x_{5}})}$.

Unitization.liftdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from the set of non unital algebra homomorphisms of $A$ and $C$ to the set of algebra homomorphisms of the set of unitizations of $R$ and $A$ and $C$.

Unitization.linearEquivdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

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

English

Let $S$, $R$ and $A$ be sets. Then the linear equivalence of $R$ and $A$ is a linear equivalence of the set of unitizations of $R$ and $A$ and $\mathrm{Prod}$ applied to $R$ and $A$.

Unitization.sndHomdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the second component homomorphism of R and A (from the name)

English

Let $S$, $R$ and $A$ be sets. Then the second component homomorphism of $R$ and $A$ is a linear map of the set of unitizations of $R$ and $A$ and $A$.

Unitization.starLiftdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the star lift (from the name)

English

The star lift is an equivalence from the set of non unital star algebra homomorphisms of $A$ and $C$ to the set of star algebra homomorphisms of the set of unitizations of $R$ and $A$ and $C$.

Unitization.starMapdefMathlib.Algebra.Algebra.Unitization, function or constant

Wording

the star map of x8 (from the name)

English

Let $x_{8}$ be a non unital star algebra homomorphism of $A$ and $B$. Then the star map of $x_{8}$ is a star algebra homomorphism of the set of unitizations of $R$ and $A$ and the set of unitizations of $R$ and $B$ defined as $\operatorname{starLift}$ applied to the composition of the right injection non unital star algebra homomorphism of $R$ and $B$ and $x_{8}$.

Mathlib.Algebra.Azumaya.Basic

IsAzumaya.tensorEquivEnddefMathlib.Algebra.Azumaya.Basic, function or constant

Wording

the tensor equivalence end of R (from the name)

English

Let $R$ be a set. Then the tensor equivalence end of $R$ is an algebra isomorphism of the set of tensor products of $R$ and the set of multiplicative opposites of $R$ and the set of ends of $R$ and $R$ defined as the composition of $\operatorname{lid}$ applied to $R$ and the set of multiplicative opposites of $R$ and the module end self of $R$.

Mathlib.Algebra.Azumaya.Defs

AlgHom.mulLeftRightdefMathlib.Algebra.Azumaya.Defs, function or constant

Wording

the right multiplicative left of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the right multiplicative left of $R$ and $A$ is an algebra homomorphism of the set of tensor products of $A$ and the set of multiplicative opposites of $A$ and the set of ends of $R$ and $A$ defined as $\operatorname{lsmul}$ applied to $R$, $R$ and $A$.

IsAzumayaclassMathlib.Algebra.Azumaya.Defs, predicate

Wording

no wording

English

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

Mathlib.Algebra.Azumaya.Matrix

AlgHom.mulLeftRightMatrix_invdefMathlib.Algebra.Azumaya.Matrix, function or constant

Wording

the multiplicative left right matrix inverse of R and n (from the name)

English

Let $R$ and $n$ be sets. Then the multiplicative left right matrix inverse of $R$ and $n$ is a linear map of the set of ends of $R$ and the set of matrixes of $n$ and $R$ and the set of tensor products of the set of matrixes of $n$ and $R$ and the set of multiplicative opposites of the set of matrixes of $n$ and $R$.

Mathlib.Algebra.BigOperators.Balance

Fintype.balancedefMathlib.Algebra.BigOperators.Balance, function or constant

Wording

the balancing of f and x4 (from the docstring)

English

Let $f$ be a function from elements of $x$ to elements of $G$. Let $x_{4}$ be an element of $x$. Then the balancing of $f$ and $x_{4}$ is an element of $G$ defined as $\mathrm{minus} (f , \operatorname{const} (x , \operatorname{expect} (\FinsetunivMACRoAC , \lambda y . f (y))), x_{4})$.

Mathlib.Algebra.BigOperators.Expect

BigOperators.bigexpectdefMathlib.Algebra.BigOperators.Expect, function or constant

Wording

no wording

English

generation took over the time limit

Finset.expectdefMathlib.Algebra.BigOperators.Expect, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{expect}$ applied to $s$ and $f$ is an element of $M$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (\FinsetcardMACRoM {s})}{(\FinsetSum {s}{i}{f (i)})}$.

Mathlib.Algebra.BigOperators.Fin

Fin.partialProddefMathlib.Algebra.BigOperators.Fin, function or constant

Wording

the partial product of f and i (from the name)

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $M$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the partial product of $f$ and $i$ is an element of $M$ defined as $\operatorname{prod}$ applied to $\operatorname{take}$ applied to $\operatorname{val}$ applied to $i$ and $\operatorname{ofFn}$ applied to $f$.

Fin.partialSumdefMathlib.Algebra.BigOperators.Fin, function or constant

Wording

the partial sum of f and i (from the name)

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $M$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the partial sum of $f$ and $i$ is an element of $M$ defined as $\operatorname{sum}$ applied to $\operatorname{take}$ applied to $\operatorname{val}$ applied to $i$ and $\operatorname{ofFn}$ applied to $f$.

finFunctionFinEquivdefMathlib.Algebra.BigOperators.Fin, function or constant

Wording

the finite function finite equivalence (from the name)

English

The finite function finite equivalence is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Fin} (n))\rightarrow \mathrm{Fin} (m))}{\mathrm{Fin} (m ^ {n})}$.

finPiFinEquivdefMathlib.Algebra.BigOperators.Fin, function or constant

Wording

the finite product finite equivalence (from the name)

English

The finite product finite equivalence is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Fin} (m))\rightarrow \mathrm{Fin} (n (i)))}{\mathrm{Fin} (\FinsetProd {\FinsetunivMACRoAC}{i_{1}}{n (i_{1})})}$.

finSigmaFinEquivdefMathlib.Algebra.BigOperators.Fin, function or constant

Wording

the finite sigma finite equivalence (from the name)

English

The finite sigma finite equivalence is an element of $\EquivMACRoAE {\Sigma (\lambda i . \mathrm{Fin} (n (i)))}{\mathrm{Fin} (\FinsetSum {\FinsetunivMACRoAC}{i_{1}}{n (i_{1})})}$ defined as $\operatorname{brecOn}$ applied to $m$, $\mathrm{finSigmaFinEquiv\_\_\_f}$ and $n$.

Mathlib.Algebra.BigOperators.Finprod

finproddefMathlib.Algebra.BigOperators.Finprod, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $M$. Then $\mathrm{finprod}$ applied to $f$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_BigOperators\_\_Finprod\_\_787831954\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $f$.

finsumdefMathlib.Algebra.BigOperators.Finprod, function or constant

Wording

the finite sum of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $M$. Then the finite sum of $f$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_BigOperators\_\_Finprod\_\_2417567597\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $f$.

Mathlib.Algebra.BigOperators.Finsupp.Basic

Finsupp.liftAddHomdefMathlib.Algebra.BigOperators.Finsupp.Basic, function or constant

Wording

the lift additive homomorphism (from the name)

English

The lift additive homomorphism is an additive equivalence of the set of functions from elements of $x$ to additive monoid homomorphisms of $M$ and $N$ and the set of additive monoid homomorphisms of $\FinsuppMACRoQ {x}{M}$ and $N$.

Finsupp.proddefMathlib.Algebra.BigOperators.Finsupp.Basic, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Let $g$ be a function from elements of $x$ and elements of $M$ to elements of $N$. Then $\FinsuppProd {f}{g}$ is an element of $N$ defined as $\FinsetProd {\FinsuppsupportMACRoR {f}}{a}{g (a , f (a))}$.

Finsupp.sumdefMathlib.Algebra.BigOperators.Finsupp.Basic, function or constant

Wording

the sum of f and g (from the name)

English

Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Let $g$ be a function from elements of $x$ and elements of $M$ to elements of $N$. Then the sum of $f$ and $g$ is an element of $N$ defined as $\FinsetSum {\FinsuppsupportMACRoR {f}}{a}{g (a , f (a))}$.

Mathlib.Algebra.BigOperators.Finsupp.Fin

finTwoArrowEquiv'defMathlib.Algebra.BigOperators.Finsupp.Fin, function or constant

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{finTwoArrowEquiv'}$ applied to $M$ is an element of $\EquivMACRoAE {(\FinsuppMACRoQ {\mathrm{Fin} (2)}{M})}{\mathrm{Prod} (M , M)}$ defined as the composition of $\operatorname{equivFunOnFinite}$ and $\mathrm{finTwoArrowEquiv}$ applied to $M$.

Mathlib.Algebra.BigOperators.Group.Finset.Defs

BigOperators.BigOpWithdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.bigOpBinderdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.bigOpBinderCollectiondefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.bigOpBinderParenthesizeddefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.bigOpBindersdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.bigOpBindersPatterndefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

Let $\mathrm{processed}$ be an element of $\mathrm{Array}$ applied to $\mathrm{Prod}$ applied to $\operatorname{Term}$ and $\operatorname{Term}$. Then $\operatorname{MacroM}$ holds for $\operatorname{Term}$.

BigOperators.bigOpBindersProddefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

BigOperators.bigproddefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.bigsumdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.processBigOpBinderdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

BigOperators.processBigOpBindersdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

generation took over the time limit

Finset.proddefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

the product of s and f (from the name)

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $M$. Then $\FinsetProd {s}{f}$ is an element of $M$ defined as the product of the map of $f$ and the value of $s$.

Finset.sumdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

the sum of s and f (from the name)

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $M$. Then $\FinsetSum {s}{f}$ is an element of $M$ defined as the sum of the map of $f$ and the value of $s$.

LibraryNote.operator_precedence_of_big_operatorsdefMathlib.Algebra.BigOperators.Group.Finset.Defs, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_operator\_precedence\_of\_big\_operators}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Mathlib.Algebra.BigOperators.Group.List.Defs

List.alternatingProddefMathlib.Algebra.BigOperators.Group.List.Defs, function or constant

Wording

the alternating product of x3 (from the docstring)

English

Let $x_{3}$ be a list of elements of $G$. Then the alternating product of $x_{3}$ is an element of $G$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{List\_\_alternatingProd\_\_\_f}$.

List.alternatingSumdefMathlib.Algebra.BigOperators.Group.List.Defs, function or constant

Wording

the alternating sum of x3 (from the docstring)

English

Let $x_{3}$ be a list of elements of $G$. Then the alternating sum of $x_{3}$ is an element of $G$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{List\_\_alternatingSum\_\_\_f}$.

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Multiset.sumAddMonoidHomdefMathlib.Algebra.BigOperators.Group.Multiset.Basic, function or constant

Wording

the sum additive monoid homomorphism (from the name)

English

The sum additive monoid homomorphism is an additive monoid homomorphism of the set of multisets of $M$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{sum}$ and $\mathrm{Multiset\_\_sum\_zero}$ and $\mathrm{Multiset\_\_sum\_add}$.

Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Multiset.proddefMathlib.Algebra.BigOperators.Group.Multiset.Defs, function or constant

Wording

the product of x1 (from the name)

English

Let $x_{1}$ be a multiset of $M$. Then the product of $x_{1}$ is an element of $M$ defined as $\operatorname{foldr}$ applied to the function that maps $x_{1}$ and $x_{2}$ to $x_{1} \times x_{2}$, $1$ and $x_{1}$.

Multiset.sumdefMathlib.Algebra.BigOperators.Group.Multiset.Defs, function or constant

Wording

the sum of x1 (from the name)

English

Let $x_{1}$ be a multiset of $M$. Then the sum of $x_{1}$ is an element of $M$ defined as $\operatorname{foldr}$ applied to the function that maps $x_{1}$ and $x_{2}$ to $x_{1} + x_{2}$, $0$ and $x_{1}$.

Mathlib.Algebra.BigOperators.Pi

Pi.addMonoidHomAddEquivdefMathlib.Algebra.BigOperators.Pi, function or constant

Wording

the additive monoid homomorphism additive equivalence of M and i (from the name)

English

Let $M$ be a function from elements of $x$ to sets. Let $\mathrm{M'}$ be a set. Then the additive monoid homomorphism additive equivalence of $M$ and $\mathrm{M'}$ is an additive equivalence of the set of additive monoid homomorphisms of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and $\mathrm{M'}$ and the set of functions from elements $i_{1}$ of $x$ to additive monoid homomorphisms of $M$ applied to $i_{1}$ and $\mathrm{M'}$.

Pi.monoidHomMulEquivdefMathlib.Algebra.BigOperators.Pi, function or constant

Wording

the monoid homomorphism multiplicative equivalence of M and i (from the name)

English

Let $M$ be a function from elements of $x$ to sets. Let $\mathrm{M'}$ be a set. Then the monoid homomorphism multiplicative equivalence of $M$ and $\mathrm{M'}$ is a multiplicative equivalence of the set of monoid homomorphisms of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and $\mathrm{M'}$ and the set of functions from elements $i_{1}$ of $x$ to monoid homomorphisms of $M$ applied to $i_{1}$ and $\mathrm{M'}$.

Mathlib.Algebra.BrauerGroup.Defs

BrauerGroupdefMathlib.Algebra.BrauerGroup.Defs, type

Wording

Brauer group of K (from the name)

English

Let $K$ be a set. Then a Brauer group of $K$ is an element of the function that maps $K$ to $\mathrm{Quotient}$ applied to $\mathrm{Brauer\_\_CSA\_Setoid}$ applied to $K$.

CSAstructureMathlib.Algebra.BrauerGroup.Defs, type

Wording

no wording

English

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

IsBrauerEquivalentdefMathlib.Algebra.BrauerGroup.Defs, predicate

Wording

A is a Brauer equivalent with respect to B (from the name)

English

Let $A$ and $B$ be elements of $\mathrm{CSA}$ applied to $K$. Then $A$ is a Brauer equivalent with respect to $B$, if there exist natural numbers $n$ and $m$, such that $n \neq 0$, $m \neq 0$ and $\mathrm{Nonempty}$ holds for the set of algebra isomorphisms of the set of matrixes of $\mathrm{Fin}$ applied to $n$ and the set of carriers of $\operatorname{toAlgCat}$ applied to $A$ and the set of matrixes of $\mathrm{Fin}$ applied to $m$ and the set of carriers of $\operatorname{toAlgCat}$ applied to $B$.

Mathlib.Algebra.Category.AlgCat.Basic

AlgCatstructureMathlib.Algebra.Category.AlgCat.Basic, type

Wording

algebra category of R (from the name)

English

Let $R$ be a set. Then the algebra categories of $R$ are a basic type.

AlgCat.HomstructureMathlib.Algebra.Category.AlgCat.Basic, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be algebra categories of $R$. Then the homomorphisms of $A$ and $B$ are a basic type.

AlgCat.Hom.homdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Then the homomorphism of $f$ is an algebra homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as the homomorphism of $f$.

AlgCat.Hom.hom'defMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is an algebra homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgCat.adjdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the adjoint of R (from the name)

English

Let $R$ be a set. Then the adjoint of $R$ is an adjunction of the free of $R$ and the forgetful functor of the set of algebra categories of $R$.

AlgCat.carrierdefMathlib.Algebra.Category.AlgCat.Basic, type

Wording

carrier of self (from the name)

English

Let $\mathrm{self}$ be an algebra category of $R$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

AlgCat.freedefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the free of R (from the name)

English

Let $R$ be a set. Then the free of $R$ is a functor of the set of sets and the set of algebra categories of $R$.

AlgCat.intEquivalencedefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the integer equivalence (from the name)

English

The integer equivalence is an equivalence of the set of algebra categories of $\Integer$ and the set of categories of rings.

AlgCat.ofdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

no wording

English

Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is an algebra category of $R$ defined as $\mathrm{AlgCat\_\_\_mkInternal}$ applied to $X$.

AlgCat.ofHomdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the algebra category of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the algebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $A$ and $\operatorname{of}$ applied to $R$ and $B$ defined as the concrete category of $f$.

AlgCat.restrictScalarsdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{restrictScalars}$ applied to $f$ is a functor of the set of algebra categories of $S$ and the set of algebra categories of $R$.

AlgCat.restrictScalarsComp'defMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a ring homomorphism of $S$ and $T$. Let $\mathrm{gf}$ be a ring homomorphism of $R$ and $T$ such that $\mathrm{gf}$ is equal to the composition of $g$ and $f$. Then $\operatorname{restrictScalarsComp'}$ applied to $f$, $g$, $\mathrm{gf}$ and $\mathrm{hfg}$ is an isomorphism of $\operatorname{restrictScalars}$ applied to $\mathrm{gf}$ and the composition of $\operatorname{restrictScalars}$ applied to $g$ and $\operatorname{restrictScalars}$ applied to $f$.

AlgCat.restrictScalarsEquivalenceOfRingEquivdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

no wording

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then $\operatorname{restrictScalarsEquivalenceOfRingEquiv}$ applied to $e$ is an equivalence of the set of algebra categories of $S$ and the set of algebra categories of $R$.

AlgCat.restrictScalarsId'defMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $R$ such that $f$ is equal to the identity ring homomorphism of $R$. Then $\operatorname{restrictScalarsId'}$ applied to $f$ and $\mathrm{hf}$ is an isomorphism of $\operatorname{restrictScalars}$ applied to $f$ and the identity of the set of algebra categories of $R$.

AlgEquiv.toAlgebraIsodefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the algebra isomorphism of e (from the name)

English

Let $e$ be an algebra isomorphism of $x_{1}$ and $x_{2}$. Then the algebra isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $x_{1}$ and $\operatorname{of}$ applied to $R$ and $x_{2}$.

CategoryTheory.Iso.toAlgEquivdefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the algebra isomorphism of i (from the name)

English

Let $i$ be an isomorphism of $X$ and $Y$. Then the algebra isomorphism of $i$ is an algebra isomorphism of the set of carriers of $X$ and the set of carriers of $Y$.

algEquivIsoAlgebraIsodefMathlib.Algebra.Category.AlgCat.Basic, function or constant

Wording

the algebra isomorphism isomorphism algebra isomorphism (from the name)

English

The algebra isomorphism isomorphism algebra isomorphism is an isomorphism of the set of algebra isomorphisms of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.

Mathlib.Algebra.Category.AlgCat.Limits

AlgCat.HasLimits.limitConedefMathlib.Algebra.Category.AlgCat.Limits, function or constant

Wording

the limit cone of F (from the name)

English

Let $F$ be a functor of $J$ and the set of algebra categories of $R$. Then the limit cone of $F$ is a cone of $F$.

AlgCat.HasLimits.limitConeIsLimitdefMathlib.Algebra.Category.AlgCat.Limits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of algebra categories of $R$. Then $\operatorname{limitConeIsLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.

AlgCat.limitπAlgHomdefMathlib.Algebra.Category.AlgCat.Limits, function or constant

Wording

the limit projection algebra homomorphism of F and j (from the name)

English

Let $F$ be a functor of $J$ and the set of algebra categories of $R$. Let $j$ be an element of $J$. Then the limit projection algebra homomorphism of $F$ and $j$ is an algebra homomorphism of $\operatorname{pt}$ applied to the limit cone of the composition of $F$ and the forgetful functor of the set of algebra categories of $R$ and the action of the composition of $F$ and the forgetful functor of the set of algebra categories of $R$ and $j$.

AlgCat.sectionsSubalgebradefMathlib.Algebra.Category.AlgCat.Limits, function or constant

Wording

the section subalgebra of F (from the name)

English

Let $F$ be a functor of $J$ and the set of algebra categories of $R$. Then the section subalgebra of $F$ is a subalgebra of $R$ and the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.

Mathlib.Algebra.Category.AlgCat.TensorAlgebra

AlgCat.tensorAlgebradefMathlib.Algebra.Category.AlgCat.TensorAlgebra, function or constant

Wording

the tensor algebra of R (from the name)

English

Let $R$ be a set. Then the tensor algebra of $R$ is a functor of the set of module categories of $R$ and the set of algebra categories of $R$.

AlgCat.tensorAlgebraAdjdefMathlib.Algebra.Category.AlgCat.TensorAlgebra, function or constant

Wording

the tensor algebra adjoint of R (from the name)

English

Let $R$ be a set. Then the tensor algebra adjoint of $R$ is an adjunction of the tensor algebra of $R$ and the forgetful functor of the set of algebra categories of $R$ and the set of module categories of $R$.

Mathlib.Algebra.Category.BialgCat.Basic

BialgCatstructureMathlib.Algebra.Category.BialgCat.Basic, type

Wording

bialgebra category of R (from the name)

English

Let $R$ be a set. Then the bialgebra categories of $R$ are a basic type.

BialgCat.HomstructureMathlib.Algebra.Category.BialgCat.Basic, type

Wording

homomorphism of V and W (from the name)

English

Let $V$ and $W$ be bialgebra categories of $R$. Then the homomorphisms of $V$ and $W$ are a basic type.

BialgCat.Hom.toBialgHomdefMathlib.Algebra.Category.BialgCat.Basic, function or constant

Wording

the bialgebra homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the bialgebra homomorphism of $f$ is a bialgebra homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.

BialgCat.Hom.toBialgHom'defMathlib.Algebra.Category.BialgCat.Basic, function or constant

Wording

the bialgebra homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $V$ and $W$. Then the bialgebra homomorphism of $\mathrm{self}$ is a bialgebra homomorphism of the set of carriers of $V$ and the set of carriers of $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

BialgCat.carrierdefMathlib.Algebra.Category.BialgCat.Basic, type

Wording

carrier of self (from the name)

English

Let $\mathrm{self}$ be a bialgebra category of $R$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

BialgCat.ofdefMathlib.Algebra.Category.BialgCat.Basic, function or constant

Wording

no wording

English

Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a bialgebra category of $R$ defined as $\operatorname{mk}$ applied to $X$.

BialgCat.ofHomdefMathlib.Algebra.Category.BialgCat.Basic, function or constant

Wording

the bialgebra category of f (from the name)

English

Let $f$ be a bialgebra homomorphism of $X$ and $Y$. Then the bialgebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.

BialgEquiv.toBialgIsodefMathlib.Algebra.Category.BialgCat.Basic, function or constant

Wording

the bialgebra isomorphism of e (from the name)

English

Let $e$ be a bialgebra equivalence of $X$ and $Y$. Then the bialgebra isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.

CategoryTheory.Iso.toBialgEquivdefMathlib.Algebra.Category.BialgCat.Basic, function or constant

Wording

the bialgebra equivalence of i (from the name)

English

Let $i$ be an isomorphism of $X$ and $Y$. Then the bialgebra equivalence of $i$ is a bialgebra equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

Mathlib.Algebra.Category.BialgCat.Monoidal

BialgCat.MonoidalCategory.inducingFunctorDatadefMathlib.Algebra.Category.BialgCat.Monoidal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{inducingFunctorData}$ applied to $R$ is an element of $\operatorname{InducingFunctorData}$ applied to the forgetful functor of the set of bialgebra categories of $R$ and the set of algebra categories of $R$.

Mathlib.Algebra.Category.BoolRing

BoolRingstructureMathlib.Algebra.Category.BoolRing, type

Wording

bool ring (from the name)

English

The bool rings are a basic type.

BoolRing.HomstructureMathlib.Algebra.Category.BoolRing, type

Wording

homomorphism of R and S (from the name)

English

Let $R$ and $S$ be bool rings. Then the homomorphisms of $R$ and $S$ are a basic type.

BoolRing.Hom.homdefMathlib.Algebra.Category.BoolRing, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a ring homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.

BoolRing.Hom.hom'defMathlib.Algebra.Category.BoolRing, function or constant

Wording

the underlying ring hom of self (from the docstring)

English

Let $\mathrm{self}$ be a homomorphism of $R$ and $S$. Then the underlying ring hom of $\mathrm{self}$ is a ring homomorphism of the set of carriers of $R$ and the set of carriers of $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

BoolRing.Iso.mkdefMathlib.Algebra.Category.BoolRing, function or constant

Wording

no wording

English

Let $e$ be a ring isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.

BoolRing.carrierdefMathlib.Algebra.Category.BoolRing, type

Wording

carrier of self (from the name)

English

Let $\mathrm{self}$ be a bool ring. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

BoolRing.ofHomdefMathlib.Algebra.Category.BoolRing, function or constant

Wording

the bool ring of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the bool ring of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $\operatorname{of}$ applied to $S$ defined as the concrete category of $f$.

boolRingCatEquivBoolAlgdefMathlib.Algebra.Category.BoolRing, function or constant

Wording

the bool ring category equivalence bool algebra (from the name)

English

The bool ring category equivalence bool algebra is an equivalence of the set of bool rings and the set of bool algebras.

Mathlib.Algebra.Category.CoalgCat.Basic

CategoryTheory.Iso.toCoalgEquivdefMathlib.Algebra.Category.CoalgCat.Basic, function or constant

Wording

the coalgebra equivalence of i (from the name)

English

Let $i$ be an isomorphism of $X$ and $Y$. Then the coalgebra equivalence of $i$ is a coalgebra equivalence of the set of carriers of $\operatorname{toModuleCat}$ applied to $X$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $Y$.

CoalgCatstructureMathlib.Algebra.Category.CoalgCat.Basic, type

Wording

coalgebra category of R (from the name)

English

Let $R$ be a set. Then the coalgebra categories of $R$ are a basic type.

CoalgCat.HomstructureMathlib.Algebra.Category.CoalgCat.Basic, type

Wording

homomorphism of V and W (from the name)

English

Let $V$ and $W$ be coalgebra categories of $R$. Then the homomorphisms of $V$ and $W$ are a basic type.

CoalgCat.Hom.toCoalgHomdefMathlib.Algebra.Category.CoalgCat.Basic, function or constant

Wording

the coalgebra homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the coalgebra homomorphism of $f$ is a coalgebra homomorphism of the set of carriers of $\operatorname{toModuleCat}$ applied to $X$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $Y$ defined as the homomorphism of $f$.

CoalgCat.Hom.toCoalgHom'defMathlib.Algebra.Category.CoalgCat.Basic, function or constant

Wording

the coalgebra homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $V$ and $W$. Then the coalgebra homomorphism of $\mathrm{self}$ is a coalgebra homomorphism of the set of carriers of $\operatorname{toModuleCat}$ applied to $V$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CoalgCat.ofdefMathlib.Algebra.Category.CoalgCat.Basic, function or constant

Wording

no wording

English

Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a coalgebra category of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and $X$ and $\mathrm{inferInstance}$.

CoalgCat.ofHomdefMathlib.Algebra.Category.CoalgCat.Basic, function or constant

Wording

the coalgebra category of f (from the name)

English

Let $f$ be a coalgebra homomorphism of $X$ and $Y$. Then the coalgebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.

CoalgEquiv.toCoalgIsodefMathlib.Algebra.Category.CoalgCat.Basic, function or constant

Wording

the coalgebra isomorphism of e (from the name)

English

Let $e$ be a coalgebra equivalence of $X$ and $Y$. Then the coalgebra isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.

Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

CoalgCat.comonEquivalencedefMathlib.Algebra.Category.CoalgCat.ComonEquivalence, function or constant

Wording

the comonoid equivalence of R (from the name)

English

Let $R$ be a set. Then the comonoid equivalence of $R$ is an equivalence of the set of coalgebra categories of $R$ and $\operatorname{Comon}$ applied to the set of module categories of $R$.

CoalgCat.ofComondefMathlib.Algebra.Category.CoalgCat.ComonEquivalence, function or constant

Wording

the coalgebra category of R (from the name)

English

Let $R$ be a set. Then the coalgebra category of $R$ is a functor of $\operatorname{Comon}$ applied to the set of module categories of $R$ and the set of coalgebra categories of $R$.

CoalgCat.ofComonObjdefMathlib.Algebra.Category.CoalgCat.ComonEquivalence, function or constant

Wording

the coalgebra category of X (from the name)

English

Let $X$ be a module category of $R$. Then the coalgebra category of $X$ is a coalgebra category of $R$.

CoalgCat.toComondefMathlib.Algebra.Category.CoalgCat.ComonEquivalence, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{toComon}$ applied to $R$ is a functor of the set of coalgebra categories of $R$ and $\operatorname{Comon}$ applied to the set of module categories of $R$.

CoalgCat.toComonObjdefMathlib.Algebra.Category.CoalgCat.ComonEquivalence, function or constant

Wording

the comonoid object of X (from the name)

English

Let $X$ be a coalgebra category of $R$. Then the comonoid object of $X$ is an element of $\operatorname{Comon}$ applied to the set of module categories of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and the set of carriers of $\operatorname{toModuleCat}$ applied to $X$.

Mathlib.Algebra.Category.CoalgCat.Monoidal

CoalgCat.MonoidalCategory.inducingFunctorDatadefMathlib.Algebra.Category.CoalgCat.Monoidal, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{inducingFunctorData}$ applied to $R$ is an element of $\operatorname{InducingFunctorData}$ applied to the forgetful functor of the set of coalgebra categories of $R$ and the set of module categories of $R$.

Mathlib.Algebra.Category.CommAlgCat.Basic

CommAlgCatstructureMathlib.Algebra.Category.CommAlgCat.Basic, type

Wording

commutative algebra category of R (from the name)

English

Let $R$ be a set. Then the commutative algebra categories of $R$ are a basic type.

CommAlgCat.HomstructureMathlib.Algebra.Category.CommAlgCat.Basic, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be commutative algebra categories of $R$. Then the homomorphisms of $A$ and $B$ are a basic type.

CommAlgCat.Hom.homdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Then the homomorphism of $f$ is an algebra homomorphism of the set of carriers of $A$ and the set of carriers of $B$ defined as the homomorphism of $f$.

CommAlgCat.Hom.hom'defMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the homomorphism of self (from the name)

English

CommAlgCat.algEquivOfIsodefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the algebra isomorphism of i (from the name)

English

Let $i$ be an isomorphism of $A$ and $B$. Then the algebra isomorphism of $i$ is an algebra isomorphism of the set of carriers of $A$ and the set of carriers of $B$.

CommAlgCat.carrierdefMathlib.Algebra.Category.CommAlgCat.Basic, type

Wording

carrier of self (from the name)

English

Let $\mathrm{self}$ be a commutative algebra category of $R$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

CommAlgCat.fullyFaithfulUliftFunctordefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the fully faithful lift functor of R (from the name)

English

generation took over the time limit

CommAlgCat.homEquivCommRingCatdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the homomorphism equivalence commutative ring category of A and B (from the name)

English

Let $A$ and $B$ be commutative algebra categories of $R$. Then the homomorphism equivalence commutative ring category of $A$ and $B$ is an element of $\EquivMACRoAE {\operatorname{Hom} (A , B)}{(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (\operatorname{hom} (f), \operatorname{algebraMap} (R , \operatorname{carrier} (A)))}{\operatorname{algebraMap} (R , \operatorname{carrier} (B))})})}$.

CommAlgCat.isoEquivAlgEquivdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the isomorphism equivalence algebra isomorphism (from the name)

English

The isomorphism equivalence algebra isomorphism is an equivalence from the set of isomorphisms of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ to the set of algebra isomorphisms of $X$ and $Y$.

CommAlgCat.isoMkdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the isomorphism of e (from the name)

English

Let $e$ be an algebra isomorphism of $X$ and $Y$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$.

CommAlgCat.ofdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

no wording

English

Let $R$ and $X$ be sets. Then $\operatorname{of}$ applied to $R$ and $X$ is a commutative algebra category of $R$ defined as $\mathrm{CommAlgCat\_\_\_mkInternal}$ applied to $X$.

CommAlgCat.ofHomdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the commutative algebra category of f (from the name)

English

Let $f$ be an algebra homomorphism of $X$ and $Y$. Then the commutative algebra category of $f$ is a homomorphism of $\operatorname{of}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $Y$ defined as the concrete category of $f$.

CommAlgCat.uliftFunctordefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

the lift functor of R (from the name)

English

Let $R$ be a set. Then the lift functor of $R$ is a functor of the set of commutative algebra categories of $R$ and the set of commutative algebra categories of $R$.

commAlgCatEquivUnderdefMathlib.Algebra.Category.CommAlgCat.Basic, function or constant

Wording

no wording

English

Let $R$ be a category of commutative rings. Then $\mathrm{commAlgCatEquivUnder}$ applied to $R$ is an equivalence of the set of commutative algebra categories of the set of carriers of $R$ and $\operatorname{Under}$ applied to $R$.