Definitions: Mathlib.Algebra, part 17 of 17

280 definitions of 32 modules, Mathlib.Algebra.RingQuot to Mathlib.Algebra.WithConv. ‹ previous next ›

Mathlib.Algebra.RingQuot

RingQuotstructureMathlib.Algebra.RingQuot, type
Wording
ring quotient of r (from the name)
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Then the ring quotients of $r$ are a basic type.
RingQuot.RelinductiveMathlib.Algebra.RingQuot, predicate
Wording
no wording
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $R$. Then we can say that $\operatorname{Rel}$ holds for $r$, $x_{1}$ and $x_{2}$.
RingQuot.Rel.belowinductiveMathlib.Algebra.RingQuot, predicate
Wording
no wording
English
Assume that $\operatorname{Rel}$ holds for $r$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
RingQuot.algEquivQuotAlgEquivdefMathlib.Algebra.RingQuot, function or constant
Wording
the algebra isomorphism quotient algebra isomorphism of f and rel (from the name)
English
Let $f$ be an algebra isomorphism of $A$ and $B$. Let $\mathrm{rel}$ be a function from elements of $A$ and elements of $A$ to propositions. Then the algebra isomorphism quotient algebra isomorphism of $f$ and $\mathrm{rel}$ is an algebra isomorphism of the set of ring quotients of $\mathrm{rel}$ and the set of ring quotients of $\operatorname{onFun}$ applied to $\mathrm{rel}$ and $\operatorname{coe}$ applied to the inverse of $f$.
RingQuot.equivQuotEquivdefMathlib.Algebra.RingQuot, function or constant
Wording
the equivalence quotient equivalence of f and rel (from the name)
English
Let $f$ be a ring isomorphism of $A$ and $B$. Let $\mathrm{rel}$ be a function from elements of $A$ and elements of $A$ to propositions. Then the equivalence quotient equivalence of $f$ and $\mathrm{rel}$ is a ring isomorphism of the set of ring quotients of $\mathrm{rel}$ and the set of ring quotients of $\operatorname{onFun}$ applied to $\mathrm{rel}$ and $\operatorname{coe}$ applied to the inverse of $f$.
RingQuot.idealQuotientToRingQuotdefMathlib.Algebra.RingQuot, function or constant
Wording
the ideal quotient to ring quotient of r (from the name)
English
Let $r$ be a function from elements of $B$ and elements of $B$ to propositions. Then the ideal quotient to ring quotient of $r$ is a ring homomorphism of the set of quotients of $B$ and the ideal generated by an arbitrary binary relation of $r$ and the set of ring quotients of $r$.
RingQuot.intCastdefMathlib.Algebra.RingQuot, function or constant
Wording
the integer cast of r and z (from the name)
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Let $z$ be an integer. Then the integer cast of $r$ and $z$ is a ring quotient of $r$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $r$ and $z$.
RingQuot.liftdefMathlib.Algebra.RingQuot, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (R , \lambda x_{2} . \mathrm{forall} (R , \lambda y . \mathrm{if} (r (x_{2} , y), \EqtMACRoH {f (x_{2})}{f (y)})))}$ to the set of ring homomorphisms of the set of ring quotients of $r$ and $T$ defined as $\operatorname{proj0}$ applied to $\mathrm{RingQuot\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_RingQuot\_\_1074400100\_\_\_hygCtx\_\_\_hyg\_\_2}$.
RingQuot.liftAlgHomdefMathlib.Algebra.RingQuot, function or constant
Wording
the lift algebra homomorphism of S (from the name)
English
Let $S$ be a set. Then the lift algebra homomorphism of $S$ is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (A , \lambda x_{5} . \mathrm{forall} (A , \lambda y . \mathrm{if} (s (x_{5} , y), \EqtMACRoH {f (x_{5})}{f (y)})))}$ to the set of algebra homomorphisms of the set of ring quotients of $s$ and $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{RingQuot\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_RingQuot\_\_1624853203\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $S$.
RingQuot.mkAlgHomdefMathlib.Algebra.RingQuot, function or constant
Wording
the algebra homomorphism of S and s (from the name)
English
Let $S$ be a set. Let $s$ be a function from elements of $A$ and elements of $A$ to propositions. Then the algebra homomorphism of $S$ and $s$ is an algebra homomorphism of $A$ and the set of ring quotients of $s$ defined as $\operatorname{proj0}$ applied to $\mathrm{RingQuot\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_RingQuot\_\_3673095128\_\_\_hygCtx\_\_\_hyg\_\_2}$, $S$ and $s$.
RingQuot.mkRingHomdefMathlib.Algebra.RingQuot, function or constant
Wording
the ring homomorphism of r (from the name)
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Then the ring homomorphism of $r$ is a ring homomorphism of $R$ and the set of ring quotients of $r$ defined as $\operatorname{proj0}$ applied to $\mathrm{RingQuot\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_RingQuot\_\_3469094938\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $r$.
RingQuot.natCastdefMathlib.Algebra.RingQuot, function or constant
Wording
the natural cast of r and n (from the name)
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Let $n$ be a natural number. Then the natural cast of $r$ and $n$ is a ring quotient of $r$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $r$ and $n$.
RingQuot.preLiftdefMathlib.Algebra.RingQuot, function or constant
Wording
the lift of h (from the name)
English
Assume that for all elements $x_{2}$ and $y$ of $R$, if $r$ holds for $x_{2}$ and $y$, then $\EqtMACRoH {f (x_{2})}{f (y)}$. Then the lift of $h$ is a ring homomorphism of the set of ring quotients of $r$ and $T$ defined as $\operatorname{proj0}$ applied to $\mathrm{RingQuot\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_RingQuot\_\_1093876312\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $h$.
RingQuot.preLiftAlgHomdefMathlib.Algebra.RingQuot, function or constant
Wording
the lift algebra homomorphism of S and h (from the name)
English
Let $S$ be a set. Assume that for all elements $x_{5}$ and $y$ of $A$, if $s$ holds for $x_{5}$ and $y$, then $\EqtMACRoH {f (x_{5})}{f (y)}$. Then the lift algebra homomorphism of $S$ and $h$ is an algebra homomorphism of the set of ring quotients of $s$ and $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{RingQuot\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_RingQuot\_\_1554258878\_\_\_hygCtx\_\_\_hyg\_\_2}$, $S$ and $h$.
RingQuot.ringCondefMathlib.Algebra.RingQuot, function or constant
Wording
the ring congruence of r (from the docstring)
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Then the ring congruence of $r$ is a ring congruence relation of $R$.
RingQuot.ringQuotEquivIdealQuotientdefMathlib.Algebra.RingQuot, function or constant
Wording
the ring quotient equivalence ideal quotient of r (from the name)
English
Let $r$ be a function from elements of $B$ and elements of $B$ to propositions. Then the ring quotient equivalence ideal quotient of $r$ is a ring isomorphism of the set of ring quotients of $r$ and the set of quotients of $B$ and the ideal generated by an arbitrary binary relation of $r$.
RingQuot.ringQuotToIdealQuotientdefMathlib.Algebra.RingQuot, function or constant
Wording
the ring quotient to ideal quotient of r (from the name)
English
Let $r$ be a function from elements of $B$ and elements of $B$ to propositions. Then the ring quotient to ideal quotient of $r$ is a ring homomorphism of the set of ring quotients of $r$ and the set of quotients of $B$ and the ideal generated by an arbitrary binary relation of $r$ defined as $\operatorname{lift}$ applied to $\operatorname{mk}$ applied to the ideal generated by an arbitrary binary relation of $r$.
RingQuot.smuldefMathlib.Algebra.RingQuot, function or constant
Wording
the scalar multiple of n and x3 (from the name)
English
Let $r$ be a function from elements of $R$ and elements of $R$ to propositions. Let $n$ be an element of $S$. Let $x_{3}$ be a ring quotient of $r$. Then the scalar multiple of $n$ and $x_{3}$ is a ring quotient of $r$.
RingQuot.toQuotdefMathlib.Algebra.RingQuot, function or constant
Wording
the quotient of self (from the name)
English
Let $\mathrm{self}$ be a ring quotient of $r$. Then the quotient of $\mathrm{self}$ is an element of $\mathrm{Quot}$ applied to $\operatorname{Rel}$ applied to $r$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Algebra.SkewMonoidAlgebra.Basic

SkewMonoidAlgebrastructureMathlib.Algebra.SkewMonoidAlgebra.Basic, type
Wording
skew monoid algebra of G over k (from the docstring)
English
Let $k$ and $G$ be sets. Then the skew monoid algebras of $G$ over $k$ are a basic type.
SkewMonoidAlgebra.DistribMulActionHom.singledefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
no wording
English
Let $a$ be an element of $x_{3}$. Then $\operatorname{single}$ applied to $a$ is a distributive multiplicative action homomorphism of $M$ and the set of skew monoid algebras of $x_{3}$ over $M$.
SkewMonoidAlgebra.basisSingleOnedefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the basis single one (from the name)
English
The basis single one is a basis of $k$ and the set of skew monoid algebras of $G$ over $k$ defined as $\operatorname{ofRepr}$ applied to the coefficient linear equivalence.
SkewMonoidAlgebra.coeffdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the coefficient of self (from the name)
English
Let $\mathrm{self}$ be a skew monoid algebra of $G$ over $k$. Then the coefficient of $\mathrm{self}$ is an element of $\FinsuppMACRoQ {G}{k}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SkewMonoidAlgebra.coeffAddEquivdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the coefficient additive equivalence (from the name)
English
The coefficient additive equivalence is an additive equivalence of the set of skew monoid algebras of $G$ over $k$ and $\FinsuppMACRoQ {G}{k}$.
SkewMonoidAlgebra.coeffLinearEquivdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the coefficient linear equivalence (from the name)
English
The coefficient linear equivalence is a linear equivalence of the set of skew monoid algebras of $G$ over $k$ and $\FinsuppMACRoQ {G}{k}$.
SkewMonoidAlgebra.liftNCdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
no wording
English
Let $f$ be an additive monoid homomorphism of $k$ and $R$. Let $g$ be a function from elements of $G$ to elements of $R$. Then $\operatorname{liftNC}$ applied to $f$ and $g$ is an additive monoid homomorphism of the set of skew monoid algebras of $G$ over $k$ and $R$ defined as the composition of $\operatorname{liftAddHom}$ applied to the function that maps $x_{3}$ to the composition of the right multiplicative of $g$ applied to $x_{3}$ and $f$ and the additive monoid homomorphism of the coefficient additive equivalence.
SkewMonoidAlgebra.liftNCRingHomdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
no wording
English
Let $f$ be a ring homomorphism of $k$ and $R$. Let $g$ be a monoid homomorphism of $G$ and $R$ such that for all elements $x_{4}$ of $k$, for all elements $y$ of $G$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {y}{x_{4}})\times g (y)}{g (y)\times f (x_{4})}$. Then $\operatorname{liftNCRingHom}$ applied to $f$, $g$ and $\mathrm{h\_comm}$ is a ring homomorphism of the set of skew monoid algebras of $G$ over $k$ and $R$.
SkewMonoidAlgebra.lsingledefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
no wording
English
Let $R$ be a set. Let $a$ be an element of $x_{2}$. Then $\operatorname{lsingle}$ applied to $R$ and $a$ is a linear map of $M$ and the set of skew monoid algebras of $x_{2}$ over $M$.
SkewMonoidAlgebra.mapDomaindefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the map domain of f (from the name)
English
Let $f$ be a function from elements of $G$ to elements of $\mathrm{G'}$. Then the map domain of $f$ is an additive monoid homomorphism of the set of skew monoid algebras of $G$ over $k$ and the set of skew monoid algebras of $\mathrm{G'}$ over $k$.
SkewMonoidAlgebra.mapDomainRingHomdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the map domain ring homomorphism of hf (from the name)
English
Assume that for all elements $a$ of $x$, for all elements $x_{9}$ of $x_{2}$, $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{9}}}{\HSMulhSMulMACRoAL {f (a)}{x_{9}}}$. Then the map domain ring homomorphism of $\mathrm{hf}$ is a ring homomorphism of the set of skew monoid algebras of $x$ over $x_{2}$ and the set of skew monoid algebras of $x_{1}$ over $x_{2}$.
SkewMonoidAlgebra.ofdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
no wording
English
Let $k$ and $G$ be sets. Then $\operatorname{of}$ applied to $k$ and $G$ is a monoid homomorphism of $G$ and the set of skew monoid algebras of $G$ over $k$.
SkewMonoidAlgebra.singledefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
no wording
English
Let $a$ be an element of $G$. Let $b$ be an element of $k$. Then $\operatorname{single}$ applied to $a$ and $b$ is a skew monoid algebra of $G$ over $k$ defined as $\operatorname{ofCoeff}$ applied to $\FinsuppsingleMACRoS {a}{b}$.
SkewMonoidAlgebra.singleAddHomdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the single additive homomorphism of a (from the name)
English
Let $a$ be an element of $G$. Then the single additive homomorphism of $a$ is an additive monoid homomorphism of $k$ and the set of skew monoid algebras of $G$ over $k$.
SkewMonoidAlgebra.singleOneRingHomdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the single one ring homomorphism (from the name)
English
The single one ring homomorphism is a ring homomorphism of $k$ and the set of skew monoid algebras of $G$ over $k$.
SkewMonoidAlgebra.supportdefMathlib.Algebra.SkewMonoidAlgebra.Basic, function or constant
Wording
the support of p (from the name)
English
Let $p$ be a skew monoid algebra of $G$ over $k$. Then the support of $p$ is a finite set of $G$ defined as the support of the coefficient of $p$.

Mathlib.Algebra.SkewMonoidAlgebra.Lift

SkewMonoidAlgebra.domCongrdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the domain congruence of e (from the name)
English
Let $e$ be an equivalence from $G$ to $H$. Then the domain congruence of $e$ is an additive equivalence of the set of skew monoid algebras of $G$ over $A$ and the set of skew monoid algebras of $H$ over $A$.
SkewMonoidAlgebra.domCongrAlgdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the domain congruence algebra of A and he (from the name)
English
Let $k$ and $A$ be sets such that for all elements $a$ of $G$, for all elements $x_{7}$ of $A$, $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{7}}}{\HSMulhSMulMACRoAL {e (a)}{x_{7}}}$. Then the domain congruence algebra of $A$ and $\mathrm{he}$ is an algebra isomorphism of the set of skew monoid algebras of $G$ over $A$ and the set of skew monoid algebras of $H$ over $A$.
SkewMonoidAlgebra.domLCongrdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the domain congruence of e (from the name)
English
Let $e$ be an equivalence from $G$ to $H$. Then the domain congruence of $e$ is a linear equivalence of the set of skew monoid algebras of $G$ over $A$ and the set of skew monoid algebras of $H$ over $A$.
SkewMonoidAlgebra.equivMapDomaindefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the equivalence map domain of f and l (from the name)
English
Let $f$ be an equivalence from $G$ to $H$. Let $l$ be a skew monoid algebra of $G$ over $k$. Then the equivalence map domain of $f$ and $l$ is a skew monoid algebra of $H$ over $k$ defined as $\operatorname{ofCoeff}$ applied to the equivalence map domain of $f$ and the coefficient of $l$.
SkewMonoidAlgebra.liftdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the lift of G and A (from the name)
English
Let $k$, $G$ and $A$ be sets. Then the lift of $G$ and $A$ is an equivalence from the set of monoid homomorphisms of $G$ and $A$ to the set of algebra homomorphisms of the set of skew monoid algebras of $G$ over $k$ and $A$.
SkewMonoidAlgebra.liftNCAlgHomdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
no wording
English
Let $f$ be an algebra homomorphism of $A$ and $B$. Let $g$ be a monoid homomorphism of $G$ and $B$ such that for all elements $x_{7}$ of $A$, for all elements $y$ of $G$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {y}{x_{7}})\times g (y)}{g (y)\times f (x_{7})}$. Then $\operatorname{liftNCAlgHom}$ applied to $f$, $g$ and $\mathrm{h\_comm}$ is an algebra homomorphism of the set of skew monoid algebras of $G$ over $A$ and $B$.
SkewMonoidAlgebra.mapDomainAlgHomdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the map domain algebra homomorphism of A and hf (from the name)
English
Let $k$ and $A$ be sets such that for all elements $a$ of $G$, for all elements $x_{8}$ of $A$, $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{8}}}{\HSMulhSMulMACRoAL {f (a)}{x_{8}}}$. Then the map domain algebra homomorphism of $A$ and $\mathrm{hf}$ is an algebra homomorphism of the set of skew monoid algebras of $G$ over $A$ and the set of skew monoid algebras of $H$ over $A$.
SkewMonoidAlgebra.submoduleOfSmulMemdefMathlib.Algebra.SkewMonoidAlgebra.Lift, function or constant
Wording
the submodule of W and h1 (from the name)
English
Let $W$ be a submodule of $k$ and $V$ such that for all elements $g$ of $G$, for all elements $v$ of $V$, if $v$ is an element of $W$, then $\HSMulhSMulMACRoAL {\operatorname{of} (k , G , g)}{v}$ is an element of $W$. Then the submodule of $W$ and $h_{1}$ is a submodule of the set of skew monoid algebras of $G$ over $k$ and $V$.

Mathlib.Algebra.SkewMonoidAlgebra.Single

SkewMonoidAlgebra.erasedefMathlib.Algebra.SkewMonoidAlgebra.Single, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{erase}$ applied to $a$ is an additive monoid homomorphism of the set of skew monoid algebras of $x$ over $M$ and the set of skew monoid algebras of $x$ over $M$.
SkewMonoidAlgebra.updatedefMathlib.Algebra.SkewMonoidAlgebra.Single, function or constant
Wording
no wording
English
Let $f$ be a skew monoid algebra of $x$ over $M$. Let $a$ be an element of $x$. Let $b$ be an element of $M$. Then $\operatorname{update}$ applied to $f$, $a$ and $b$ is a skew monoid algebra of $x$ over $M$ defined as $\operatorname{ofCoeff}$ applied to $\operatorname{update}$ applied to the coefficient of $f$, $a$ and $b$.

Mathlib.Algebra.SkewPolynomial.Basic

SkewPolynomialdefMathlib.Algebra.SkewPolynomial.Basic, type
Wording
skew polynomial of R (from the name)
English
Let $R$ be a set. Then a skew polynomial of $R$ is an element of the function that maps $R$ to the set of skew monoid algebras of the set of multiplicatives of $\Natural$ over $R$.
SkewPolynomial.CdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
no wording
English
$\operatorname{C}$ is an additive monoid homomorphism of $R$ and the set of skew polynomials of $R$ defined as the single additive homomorphism of $1$.
SkewPolynomial.CRingHomdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
the ring homomorphism (from the name)
English
The ring homomorphism is a ring homomorphism of $R$ and the set of skew polynomials of $R$ defined as the single one ring homomorphism.
SkewPolynomial.XdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
no wording
English
$\operatorname{X}$ is a skew polynomial of $R$ defined as $\operatorname{monomial}$ applied to $1$ and $1$.
SkewPolynomial.coeffdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
the coefficient of p and x1 (from the name)
English
Let $p$ be a skew polynomial of $R$. Let $x_{1}$ be a natural number. Then the coefficient of $p$ and $x_{1}$ is an element of $R$ defined as $\operatorname{coeff}$ applied to $p$ and $\operatorname{ofAdd}$ applied to $x_{1}$.
SkewPolynomial.erasedefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
no wording
English
Let $n$ be a natural number. Let $p$ be a skew polynomial of $R$. Then $\operatorname{erase}$ applied to $n$ and $p$ is a skew polynomial of $R$ defined as $\operatorname{erase}$ applied to $\operatorname{ofAdd}$ applied to $n$ and $p$.
SkewPolynomial.monomialdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
the monomial of n (from the docstring)
English
Let $n$ be a natural number. Then the monomial of $n$ is a linear map of $R$ and the set of skew polynomials of $R$ defined as $\operatorname{lsingle}$ applied to $R$ and $\operatorname{ofAdd}$ applied to $n$.
SkewPolynomial.sumdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
the sum of p and f (from the name)
English
Let $p$ be a skew polynomial of $R$. Let $f$ be a function from natural numbers and elements of $R$ to elements of $S$. Then the sum of $p$ and $f$ is an element of $S$ defined as the sum of the coefficient of $p$ and the function that maps $n$ and $r$ to $f$ applied to $\operatorname{toAdd}$ applied to $n$ and $r$.
SkewPolynomial.supportdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
the support of p (from the name)
English
Let $p$ be a skew polynomial of $R$. Then the support of $p$ is a finite set of $\Natural$.
SkewPolynomial.updatedefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
no wording
English
Let $p$ be a skew polynomial of $R$. Let $n$ be a natural number. Let $a$ be an element of $R$. Then $\operatorname{update}$ applied to $p$, $n$ and $a$ is a skew polynomial of $R$ defined as $\operatorname{update}$ applied to $p$, $\operatorname{ofAdd}$ applied to $n$ and $a$.
SkewPolynomial.φdefMathlib.Algebra.SkewPolynomial.Basic, function or constant
Wording
no wording
English
$\mathrm{SkewPolynomial\_\_\_u3c6\_}$ is a ring homomorphism of $R$ and $R$ defined as the ring homomorphism of $\operatorname{ofAdd}$ applied to $1$.

Mathlib.Algebra.Squarefree.Basic

SquarefreedefMathlib.Algebra.Squarefree.Basic, predicate
Wording
r is a squarefree (from the name)
English
Let $r$ be an element of $R$. Then $r$ is a squarefree, if for all elements $x_{1}$ of $R$, if $x_{1} \times x_{1}$ divides $r$, then $x_{1}$ is a unit.

Mathlib.Algebra.Star.Basic

Equiv.Perm.stardefMathlib.Algebra.Star.Basic, function or constant
Wording
the star (from the name)
English
The star is a permutation of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{star}$, $\operatorname{star}$, $\mathrm{Equiv\_\_left\_inv}$ applied to the permutation of $\operatorname{star}$ and $\mathrm{InvolutiveStar\_\_star\_involutive}$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the permutation of $\operatorname{star}$ and $\mathrm{InvolutiveStar\_\_star\_involutive}$.
InvolutiveStarclassMathlib.Algebra.Star.Basic, predicate
Wording
R is a involutive star (from the name)
English
Let $R$ be a set. Then we can say that $R$ is an involutive star.
IsProperStarclassMathlib.Algebra.Star.Basic, predicate
Wording
R is a proper star (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a proper star.
StarAddMonoidclassMathlib.Algebra.Star.Basic, predicate
Wording
R is a star additive monoid (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a star additive monoid.
StarHomClassclassMathlib.Algebra.Star.Basic, predicate
Wording
no wording
English
Let $F$ be a set. Let $R$ and $S$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{StarHomClass}$ holds for $F$, $R$ and $S$.
StarMemClassclassMathlib.Algebra.Star.Basic, predicate
Wording
no wording
English
Let $S$ and $R$ be sets. Then we can say that $\mathrm{StarMemClass}$ holds for $S$ and $R$.
StarModuleclassMathlib.Algebra.Star.Basic, predicate
Wording
A is a star module with respect to R (from the name)
English
Let $R$ and $A$ be sets. Then we can say that $A$ is a star module with respect to $R$.
StarMulclassMathlib.Algebra.Star.Basic, predicate
Wording
R is a star product (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a star product.
StarRingclassMathlib.Algebra.Star.Basic, predicate
Wording
R is a star ring (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a star ring.
TrivialStarclassMathlib.Algebra.Star.Basic, predicate
Wording
R is a trivial star (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a trivial star.
starAddEquivdefMathlib.Algebra.Star.Basic, function or constant
Wording
the star additive equivalence (from the name)
English
The star additive equivalence is an additive equivalence of $R$ and $R$ defined as $\operatorname{mk}$ applied to the star and $\mathrm{StarAddMonoid\_\_star\_add}$.
starMulAutdefMathlib.Algebra.Star.Basic, function or constant
Wording
the star multiplicative automorphism (from the name)
English
The star multiplicative automorphism is a multiplicative automorphism of $R$.
starMulEquivdefMathlib.Algebra.Star.Basic, function or constant
Wording
the star multiplicative equivalence (from the name)
English
The star multiplicative equivalence is a multiplicative equivalence of $R$ and the set of multiplicative opposites of $R$.
starRingAutdefMathlib.Algebra.Star.Basic, function or constant
Wording
the star ring automorphism (from the name)
English
The star ring automorphism is a ring automorphism of $R$.
starRingEnddefMathlib.Algebra.Star.Basic, function or constant
Wording
the star ring end of R (from the name)
English
Let $R$ be a set. Then the star ring end of $R$ is a ring homomorphism of $R$ and $R$.
starRingEquivdefMathlib.Algebra.Star.Basic, function or constant
Wording
the star ring isomorphism (from the name)
English
The star ring isomorphism is a ring isomorphism of $R$ and the set of multiplicative opposites of $R$.

Mathlib.Algebra.Star.CHSH

IsCHSHTuplestructureMathlib.Algebra.Star.CHSH, predicate
Wording
no wording
English
Let $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $R$. Then we can say that $\mathrm{IsCHSHTuple}$ holds for $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$.

Mathlib.Algebra.Star.CentroidHom

CentroidHom.centerStarEmbeddingdefMathlib.Algebra.Star.CentroidHom, function or constant
Wording
the center star embedding (from the name)
English
The center star embedding is a non unital star ring homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{CentroidHom} (x))}{x_{3}})}$ and the set of centroid homomorphisms of $x$.
CentroidHom.starCenterIsoCentroiddefMathlib.Algebra.Star.CentroidHom, function or constant
Wording
the canonical isomorphism from the center (from the docstring)
English
The canonical isomorphism from the center is a star ring isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{3}})}$ and the set of centroid homomorphisms of $x$.
CentroidHom.starCenterToCentroiddefMathlib.Algebra.Star.CentroidHom, function or constant
Wording
the canonical homomorphism from the center into the centroid (from the docstring)
English
The canonical homomorphism from the center into the centroid is a non unital star ring homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{3}})}$ and the set of centroid homomorphisms of $x$ defined as the composition of the center star embedding and the star center to centroid center.
CentroidHom.starCenterToCentroidCenterdefMathlib.Algebra.Star.CentroidHom, function or constant
Wording
the star center to centroid center (from the name)
English
The star center to centroid center is a non unital star ring homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{CentroidHom} (x))}{x_{4}})}$.

Mathlib.Algebra.Star.Conjneg

conjnegdefMathlib.Algebra.Star.Conjneg, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $G$ to elements of $R$. Let $x_{3}$ be an element of $G$. Then $\mathrm{conjneg}$ applied to $f$ and $x_{3}$ is an element of $R$ defined as $\operatorname{starRingEnd}$ applied to the set of functions from elements of $G$ to elements of $R$, the function that maps $x_{6}$ to $f$ applied to $\operatorname{neg}$ applied to $x_{6}$ and $x_{3}$.
conjnegRingHomdefMathlib.Algebra.Star.Conjneg, function or constant
Wording
no wording
English
$\mathrm{conjnegRingHom}$ is a ring homomorphism of the set of functions from elements of $G$ to elements of $R$ and the set of functions from elements of $G$ to elements of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{conjneg}$ and $\mathrm{conjneg\_one}$ and $\mathrm{conjneg\_mul}$, $\mathrm{conjneg\_zero}$ and $\mathrm{conjneg\_add}$.

Mathlib.Algebra.Star.Free

FreeAlgebra.starHomdefMathlib.Algebra.Star.Free, function or constant
Wording
the star homomorphism (from the name)
English
The star homomorphism is an algebra isomorphism of the set of free algebras of $R$ and $X$ and the set of multiplicative opposites of the set of free algebras of $R$ and $X$.

Mathlib.Algebra.Star.Module

StarModule.decomposeProdAdjointdefMathlib.Algebra.Star.Module, function or constant
Wording
no wording
English
Let $R$ and $A$ be sets. Then $\operatorname{decomposeProdAdjoint}$ applied to $R$ and $A$ is a linear equivalence of $A$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{skewAdjoint} (A)}{x_{7}})}$.
selfAdjoint.submoduledefMathlib.Algebra.Star.Module, function or constant
Wording
the submodule of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the submodule of $R$ and $A$ is a submodule of $R$ and $A$.
selfAdjointPartdefMathlib.Algebra.Star.Module, function or constant
Wording
the self-adjoint part of R (from the docstring)
English
Let $R$ be a set. Then the self-adjoint part of $R$ is a linear map of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{6}})}$.
skewAdjoint.submoduledefMathlib.Algebra.Star.Module, function or constant
Wording
the submodule of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the submodule of $R$ and $A$ is a submodule of $R$ and $A$.
skewAdjointPartdefMathlib.Algebra.Star.Module, function or constant
Wording
the skew adjoint part of R (from the name)
English
Let $R$ be a set. Then the skew adjoint part of $R$ is a linear map of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{skewAdjoint} (A)}{x_{6}})}$.
starLinearEquivdefMathlib.Algebra.Star.Module, function or constant
Wording
the star linear equivalence of R (from the name)
English
Let $R$ be a set. Then the star linear equivalence of $R$ is a linear equivalence of $A$ and $A$.

Mathlib.Algebra.Star.MonoidHom

StarMonoidHomstructureMathlib.Algebra.Star.MonoidHom, type
Wording
star monoid homomorphism of A and B (from the name)
English
Let $A$ and $B$ be sets. Then the star monoid homomorphisms of $A$ and $B$ are a basic type.
StarMonoidHom.compdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a star monoid homomorphism of $B$ and $C$. Let $g$ be a star monoid homomorphism of $A$ and $B$. Then the composition of $f$ and $g$ is a star monoid homomorphism of $A$ and $C$.
StarMonoidHom.copydefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the copy of f and h (from the name)
English
Let $f$ be a star monoid homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a star monoid homomorphism of $A$ and $B$.
StarMonoidHom.iddefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the identity of A (from the docstring)
English
Let $A$ be a set. Then the identity of $A$ is a star monoid homomorphism of $A$ and $A$.
StarMonoidHom.ofClassdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the star monoid homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the star monoid homomorphism of $f$ is a star monoid homomorphism of $A$ and $B$.
StarMulEquivstructureMathlib.Algebra.Star.MonoidHom, type
Wording
star multiplicative equivalence of A and B (from the name)
English
Let $A$ and $B$ be sets. Then the star multiplicative equivalences of $A$ and $B$ are a basic type.
StarMulEquiv.ofBijectivedefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the star multiplicative equivalence of f and hf (from the name)
English
Let $f$ be a star monoid homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the star multiplicative equivalence of $f$ and $\mathrm{hf}$ is a star multiplicative equivalence of $A$ and $B$.
StarMulEquiv.ofClassdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the star multiplicative equivalence of f (from the name)
English
Let $f$ be an element of $F$. Then the star multiplicative equivalence of $f$ is a star multiplicative equivalence of $A$ and $B$.
StarMulEquiv.ofStarMonoidHomdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the star multiplicative equivalence of f and g (from the name)
English
Let $f$ be a star monoid homomorphism of $A$ and $B$. Let $g$ be a star monoid homomorphism of $B$ and $A$ such that the composition of $g$ and $f$ is equal to the identity of $A$ and the composition of $f$ and $g$ is equal to the identity of $B$. Then the star multiplicative equivalence of $f$ and $g$ is a star multiplicative equivalence of $A$ and $B$.
StarMulEquiv.refldefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the identity map of A (from the docstring)
English
Let $A$ be a set. Then the identity map of $A$ is a star multiplicative equivalence of $A$ and $A$.
StarMulEquiv.symmdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the inverse of e (from the docstring)
English
Let $e$ be a star multiplicative equivalence of $A$ and $B$. Then the inverse of $e$ is a star multiplicative equivalence of $B$ and $A$.
StarMulEquiv.toStarMonoidHomdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the star monoid homomorphism of f (from the name)
English
Let $f$ be a star multiplicative equivalence of $A$ and $B$. Then the star monoid homomorphism of $f$ is a star monoid homomorphism of $A$ and $B$.
StarMulEquiv.transdefMathlib.Algebra.Star.MonoidHom, function or constant
Wording
the composition of x6 and x7 (from the name)
English
Let $x_{6}$ be a star multiplicative equivalence of $A$ and $B$. Let $x_{7}$ be a star multiplicative equivalence of $B$ and $C$. Then the composition of $x_{6}$ and $x_{7}$ is a star multiplicative equivalence of $A$ and $C$.

Mathlib.Algebra.Star.NonUnitalSubalgebra

NonUnitalStarAlgHom.codRestrictdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
no wording
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Let $S$ be a non unital star subalgebra of $R$ and $B$ such that for all elements $x_{8}$ of $A$, $\MembershipmemMACRoT {S}{f (x_{8})}$. Then $\operatorname{codRestrict}$ applied to $f$, $S$ and $\mathrm{hf}$ is a non unital star algebra homomorphism of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$.
NonUnitalStarAlgHom.equalizerdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the equalizer of x7 and x8 (from the name)
English
Let $x_{7}$ and $x_{8}$ be non unital star algebra homomorphisms of $A$ and $B$. Then the equalizer of $x_{7}$ and $x_{8}$ is a non unital star subalgebra of $R$ and $A$.
NonUnitalStarAlgHom.rangedefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the range of x7 (from the name)
English
Let $x_{7}$ be a non unital star algebra homomorphism of $A$ and $B$. Then the range of $x_{7}$ is a non unital star subalgebra of $R$ and $B$.
NonUnitalStarAlgHom.rangeRestrictdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
no wording
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a non unital star algebra homomorphism of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{7}})}$ defined as $\operatorname{codRestrict}$ applied to $f$, the range of $f$ and $\mathrm{NonUnitalStarAlgHom\_\_mem\_range\_self}$ applied to $f$.
NonUnitalStarAlgebra.adjoindefMathlib.Algebra.Star.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 star subalgebra of $R$ and $A$.
NonUnitalStarAlgebra.gidefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
no wording
English
$\operatorname{gi}$ is a Galois insertion of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{instSetLike}$.
NonUnitalStarAlgebra.toTopdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the top (from the name)
English
The top is a non unital star algebra homomorphism of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{5}})}$.
NonUnitalStarSubalgebrastructureMathlib.Algebra.Star.NonUnitalSubalgebra, type
Wording
non unital star subalgebra of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the non unital star subalgebras of $R$ and $A$ are a basic type.
NonUnitalStarSubalgebra.centerdefMathlib.Algebra.Star.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 star subalgebra of $R$ and $A$.
NonUnitalStarSubalgebra.centralizerdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the centralizer of R and s (from the name)
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 star subalgebra of $R$ and $A$.
NonUnitalStarSubalgebra.comapdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the preimage of f and S (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Let $S$ be a non unital star subalgebra of $R$ and $B$. Then the preimage of $f$ and $S$ is a non unital star subalgebra of $R$ and $A$.
NonUnitalStarSubalgebra.copydefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the copy of S and s (from the name)
English
Let $S$ be a non unital star 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 star subalgebra of $R$ and $A$.
NonUnitalStarSubalgebra.iSupLiftdefMathlib.Algebra.Star.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_{7}$ to non unital star subalgebras of $R$ and $A$ such that $\mathrm{Directed}$ holds for the function that maps $x_{12}$ and $x_{13}$ to $\mathrm{Leq} (x_{12} , x_{13})$ and $K$. Let $f$ be a function from elements $i_{1}$ of $x_{7}$ to non unital star algebra homomorphisms of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {K (i_{1})}{x_{11}})}$ and $B$ such that for all elements $i$ and $j$ of $x_{7}$, for all elements $h_{4}$ 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_{4}$. Let $T$ be a non unital star 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 star algebra homomorphism of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {T}{x_{9}})}$ and $B$.
NonUnitalStarSubalgebra.inclusiondefMathlib.Algebra.Star.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 star algebra homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {T}{x_{5}})}$.
NonUnitalStarSubalgebra.mapdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the map of f and S (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Let $S$ be a non unital star subalgebra of $R$ and $A$. Then the map of $f$ and $S$ is a non unital star subalgebra of $R$ and $B$.
NonUnitalStarSubalgebra.ofClassdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the non unital star subalgebra of s (from the name)
English
Let $s$ be an element of $S$. Then the non unital star subalgebra of $s$ is a non unital star subalgebra of $R$ and $A$.
NonUnitalStarSubalgebra.proddefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the product of S and x7 (from the name)
English
Let $S$ be a non unital star subalgebra of $R$ and $A$. Let $x_{7}$ be a non unital star subalgebra of $R$ and $B$. Then the product of $S$ and $x_{7}$ is a non unital star subalgebra of $R$ and $\mathrm{Prod}$ applied to $A$ and $B$.
NonUnitalStarSubalgebra.toNonUnitalSubalgebra'defMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the non unital subalgebra (from the name)
English
The non unital subalgebra is an order embedding of the set of non unital star subalgebras of $R$ and $A$ and the set of non unital subalgebras of $R$ and $A$.
NonUnitalStarSubalgebra.toNonUnitalSubringdefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the non unital subring of S (from the name)
English
Let $S$ be a non unital star subalgebra of $R$ and $A$. Then the non unital subring of $S$ is a non unital subring of $A$.
NonUnitalStarSubalgebraClass.subtypedefMathlib.Algebra.Star.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 star algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {s}{x_{5}})}$ and $A$.
NonUnitalSubalgebra.starClosuredefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the star closure of S (from the name)
English
Let $S$ be a non unital subalgebra of $R$ and $A$. Then the star closure of $S$ is a non unital star subalgebra of $R$ and $A$.
NonUnitalSubalgebra.toNonUnitalStarSubalgebradefMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the non unital star subalgebra of s and h_star (from the name)
English
Let $s$ be a non unital subalgebra of $R$ and $A$ such that for all elements $x_{4}$ of $A$, if $x_{4}$ is an element of $s$, then the star of $x_{4}$ is an element of $s$. Then the non unital star subalgebra of $s$ and $\mathrm{h\_star}$ is a non unital star subalgebra of $R$ and $A$ defined as $\operatorname{mk}$ applied to $s$ and $\mathrm{h\_star}$.
StarAlgEquiv.ofInjective'defMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the star algebra isomorphism of f and hf (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the star algebra isomorphism of $f$ and $\mathrm{hf}$ is a star algebra isomorphism of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{7}})}$.
StarAlgEquiv.ofLeftInverse'defMathlib.Algebra.Star.NonUnitalSubalgebra, function or constant
Wording
the star algebra isomorphism of h (from the name)
English
Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the star algebra isomorphism of $h$ is a star algebra isomorphism of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{7}})}$.

Mathlib.Algebra.Star.NonUnitalSubsemiring

NonUnitalStarSubsemiringstructureMathlib.Algebra.Star.NonUnitalSubsemiring, type
Wording
non unital star subsemiring of R (from the name)
English
Let $R$ be a set. Then the non unital star subsemirings of $R$ are a basic type.
NonUnitalStarSubsemiring.centerdefMathlib.Algebra.Star.NonUnitalSubsemiring, function or constant
Wording
the center of R (from the docstring)
English
Let $R$ be a set. Then the center of $R$ is a non unital star subsemiring of $R$.
NonUnitalStarSubsemiring.copydefMathlib.Algebra.Star.NonUnitalSubsemiring, function or constant
Wording
the copy of S and s (from the name)
English
Let $S$ be a non unital star subsemiring of $R$. Let $s$ be an element of $\wp R$ such that $\EqtMACRoH {s}{S}$. Then the copy of $S$ and $s$ is a non unital star subsemiring of $R$.
NonUnitalStarSubsemiring.ofClassdefMathlib.Algebra.Star.NonUnitalSubsemiring, function or constant
Wording
the non unital star subsemiring of s (from the name)
English
Let $s$ be an element of $S$. Then the non unital star subsemiring of $s$ is a non unital star subsemiring of $R$.
SubStarSemigroupstructureMathlib.Algebra.Star.NonUnitalSubsemiring, type
Wording
difference star semigroup of M (from the name)
English
Let $M$ be a set. Then the difference star semigroups of $M$ are a basic type.

Mathlib.Algebra.Star.SelfAdjoint

IsSelfAdjointdefMathlib.Algebra.Star.SelfAdjoint, predicate
Wording
x1 is self-adjoint (from the docstring)
English
Let $x_{1}$ be an element of $R$. Then $x_{1}$ is self-adjoint, if the star of $x_{1}$ is equal to $x_{1}$.
IsStarNormalclassMathlib.Algebra.Star.SelfAdjoint, predicate
Wording
x2 is normal (from the docstring)
English
Let $x_{2}$ be an element of $R$. Then we can say that $x_{2}$ is normal.
selfAdjointdefMathlib.Algebra.Star.SelfAdjoint, function or constant
Wording
the self adjoint of R (from the name)
English
Let $R$ be a set. Then the self adjoint of $R$ is an additive subgroup of $R$.
skewAdjointdefMathlib.Algebra.Star.SelfAdjoint, function or constant
Wording
the skew adjoint of R (from the name)
English
Let $R$ be a set. Then the skew adjoint of $R$ is an additive subgroup of $R$.

Mathlib.Algebra.Star.StarAlgHom

NonUnitalAlgEquivClassclassMathlib.Algebra.Star.StarAlgHom, 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{NonUnitalAlgEquivClass}$ holds for $F$, $R$, $A$ and $B$.
NonUnitalStarAlgHomstructureMathlib.Algebra.Star.StarAlgHom, type
Wording
non unital star algebra homomorphism of A and B (from the name)
English
Let $R$, $A$ and $B$ be sets. Then the non unital star algebra homomorphisms of $A$ and $B$ are a basic type.
NonUnitalStarAlgHom.compdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $B$ and $C$. Let $g$ be a non unital star algebra homomorphism of $A$ and $B$. Then the composition of $f$ and $g$ is a non unital star algebra homomorphism of $A$ and $C$.
NonUnitalStarAlgHom.copydefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the copy of f and h (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a non unital star algebra homomorphism of $A$ and $B$.
NonUnitalStarAlgHom.fstdefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$.
NonUnitalStarAlgHom.iddefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the identity of R and A (from the docstring)
English
Let $R$ and $A$ be sets. Then the identity of $R$ and $A$ is a non unital star algebra homomorphism of $A$ and $A$.
NonUnitalStarAlgHom.inldefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of $1$ and $0$.
NonUnitalStarAlgHom.inrdefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphism of $B$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of $0$ and $1$.
NonUnitalStarAlgHom.ofClassdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the non unital star algebra homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the non unital star algebra homomorphism of $f$ is a non unital star algebra homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the non unital algebra homomorphism of $f$ and $\mathrm{StarHomClass\_\_map\_star}$ applied to $f$.
NonUnitalStarAlgHom.proddefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the product of f and g (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Let $g$ be a non unital star algebra homomorphism of $A$ and $C$. Then the product of $f$ and $g$ is a non unital star algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
NonUnitalStarAlgHom.prodEquivdefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphisms of $A$ and $B$ and the set of non unital star algebra homomorphisms of $A$ and $C$ to the set of non unital star algebra homomorphisms of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
NonUnitalStarAlgHom.restrictScalarsdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
no wording
English
Let $R$ be a set. Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a non unital star algebra homomorphism of $A$ and $B$.
NonUnitalStarAlgHom.snddefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$.
Pi.evalNonUnitalStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the evaluation non unital star algebra homomorphism of A and j (from the name)
English
Let $R$ be a set. Let $A$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the evaluation non unital star algebra homomorphism of $A$ and $j$ is a non unital star algebra homomorphism of the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$ and $A$ applied to $j$.
Pi.evalStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the evaluation star algebra homomorphism of A and j (from the name)
English
Let $R$ be a set. Let $A$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the evaluation star algebra homomorphism of $A$ and $j$ is a star algebra homomorphism of the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$ and $A$ applied to $j$.
StarAlgEquivstructureMathlib.Algebra.Star.StarAlgHom, type
Wording
star algebra isomorphism of A and B (from the name)
English
Let $R$, $A$ and $B$ be sets. Then the star algebra isomorphisms of $A$ and $B$ are a basic type.
StarAlgEquiv.arrowCongrdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the arrow congruence of x17 and x18 (from the name)
English
Let $x_{17}$ be a star algebra isomorphism of $x$ and $x_{2}$. Let $x_{18}$ be a star algebra isomorphism of $x_{1}$ and $x_{3}$. Then the arrow congruence of $x_{17}$ and $x_{18}$ is an equivalence from the set of star algebra homomorphisms of $x$ and $x_{1}$ to the set of star algebra homomorphisms of $x_{2}$ and $x_{3}$.
StarAlgEquiv.arrowCongr'defMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the arrow congruence of x17 and x18 (from the name)
English
Let $x_{17}$ be a star algebra isomorphism of $x$ and $x_{2}$. Let $x_{18}$ be a star algebra isomorphism of $x_{1}$ and $x_{3}$. Then the arrow congruence of $x_{17}$ and $x_{18}$ is an equivalence from the set of non unital star algebra homomorphisms of $x$ and $x_{1}$ to the set of non unital star algebra homomorphisms of $x_{2}$ and $x_{3}$.
StarAlgEquiv.ofAlgEquivdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra isomorphism of f and map_star (from the name)
English
Let $f$ be an algebra isomorphism of $A$ and $B$ such that for all elements $x_{7}$ of $A$, $f$ applied to the star of $x_{7}$ is equal to the star of $f$ applied to $x_{7}$. Then the star algebra isomorphism of $f$ and $\mathrm{map\_star}$ is a star algebra isomorphism of $A$ and $B$.
StarAlgEquiv.ofBijectivedefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra isomorphism of f and hf (from the name)
English
Let $f$ be an element of $F$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the star algebra isomorphism of $f$ and $\mathrm{hf}$ is a star algebra isomorphism of $A$ and $B$.
StarAlgEquiv.ofClassdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra isomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the star algebra isomorphism of $f$ is a star algebra isomorphism of $A$ and $B$.
StarAlgEquiv.ofNonUnitalStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra isomorphism of f and g (from the name)
English
Let $f$ be a non unital star algebra homomorphism of $x$ and $x_{1}$. Let $g$ be a non unital star algebra homomorphism of $x_{1}$ and $x$ such that the composition of $g$ and $f$ is equal to the identity of $R$ and $x$ and the composition of $f$ and $g$ is equal to the identity of $R$ and $x_{1}$. Then the star algebra isomorphism of $f$ and $g$ is a star algebra isomorphism of $x$ and $x_{1}$.
StarAlgEquiv.ofStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra isomorphism of f and g (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Let $g$ be a star algebra homomorphism of $B$ and $A$ such that the composition of $g$ and $f$ is equal to the identity of $R$ and $A$ and the composition of $f$ and $g$ is equal to the identity of $R$ and $B$. Then the star algebra isomorphism of $f$ and $g$ is a star algebra isomorphism of $A$ and $B$.
StarAlgEquiv.refldefMathlib.Algebra.Star.StarAlgHom, 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 star algebra isomorphism of $A$ and $A$.
StarAlgEquiv.symmdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the inverse of e (from the docstring)
English
Let $e$ be a star algebra isomorphism of $A$ and $B$. Then the inverse of $e$ is a star algebra isomorphism of $B$ and $A$.
StarAlgEquiv.toAlgEquivdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the algebra isomorphism of f (from the name)
English
Let $f$ be a star algebra isomorphism of $A$ and $B$. Then the algebra isomorphism of $f$ is an algebra isomorphism of $A$ and $B$.
StarAlgEquiv.toNonUnitalStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the non unital star algebra homomorphism of e (from the name)
English
Let $e$ be a star algebra isomorphism of $x$ and $x_{1}$. Then the non unital star algebra homomorphism of $e$ is a non unital star algebra homomorphism of $x$ and $x_{1}$.
StarAlgEquiv.toStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra homomorphism of e (from the name)
English
Let $e$ be a star algebra isomorphism of $x$ and $x_{1}$. Then the star algebra homomorphism of $e$ is a star algebra homomorphism of $x$ and $x_{1}$.
StarAlgEquiv.transdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the composition of x12 and x13 (from the name)
English
Let $x_{12}$ be a star algebra isomorphism of $A$ and $B$. Let $x_{13}$ be a star algebra isomorphism of $B$ and $C$. Then the composition of $x_{12}$ and $x_{13}$ is a star algebra isomorphism of $A$ and $C$.
StarAlgHomstructureMathlib.Algebra.Star.StarAlgHom, type
Wording
star algebra homomorphism of A and B (from the name)
English
Let $R$, $A$ and $B$ be sets. Then the star algebra homomorphisms of $A$ and $B$ are a basic type.
StarAlgHom.compdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a star algebra homomorphism of $B$ and $C$. Let $g$ be a star algebra homomorphism of $A$ and $B$. Then the composition of $f$ and $g$ is a star algebra homomorphism of $A$ and $C$.
StarAlgHom.copydefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the copy of f and h (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a star algebra homomorphism of $A$ and $B$.
StarAlgHom.fstdefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$.
StarAlgHom.iddefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the identity of R and A (from the docstring)
English
Let $R$ and $A$ be sets. Then the identity of $R$ and $A$ is a star algebra homomorphism of $A$ and $A$.
StarAlgHom.ofClassdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the star algebra homomorphism of $f$ is a star algebra homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the algebra homomorphism of $f$ and $\mathrm{StarHomClass\_\_map\_star}$ applied to $f$.
StarAlgHom.ofIddefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the star algebra homomorphism of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the star algebra homomorphism of $R$ and $A$ is a star algebra homomorphism of $R$ and $A$.
StarAlgHom.proddefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the product of f and g (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Let $g$ be a star algebra homomorphism of $A$ and $C$. Then the product of $f$ and $g$ is a star algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
StarAlgHom.prodEquivdefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphisms of $A$ and $B$ and the set of star algebra homomorphisms of $A$ and $C$ to the set of star algebra homomorphisms of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
StarAlgHom.snddefMathlib.Algebra.Star.StarAlgHom, 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 star algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$.
StarAlgHom.toNonUnitalStarAlgHomdefMathlib.Algebra.Star.StarAlgHom, function or constant
Wording
the non unital star algebra homomorphism of f (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Then the non unital star algebra homomorphism of $f$ is a non unital star algebra homomorphism of $A$ and $B$.

Mathlib.Algebra.Star.StarProjection

IsStarProjectionstructureMathlib.Algebra.Star.StarProjection, predicate
Wording
p is a star projection (from the name)
English
Let $p$ be an element of $R$. Then we can say that $p$ is a star projection.

Mathlib.Algebra.Star.StarRingHom

NonUnitalStarRingHomstructureMathlib.Algebra.Star.StarRingHom, type
Wording
non unital star ring homomorphism of A and B (from the name)
English
Let $A$ and $B$ be sets. Then the non unital star ring homomorphisms of $A$ and $B$ are a basic type.
NonUnitalStarRingHom.compdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a non unital star ring homomorphism of $B$ and $C$. Let $g$ be a non unital star ring homomorphism of $A$ and $B$. Then the composition of $f$ and $g$ is a non unital star ring homomorphism of $A$ and $C$.
NonUnitalStarRingHom.copydefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the copy of f and h (from the name)
English
Let $f$ be a non unital star ring homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a non unital star ring homomorphism of $A$ and $B$.
NonUnitalStarRingHom.iddefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the identity of A (from the docstring)
English
Let $A$ be a set. Then the identity of $A$ is a non unital star ring homomorphism of $A$ and $A$.
NonUnitalStarRingHom.ofClassdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the non unital star ring homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the non unital star ring homomorphism of $f$ is a non unital star ring homomorphism of $A$ and $B$.
NonUnitalStarRingHomClassclassMathlib.Algebra.Star.StarRingHom, predicate
Wording
no wording
English
Let $F$ be a set. Let $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{NonUnitalStarRingHomClass}$ holds for $F$, $A$ and $B$.
StarRingEquivstructureMathlib.Algebra.Star.StarRingHom, type
Wording
star ring isomorphism of A and B (from the name)
English
Let $A$ and $B$ be sets. Then the star ring isomorphisms of $A$ and $B$ are a basic type.
StarRingEquiv.ofBijectivedefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the star ring isomorphism of f and hf (from the name)
English
Let $f$ be an element of $F$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the star ring isomorphism of $f$ and $\mathrm{hf}$ is a star ring isomorphism of $A$ and $B$.
StarRingEquiv.ofClassdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the star ring isomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the star ring isomorphism of $f$ is a star ring isomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the ring isomorphism of $f$ and $\mathrm{StarRingEquivClass\_\_map\_star}$ applied to $f$.
StarRingEquiv.ofStarRingHomdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the star ring isomorphism of f and g (from the name)
English
Let $f$ be an element of $F$. Let $g$ be an element of $G$ such that for all elements $x_{7}$ of $A$, $\EqtMACRoH {g (f (x_{7}))}{x_{7}}$ and for all elements $x_{6}$ of $B$, $\EqtMACRoH {f (g (x_{6}))}{x_{6}}$. Then the star ring isomorphism of $f$ and $g$ is a star ring isomorphism of $A$ and $B$.
StarRingEquiv.refldefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the identity map (from the docstring)
English
The identity map is a star ring isomorphism of $A$ and $A$.
StarRingEquiv.symmdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the inverse of e (from the docstring)
English
Let $e$ be a star ring isomorphism of $A$ and $B$. Then the inverse of $e$ is a star ring isomorphism of $B$ and $A$.
StarRingEquiv.toNonUnitalStarRingHomdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the non unital star ring homomorphism of f (from the name)
English
Let $f$ be a star ring isomorphism of $A$ and $B$. Then the non unital star ring homomorphism of $f$ is a non unital star ring homomorphism of $A$ and $B$.
StarRingEquiv.transdefMathlib.Algebra.Star.StarRingHom, function or constant
Wording
the composition of x9 and x10 (from the name)
English
Let $x_{9}$ be a star ring isomorphism of $A$ and $B$. Let $x_{10}$ be a star ring isomorphism of $B$ and $C$. Then the composition of $x_{9}$ and $x_{10}$ is a star ring isomorphism of $A$ and $C$.
StarRingEquivClassclassMathlib.Algebra.Star.StarRingHom, predicate
Wording
no wording
English
Let $F$ be a set. Let $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{StarRingEquivClass}$ holds for $F$, $A$ and $B$.

Mathlib.Algebra.Star.Subalgebra

NonUnitalStarSubalgebra.toStarSubalgebradefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the star subalgebra of S and h1 (from the name)
English
Let $S$ be a non unital star subalgebra of $R$ and $A$ such that $1$ is an element of $S$. Then the star subalgebra of $S$ and $h_{1}$ is a star subalgebra of $R$ and $A$.
StarAlgEquiv.ofInjectivedefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the star algebra isomorphism of f and hf (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the star algebra isomorphism of $f$ and $\mathrm{hf}$ is a star algebra isomorphism of $A$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{8}})}$.
StarAlgEquiv.restrictScalarsdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
no wording
English
Let $R$ be a set. Let $f$ be a star algebra isomorphism of $A$ and $B$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a star algebra isomorphism of $A$ and $B$.
StarAlgHom.codRestrictdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
no wording
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Let $S$ be a star subalgebra of $R$ and $B$ such that for all elements $x_{9}$ of $A$, $\MembershipmemMACRoT {S}{f (x_{9})}$. Then $\operatorname{codRestrict}$ applied to $f$, $S$ and $\mathrm{hf}$ is a star algebra homomorphism of $A$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$.
StarAlgHom.equalizerdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the equalizer of two star of f and g (from the docstring)
English
Let $f$ and $g$ be star algebra homomorphisms of $A$ and $B$. Then the equalizer of two star of $f$ and $g$ is a star subalgebra of $R$ and $A$.
StarAlgHom.rangedefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the range of x8 (from the name)
English
Let $x_{8}$ be a star algebra homomorphism of $A$ and $B$. Then the range of $x_{8}$ is a star subalgebra of $R$ and $B$.
StarAlgHom.rangeRestrictdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
no wording
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a star algebra homomorphism of $A$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{8}})}$.
StarAlgHom.restrictScalarsdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
no wording
English
Let $R$ be a set. Let $f$ be a star algebra homomorphism of $A$ and $B$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a star algebra homomorphism of $A$ and $B$.
StarAlgebra.adjoindefMathlib.Algebra.Star.Subalgebra, 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 star subalgebra of $R$ and $A$.
StarAlgebra.gidefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
no wording
English
$\operatorname{gi}$ is a Galois insertion of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{setLike}$.
StarSubalgebrastructureMathlib.Algebra.Star.Subalgebra, type
Wording
star subalgebra of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the star subalgebras of $R$ and $A$ are a basic type.
StarSubalgebra.centralizerdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the centralizer of R and s (from the name)
English
Let $R$ be a set. Let $s$ be an element of $\wp A$. Then the centralizer of $R$ and $s$ is a star subalgebra of $R$ and $A$.
StarSubalgebra.comapdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the preimage of f and S (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Let $S$ be a star subalgebra of $R$ and $B$. Then the preimage of $f$ and $S$ is a star subalgebra of $R$ and $A$.
StarSubalgebra.copydefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the copy of S and s (from the name)
English
Let $S$ be a star 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 star subalgebra of $R$ and $A$.
StarSubalgebra.inclusiondefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the inclusion of h1 (from the name)
English
Assume that $x_{5} \leq x_{6}$. Then the inclusion of $h_{1}$ is a star algebra homomorphism of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{5}}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6}}{x_{8}})}$.
StarSubalgebra.mapdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the map of f and S (from the name)
English
Let $f$ be a star algebra homomorphism of $A$ and $B$. Let $S$ be a star subalgebra of $R$ and $A$. Then the map of $f$ and $S$ is a star subalgebra of $R$ and $B$.
StarSubalgebra.ofClassdefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the star subalgebra of s (from the name)
English
Let $s$ be an element of $S$. Then the star subalgebra of $s$ is a star subalgebra of $R$ and $A$.
StarSubalgebra.subtypedefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the subtype of S (from the name)
English
Let $S$ be a star subalgebra of $R$ and $A$. Then the subtype of $S$ is a star algebra homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ and $A$.
StarSubalgebra.toNonUnitalStarSubalgebradefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the non unital star subalgebra of S (from the name)
English
Let $S$ be a star subalgebra of $R$ and $A$. Then the non unital star subalgebra of $S$ is a non unital star subalgebra of $R$ and $A$.
Subalgebra.starClosuredefMathlib.Algebra.Star.Subalgebra, function or constant
Wording
the star closure of S (from the name)
English
Let $S$ be a subalgebra of $R$ and $A$. Then the star closure of $S$ is a star subalgebra of $R$ and $A$.

Mathlib.Algebra.Star.Subsemiring

StarSubsemiringstructureMathlib.Algebra.Star.Subsemiring, type
Wording
star subsemiring of R (from the name)
English
Let $R$ be a set. Then the star subsemirings of $R$ are a basic type.
StarSubsemiring.centerdefMathlib.Algebra.Star.Subsemiring, function or constant
Wording
the center of R (from the docstring)
English
Let $R$ be a set. Then the center of $R$ is a star subsemiring of $R$.
StarSubsemiring.copydefMathlib.Algebra.Star.Subsemiring, function or constant
Wording
the copy of S and s (from the name)
English
Let $S$ be a star subsemiring of $R$. Let $s$ be an element of $\wp R$ such that $\EqtMACRoH {s}{S}$. Then the copy of $S$ and $s$ is a star subsemiring of $R$.
StarSubsemiring.ofClassdefMathlib.Algebra.Star.Subsemiring, function or constant
Wording
the star subsemiring of s (from the name)
English
Let $s$ be an element of $S$. Then the star subsemiring of $s$ is a star subsemiring of $R$.
SubStarSemigroup.centerdefMathlib.Algebra.Star.Subsemiring, function or constant
Wording
the center of A (from the name)
English
Let $A$ be a set. Then the center of $A$ is a difference star semigroup of $A$ defined as $\operatorname{mk}$ applied to the center of $A$ and the function that maps $x_{2}$ to $\mathrm{Set\_\_star\_mem\_center}$.

Mathlib.Algebra.Star.Unitary

Unitary.mapdefMathlib.Algebra.Star.Unitary, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a star monoid homomorphism of $R$ and $S$. Then the map of $f$ is a star monoid homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{unitary} (R)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{unitary} (S)}{x_{5}})}$.
Unitary.mapEquivdefMathlib.Algebra.Star.Unitary, function or constant
Wording
the map equivalence of f (from the name)
English
Let $f$ be a star multiplicative equivalence of $R$ and $S$. Then the map equivalence of $f$ is a star multiplicative equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{unitary} (R)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{unitary} (S)}{x_{5}})}$.
Unitary.toUnitsdefMathlib.Algebra.Star.Unitary, function or constant
Wording
the unit (from the name)
English
The unit is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{unitary} (R)}{x_{2}})}$ and $\UnitsMACRoAO {R}$.
unitarydefMathlib.Algebra.Star.Unitary, function or constant
Wording
no wording
English
Let $R$ be a set. Then $\mathrm{unitary}$ applied to $R$ is a submonoid of $R$.
unitarySubgroupdefMathlib.Algebra.Star.Unitary, function or constant
Wording
the unitary subgroup of G (from the name)
English
Let $G$ be a set. Then the unitary subgroup of $G$ is a subgroup of $G$ defined as $\operatorname{mk}$ applied to $\mathrm{unitary}$ applied to $G$ and the function that maps $x_{2}$ to $\mathrm{Unitary\_\_inv\_mem}$.
unitarySubgroupUnitsEquivdefMathlib.Algebra.Star.Unitary, function or constant
Wording
the unitary subgroup of the units (from the docstring)
English
The unitary subgroup of the units is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{unitarySubgroup} (\UnitsMACRoAO {M})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{unitary} (M)}{x_{3}})}$.

Mathlib.Algebra.Star.UnitaryStarAlgAut

Unitary.conjStarAlgAutdefMathlib.Algebra.Star.UnitaryStarAlgAut, function or constant
Wording
the conjugate star algebra automorphism of S and R (from the name)
English
Let $S$ and $R$ be sets. Then the conjugate star algebra automorphism of $S$ and $R$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{unitary} (R)}{x_{3}})}$ and the set of star algebra isomorphisms of $R$ and $R$.

Mathlib.Algebra.Symmetrized

SymAlgdefMathlib.Algebra.Symmetrized, type
Wording
symmetric power algebra of x (from the name)
English
Let $x$ be a set. Then a symmetric power algebra of $x$ is an element of the function that maps $x$ to $x$.
SymAlg.symdefMathlib.Algebra.Symmetrized, function or constant
Wording
the symmetric power (from the name)
English
The symmetric power is an equivalence from $x$ to the set of symmetric power algebras of $x$ defined as the identity of $x$.
SymAlg.unsymdefMathlib.Algebra.Symmetrized, function or constant
Wording
no wording
English
$\operatorname{unsym}$ is an equivalence from the set of symmetric power algebras of $x$ to $x$ defined as the identity of the set of symmetric power algebras of $x$.

Mathlib.Algebra.Torsor.Basic

Equiv.constSMulHomdefMathlib.Algebra.Torsor.Basic, function or constant
Wording
the constant multiplicative homomorphism of P (from the name)
English
Let $P$ be a set. Then the constant multiplicative homomorphism of $P$ is a monoid homomorphism of $G$ and the set of permutations of $P$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $v$ to the constant product of $P$ and $v$ and $\mathrm{Equiv\_\_constSMul\_one}$ applied to $G$ and $P$ and $\mathrm{Equiv\_\_constSMul\_mul}$ applied to $P$.
Equiv.constVAddHomdefMathlib.Algebra.Torsor.Basic, function or constant
Wording
the constant additive homomorphism of G and P (from the name)
English
Let $G$ and $P$ be sets. Then the constant additive homomorphism of $G$ and $P$ is a monoid homomorphism of the set of multiplicatives of $G$ and the set of permutations of $P$.

Mathlib.Algebra.Torsor.Defs

AddTorsorclassMathlib.Algebra.Torsor.Defs, predicate
Wording
G is a additive torsor (from the name)
English
Let $G$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $P$ be a set. Then we can say that $G$ is an additive torsor.
Equiv.constSDivdefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the constant quotient of p (from the name)
English
Let $p$ be an element of $P$. Then the constant quotient of $p$ is an equivalence from $P$ to $G$.
Equiv.constSMuldefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the constant product of P and v (from the name)
English
Let $P$ be a set. Let $v$ be an element of $G$. Then the constant product of $P$ and $v$ is a permutation of $P$.
Equiv.constVAdddefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the constant sum of P and v (from the name)
English
Let $P$ be a set. Let $v$ be an element of $G$. Then the constant sum of $P$ and $v$ is a permutation of $P$.
Equiv.constVSubdefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the constant difference of p (from the name)
English
Let $p$ be an element of $P$. Then the constant difference of $p$ is an equivalence from $P$ to $G$.
Equiv.pointReflectiondefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the point reflection of x2 (from the name)
English
Let $x_{2}$ be an element of $P$. Then the point reflection of $x_{2}$ is a permutation of $P$ defined as the composition of the constant difference of $x_{2}$ and the vector sum constant of $x_{2}$.
Equiv.smulConstdefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the scalar multiple constant of p (from the name)
English
Let $p$ be an element of $P$. Then the scalar multiple constant of $p$ is an equivalence from $G$ to $P$ defined as $\operatorname{mk}$ applied to the function that maps $v$ to $\HSMulhSMulMACRoAL {v}{p}$, the function that maps $\mathrm{p'}$ to $\operatorname{sdiv}$ applied to $\mathrm{p'}$ and $p$, the function that maps $x_{2}$ to $\mathrm{smul\_sdiv}$ applied to $x_{2}$ and $p$ and the function that maps $x_{3}$ to $\mathrm{sdiv\_smul}$ applied to $x_{3}$ and $p$.
Equiv.vaddConstdefMathlib.Algebra.Torsor.Defs, function or constant
Wording
the vector sum constant of p (from the name)
English
Let $p$ be an element of $P$. Then the vector sum constant of $p$ is an equivalence from $G$ to $P$ defined as $\operatorname{mk}$ applied to the function that maps $v$ to the sum of $v$ and $p$, the function that maps $\mathrm{p'}$ to the vector difference of $\mathrm{p'}$ and $p$, the function that maps $x_{2}$ to $\mathrm{vadd\_vsub}$ applied to $x_{2}$ and $p$ and the function that maps $x_{3}$ to $\mathrm{vsub\_vadd}$ applied to $x_{3}$ and $p$.
TorsorclassMathlib.Algebra.Torsor.Defs, predicate
Wording
G is a torsor (from the name)
English
Let $G$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $P$ be a set. Then we can say that $G$ is a torsor.

Mathlib.Algebra.TrivSqZeroExt.Basic

TrivSqZeroExtdefMathlib.Algebra.TrivSqZeroExt.Basic, type
Wording
trivial square zero extension of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a trivial square zero extension of $R$ and $M$ is an element of the function that maps $R$ and $M$ to $\mathrm{Prod}$ applied to $R$ and $M$.
TrivSqZeroExt.fstdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the first component of x (from the name)
English
Let $x$ be a trivial square zero extension of $R$ and $M$. Then the first component of $x$ is an element of $R$ defined as $\ProdfstMACRoZ {x}$.
TrivSqZeroExt.fstHomdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the first component homomorphism of R and M (from the name)
English
Let $S$, $R$ and $M$ be sets. Then the first component homomorphism of $R$ and $M$ is an algebra homomorphism of the set of trivial square zero extensions of $R$ and $M$ and $R$.
TrivSqZeroExt.inldefMathlib.Algebra.TrivSqZeroExt.Basic, 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 trivial square zero extension of $R$ and $M$ defined as $\ProdmkMACRoU {r}{0}$.
TrivSqZeroExt.inlAlgHomdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the left injection algebra homomorphism of R and M (from the name)
English
Let $S$, $R$ and $M$ be sets. Then the left injection algebra homomorphism of $R$ and $M$ is an algebra homomorphism of $R$ and the set of trivial square zero extensions of $R$ and $M$.
TrivSqZeroExt.inlHomdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the left injection homomorphism of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the left injection homomorphism of $R$ and $M$ is a ring homomorphism of $R$ and the set of trivial square zero extensions of $R$ and $M$.
TrivSqZeroExt.inrdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the right injection of m (from the name)
English
Let $m$ be an element of $M$. Then the right injection of $m$ is a trivial square zero extension of $R$ and $M$ defined as $\ProdmkMACRoU {0}{m}$.
TrivSqZeroExt.inrHomdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the right injection homomorphism of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the right injection homomorphism of $R$ and $M$ is a linear map of $M$ and the set of trivial square zero extensions of $R$ and $M$.
TrivSqZeroExt.invertibleEquivInvertibleFstdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the invertible equivalence invertible first component of x4 (from the name)
English
Let $x_{4}$ be a trivial square zero extension of $R$ and $M$. Then the invertible equivalence invertible first component of $x_{4}$ is an equivalence from the proposition that $x_{4}$ is invertible to the proposition that the first component of $x_{4}$ is invertible.
TrivSqZeroExt.liftdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the lift of f and g (from the name)
English
Let $f$ be an algebra homomorphism of $R$ and $A$. Let $g$ be a linear map of $M$ and $A$ such that for all elements $x_{11}$ of $M$, for all elements $y$ of $M$, $\EqtMACRoH {g (x_{11})\times g (y)}{0}$, for all elements $r_{1}$ of $R$, for all elements $x_{10}$ of $M$, $\EqtMACRoH {g (\HSMulhSMulMACRoAL {r_{1}}{x_{10}})}{f (r_{1})\times g (x_{10})}$ and for all elements $r$ of $R$, for all elements $x_{9}$ of $M$, $\EqtMACRoH {g (\HSMulhSMulMACRoAL {\operatorname{op} (r)}{x_{9}})}{g (x_{9})\times f (r)}$. Then the lift of $f$ and $g$ is an algebra homomorphism of the set of trivial square zero extensions of $R$ and $M$ and $A$.
TrivSqZeroExt.liftEquivdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the lift equivalence (from the name)
English
The lift equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {\mathrm{fg}}{\mathrm{and} (\mathrm{forall} (M , \lambda x_{9} . \mathrm{forall} (M , \lambda y . \EqtMACRoH {(\operatorname{snd} (\mathrm{fg} , x_{9})\times \operatorname{snd} (\mathrm{fg} , y))}{0})), \mathrm{and} (\mathrm{forall} (R , \lambda r . \mathrm{forall} (M , \lambda x_{10} . \EqtMACRoH {\operatorname{snd} (\mathrm{fg} , \HSMulhSMulMACRoAL {r}{x_{10}})}{(\operatorname{fst} (\mathrm{fg} , r)\times \operatorname{snd} (\mathrm{fg} , x_{10}))})), \mathrm{forall} (R , \lambda r_{1} . \mathrm{forall} (M , \lambda x_{11} . \EqtMACRoH {\operatorname{snd} (\mathrm{fg} , \HSMulhSMulMACRoAL {\operatorname{op} (r_{1})}{x_{11}})}{(\operatorname{snd} (\mathrm{fg} , x_{11})\times \operatorname{fst} (\mathrm{fg} , r_{1}))}))))})}{\mathrm{AlgHom} (\mathrm{TrivSqZeroExt} (R , M), A)}$.
TrivSqZeroExt.liftEquivOfCommdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the lift equivalence (from the name)
English
The lift equivalence is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (M , \lambda x_{6} . \mathrm{forall} (M , \lambda y . \EqtMACRoH {(f (x_{6})\times f (y))}{0}))}$ to the set of algebra homomorphisms of the set of trivial square zero extensions of $\mathrm{R'}$ and $M$ and $A$.
TrivSqZeroExt.mapdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a linear map of $M$ and $N$. Then the map of $f$ is an algebra homomorphism of the set of trivial square zero extensions of $\mathrm{R'}$ and $M$ and the set of trivial square zero extensions of $\mathrm{R'}$ and $N$ defined as $\operatorname{liftEquivOfComm}$ applied to the composition of the right injection homomorphism of $\mathrm{R'}$ and $N$ and $f$.
TrivSqZeroExt.snddefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the second component of x (from the name)
English
Let $x$ be a trivial square zero extension of $R$ and $M$. Then the second component of $x$ is an element of $M$ defined as $\ProdsndMACRoAA {x}$.
TrivSqZeroExt.sndHomdefMathlib.Algebra.TrivSqZeroExt.Basic, function or constant
Wording
the second component homomorphism of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the second component homomorphism of $R$ and $M$ is a linear map of the set of trivial square zero extensions of $R$ and $M$ and $M$.

Mathlib.Algebra.TrivSqZeroExt.Ideal

TrivSqZeroExt.kerIdealdefMathlib.Algebra.TrivSqZeroExt.Ideal, function or constant
Wording
the kernel ideal of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the kernel ideal of $R$ and $M$ is an ideal of the set of trivial square zero extensions of $R$ and $M$ defined as the kernel of the first component homomorphism of $R$ and $M$.

Mathlib.Algebra.Tropical.Basic

MaxTropicaldefMathlib.Algebra.Tropical.Basic, type
Wording
no wording
English
Let $R$ be a set. Then an element of $\mathrm{MaxTropical}$ applied to $R$ is an element of the function that maps $R$ to $R$.
MaxTropical.equivMinTropicaldefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
$\operatorname{equivMinTropical}$ is a ring isomorphism of $\mathrm{MaxTropical}$ applied to $R$ and $\mathrm{MinTropical}$ applied to the set of order duals of $R$.
MaxTropical.tropdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $R$. Then $\operatorname{trop}$ applied to $x$ is an element of $\mathrm{MaxTropical}$ applied to $R$ defined as $\mathrm{id}$ applied to $x$.
MaxTropical.tropEquivdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
$\operatorname{tropEquiv}$ is an element of $\EquivMACRoAE {R}{\mathrm{MaxTropical} (R)}$ defined as $\operatorname{mk}$ applied to $\operatorname{trop}$, $\operatorname{untrop}$, $\mathrm{MaxTropical\_\_untrop\_trop}$ and $\mathrm{MaxTropical\_\_trop\_untrop}$.
MaxTropical.tropOrderIsodefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
$\operatorname{tropOrderIso}$ is an order isomorphism of $R$ and $\mathrm{MaxTropical}$ applied to $R$.
MaxTropical.tropRecdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
Let $h$ be a function from elements $X_{1}$ of $R$ to elements of $F$ applied to $\operatorname{trop}$ applied to $X_{1}$. Let $X$ be an element of $\mathrm{MaxTropical}$ applied to $R$. Then $\operatorname{tropRec}$ applied to $X_{1}$, $h$ and $X$ is an element of $F$ applied to $X$ defined as the function that maps $X$ to $X_{1}$ applied to $\operatorname{untrop}$ applied to $h$ and $X$.
MaxTropical.untropdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{MaxTropical}$ applied to $R$. Then $\operatorname{untrop}$ applied to $x$ is an element of $R$ defined as $\mathrm{id}$ applied to $x$.
MinTropicaldefMathlib.Algebra.Tropical.Basic, type
Wording
no wording
English
Let $R$ be a set. Then an element of $\mathrm{MinTropical}$ applied to $R$ is an element of the function that maps $R$ to $R$.
MinTropical.equivMaxTropicaldefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
$\operatorname{equivMaxTropical}$ is a ring isomorphism of $\mathrm{MinTropical}$ applied to $R$ and $\mathrm{MaxTropical}$ applied to the set of order duals of $R$.
MinTropical.tropdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $R$. Then $\operatorname{trop}$ applied to $x$ is an element of $\mathrm{MinTropical}$ applied to $R$ defined as $\mathrm{id}$ applied to $x$.
MinTropical.tropEquivdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
$\operatorname{tropEquiv}$ is an element of $\EquivMACRoAE {R}{\mathrm{MinTropical} (R)}$ defined as $\operatorname{mk}$ applied to $\operatorname{trop}$, $\operatorname{untrop}$, $\mathrm{MinTropical\_\_untrop\_trop}$ and $\mathrm{MinTropical\_\_trop\_untrop}$.
MinTropical.tropOrderIsodefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
$\operatorname{tropOrderIso}$ is an order isomorphism of $R$ and $\mathrm{MinTropical}$ applied to $R$.
MinTropical.tropRecdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
Let $h$ be a function from elements $X_{1}$ of $R$ to elements of $F$ applied to $\operatorname{trop}$ applied to $X_{1}$. Let $X$ be an element of $\mathrm{MinTropical}$ applied to $R$. Then $\operatorname{tropRec}$ applied to $X_{1}$, $h$ and $X$ is an element of $F$ applied to $X$ defined as the function that maps $X$ to $X_{1}$ applied to $\operatorname{untrop}$ applied to $h$ and $X$.
MinTropical.untropdefMathlib.Algebra.Tropical.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{MinTropical}$ applied to $R$. Then $\operatorname{untrop}$ applied to $x$ is an element of $R$ defined as $\mathrm{id}$ applied to $x$.

Mathlib.Algebra.Vertex.HVertexOperator

HVertexOperatordefMathlib.Algebra.Vertex.HVertexOperator, type
Wording
vertex operator of V and W (from the name)
English
Let $x$, $R$, $V$ and $W$ be sets. Then a vertex operator of $V$ and $W$ is an element of the function that maps $x$, $R$, $V$ and $W$ to the set of linear maps of $V$ and the set of Hahn modules of $R$ and $W$.
HVertexOperator.coeffdefMathlib.Algebra.Vertex.HVertexOperator, function or constant
Wording
the coefficient (from the name)
English
The coefficient is a linear map of the set of vertex operators of $V$ and $W$ and the set of functions from elements of $x$ to linear maps of $V$ and $W$.
HVertexOperator.compdefMathlib.Algebra.Vertex.HVertexOperator, function or constant
Wording
the composition of A and B (from the name)
English
Let $A$ be a vertex operator of $V$ and $W$. Let $B$ be a vertex operator of $U$ and $V$. Then the composition of $A$ and $B$ is a vertex operator of $U$ and $W$.
HVertexOperator.compHahnSeriesdefMathlib.Algebra.Vertex.HVertexOperator, function or constant
Wording
the composition Hahn series of B and u (from the name)
English
Let $A$ be a vertex operator of $V$ and $W$. Let $B$ be a vertex operator of $U$ and $V$. Let $u$ be an element of $U$. Then the composition Hahn series of $B$ and $u$ is a Hahn series of $x_{1}$ and the set of Hahn series of $x$ and $W$.
HVertexOperator.of_coeffdefMathlib.Algebra.Vertex.HVertexOperator, function or constant
Wording
the coefficient of f and hf (from the name)
English
Let $f$ be a function from elements of $x$ to linear maps of $V$ and $W$ such that for all elements $x_{7}$ of $V$, $\operatorname{IsPWO}$ holds for the support of the function that maps $x_{8}$ to $f$ applied to $x_{8}$ and $x_{7}$. Then the coefficient of $f$ and $\mathrm{hf}$ is a vertex operator of $V$ and $W$.

Mathlib.Algebra.Vertex.VertexOperator

VertexOperatordefMathlib.Algebra.Vertex.VertexOperator, type
Wording
vertex operator of R and V (from the name)
English
Let $R$ and $V$ be sets. Then a vertex operator of $R$ and $V$ is an element of the function that maps $R$ and $V$ to the set of vertex operators of $V$ and $V$.
VertexOperator.ncoeffdefMathlib.Algebra.Vertex.VertexOperator, function or constant
Wording
no wording
English
$\operatorname{ncoeff}$ is a linear map of the set of vertex operators of $R$ and $V$ and the set of functions from integers to ends of $R$ and $V$.
VertexOperator.of_coeffdefMathlib.Algebra.Vertex.VertexOperator, function or constant
Wording
the coefficient of f and hf (from the name)
English
Let $f$ be a function from integers to ends of $R$ and $V$ such that for all elements $x_{3}$ of $V$, the support of the function that maps $y$ to $f$ applied to $y$ and $x_{3}$ is bounded below. Then the coefficient of $f$ and $\mathrm{hf}$ is a vertex operator of $R$ and $V$.

Mathlib.Algebra.WithConv

WithConvstructureMathlib.Algebra.WithConv, type
Wording
no wording
English
Let $A$ be a set. Then the elements of $\mathrm{WithConv}$ applied to $A$ are a basic type.
WithConv.addEquivdefMathlib.Algebra.WithConv, function or constant
Wording
the additive equivalence of A (from the name)
English
Let $A$ be a set. Then the additive equivalence of $A$ is an additive equivalence of $\mathrm{WithConv}$ applied to $A$ and $A$.
WithConv.congrdefMathlib.Algebra.WithConv, function or constant
Wording
the congruence of f (from the name)
English
Let $f$ be an equivalence from $A$ to $B$. Then the congruence of $f$ is an element of $\EquivMACRoAE {\mathrm{WithConv} (A)}{\mathrm{WithConv} (B)}$ defined as the composition of the equivalence of $A$ and the composition of $f$ and the inverse of the equivalence of $B$.
WithConv.congrLinearEquivdefMathlib.Algebra.WithConv, function or constant
Wording
the congruence linear equivalence of f (from the name)
English
Let $f$ be a linear equivalence of $A$ and $B$. Then the congruence linear equivalence of $f$ is a linear equivalence of $\mathrm{WithConv}$ applied to $A$ and $\mathrm{WithConv}$ applied to $B$ defined as the composition of the linear equivalence of $R$ and $A$ and the composition of $f$ and the inverse of the linear equivalence of $R$ and $B$.
WithConv.equivdefMathlib.Algebra.WithConv, function or constant
Wording
the equivalence of A (from the name)
English
Let $A$ be a set. Then the equivalence of $A$ is an element of $\EquivMACRoAE {\mathrm{WithConv} (A)}{A}$.
WithConv.linearEquivdefMathlib.Algebra.WithConv, function or constant
Wording
the linear equivalence of R and A (from the name)
English
Let $R$ and $A$ be sets. Then the linear equivalence of $R$ and $A$ is a linear equivalence of $\mathrm{WithConv}$ applied to $A$ and $A$.
WithConv.ofConvdefMathlib.Algebra.WithConv, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\mathrm{WithConv}$ applied to $A$. Then $\operatorname{ofConv}$ applied to $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

‹ previous next ›