AddMonoidAlgebrastructureMathlib.Algebra.MonoidAlgebra.Defs, typeWording
additive monoid algebra of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the additive monoid algebras of $R$ and $M$ are a basic type.
AddMonoidAlgebra.coeffdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the coefficient of self (from the name)
English
Let $\mathrm{self}$ be an additive monoid algebra of $R$ and $M$. Then the coefficient of $\mathrm{self}$ is an element of $\FinsuppMACRoQ {M}{R}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AddMonoidAlgebra.coeffAddEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the coefficient additive equivalence (from the name)
English
The coefficient additive equivalence is an additive equivalence of the set of additive monoid algebras of $R$ and $M$ and $\FinsuppMACRoQ {M}{R}$ defined as the additive equivalence of the coefficient equivalence.
AddMonoidAlgebra.coeffEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the coefficient equivalence (from the name)
English
The coefficient equivalence is an equivalence from the set of additive monoid algebras of $R$ and $M$ to $\FinsuppMACRoQ {M}{R}$.
AddMonoidAlgebra.curryAddEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the curry additive equivalence (from the name)
English
The curry additive equivalence is an additive equivalence of the set of additive monoid algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of additive monoid algebras of the set of additive monoid algebras of $R$ and $N$ and $M$ defined as the composition of the coefficient additive equivalence and the composition of the curry additive equivalence and the composition of the additive equivalence of the inverse of the coefficient additive equivalence and the inverse of the coefficient additive equivalence.
AddMonoidAlgebra.curryRingEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the curry ring isomorphism (from the name)
English
The curry ring isomorphism is a ring isomorphism of the set of additive monoid algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of additive monoid algebras of the set of additive monoid algebras of $R$ and $N$ and $M$.
AddMonoidAlgebra.erasedefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $m$ be an element of $M$. Let $x_{1}$ be an additive monoid algebra of $R$ and $M$. Then $\operatorname{erase}$ applied to $m$ and $x_{1}$ is an additive monoid algebra of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $\operatorname{erase}$ applied to $m$ and the coefficient of $x_{1}$.
AddMonoidAlgebra.mul'defMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the product of x2 and y (from the name)
English
Let $x_{2}$ and $y$ be additive monoid algebras of $R$ and $M$. Then the product of $x_{2}$ and $y$ is an additive monoid algebra of $R$ and $M$ defined as the sum of the coefficient of $x_{2}$ and the function that maps $x_{3}$ and $x_{4}$ to the sum of the coefficient of $y$ and the function that maps $x_{5}$ and $x_{6}$ to $\operatorname{single}$ applied to $x_{3} + x_{5}$ and $x_{4} \times x_{6}$.
AddMonoidAlgebra.ofdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{of}$ applied to $R$ and $M$ is a monoid homomorphism of the set of multiplicatives of $M$ and the set of additive monoid algebras of $R$ and $M$.
AddMonoidAlgebra.of'defMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $R$ and $M$ be sets. Let $x_{1}$ be an element of $M$. Then $\operatorname{of'}$ applied to $R$, $M$ and $x_{1}$ is an additive monoid algebra of $R$ and $M$ defined as $\operatorname{single}$ applied to $x_{1}$ and $1$.
AddMonoidAlgebra.ofMagmadefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the embedding of R and M (from the docstring)
English
Let $R$ and $M$ be sets. Then the embedding of $R$ and $M$ is a multiplicative homomorphism of the set of multiplicatives of $M$ and the set of additive monoid algebras of $R$ and $M$.
AddMonoidAlgebra.singledefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $m$ be an element of $M$. Let $r$ be an element of $R$. Then $\operatorname{single}$ applied to $m$ and $r$ is an additive monoid algebra of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $\FinsuppsingleMACRoS {m}{r}$.
AddMonoidAlgebra.singleAddHomdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the single additive homomorphism of m (from the name)
English
Let $m$ be an element of $M$. Then the single additive homomorphism of $m$ is an additive monoid homomorphism of $R$ and the set of additive monoid algebras of $R$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $m$ and $\mathrm{AddMonoidAlgebra\_\_single\_zero}$ applied to $m$ and $\mathrm{AddMonoidAlgebra\_\_single\_add}$ applied to $m$.
AddMonoidAlgebra.singleHomdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the single homomorphism (from the name)
English
The single homomorphism is a monoid homomorphism of $\mathrm{Prod}$ applied to $R$ and the set of multiplicatives of $M$ and the set of additive monoid algebras of $R$ and $M$.
AddMonoidAlgebra.singleZeroRingHomdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the single zero ring homomorphism (from the name)
English
The single zero ring homomorphism is a ring homomorphism of $R$ and the set of additive monoid algebras of $R$ and $M$.
AddMonoidAlgebra.uniqueRingEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the unique ring isomorphism of M (from the name)
English
Let $M$ be a set. Then the unique ring isomorphism of $M$ is a ring isomorphism of the set of additive monoid algebras of $R$ and $M$ and $R$.
AddMonoidAlgebra.updatedefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $m$ be an element of $M$. Let $r$ be an element of $R$. Let $x_{1}$ be an additive monoid algebra of $R$ and $M$. Then $\operatorname{update}$ applied to $m$, $r$ and $x_{1}$ is an additive monoid algebra of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $\operatorname{update}$ applied to the coefficient of $x_{1}$, $m$ and $r$.
MonoidAlgebrastructureMathlib.Algebra.MonoidAlgebra.Defs, typeWording
monoid algebra of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the monoid algebras of $R$ and $M$ are a basic type.
MonoidAlgebra.coeffdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the coefficient of self (from the name)
English
Let $\mathrm{self}$ be a monoid algebra of $R$ and $M$. Then the coefficient of $\mathrm{self}$ is an element of $\FinsuppMACRoQ {M}{R}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
MonoidAlgebra.coeffAddEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the coefficient additive equivalence (from the name)
English
The coefficient additive equivalence is an additive equivalence of the set of monoid algebras of $R$ and $M$ and $\FinsuppMACRoQ {M}{R}$ defined as the additive equivalence of the coefficient equivalence.
MonoidAlgebra.coeffEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the coefficient equivalence (from the name)
English
The coefficient equivalence is an equivalence from the set of monoid algebras of $R$ and $M$ to $\FinsuppMACRoQ {M}{R}$.
MonoidAlgebra.curryAddEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the curry additive equivalence (from the name)
English
The curry additive equivalence is an additive equivalence of the set of monoid algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of monoid algebras of the set of monoid algebras of $R$ and $N$ and $M$ defined as the composition of the coefficient additive equivalence and the composition of the curry additive equivalence and the composition of the additive equivalence of the inverse of the coefficient additive equivalence and the inverse of the coefficient additive equivalence.
MonoidAlgebra.curryRingEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the curry ring isomorphism (from the name)
English
The curry ring isomorphism is a ring isomorphism of the set of monoid algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of monoid algebras of the set of monoid algebras of $R$ and $N$ and $M$.
MonoidAlgebra.erasedefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $m$ be an element of $M$. Let $x_{1}$ be a monoid algebra of $R$ and $M$. Then $\operatorname{erase}$ applied to $m$ and $x_{1}$ is a monoid algebra of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $\operatorname{erase}$ applied to $m$ and the coefficient of $x_{1}$.
MonoidAlgebra.mul'defMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the product of x2 and y (from the name)
English
Let $x_{2}$ and $y$ be monoid algebras of $R$ and $M$. Then the product of $x_{2}$ and $y$ is a monoid algebra of $R$ and $M$ defined as the sum of the coefficient of $x_{2}$ and the function that maps $x_{3}$ and $x_{4}$ to the sum of the coefficient of $y$ and the function that maps $x_{5}$ and $x_{6}$ to $\operatorname{single}$ applied to $x_{3} \times x_{5}$ and $x_{4} \times x_{6}$.
MonoidAlgebra.ofdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{of}$ applied to $R$ and $M$ is a monoid homomorphism of $M$ and the set of monoid algebras of $R$ and $M$.
MonoidAlgebra.ofMagmadefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the embedding of R and M (from the docstring)
English
Let $R$ and $M$ be sets. Then the embedding of $R$ and $M$ is a multiplicative homomorphism of $M$ and the set of monoid algebras of $R$ and $M$.
MonoidAlgebra.singledefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $m$ be an element of $M$. Let $r$ be an element of $R$. Then $\operatorname{single}$ applied to $m$ and $r$ is a monoid algebra of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $\FinsuppsingleMACRoS {m}{r}$.
MonoidAlgebra.singleAddHomdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the single additive homomorphism of m (from the name)
English
Let $m$ be an element of $M$. Then the single additive homomorphism of $m$ is an additive monoid homomorphism of $R$ and the set of monoid algebras of $R$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $m$ and $\mathrm{MonoidAlgebra\_\_single\_zero}$ applied to $m$ and $\mathrm{MonoidAlgebra\_\_single\_add}$ applied to $m$.
MonoidAlgebra.singleHomdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the single homomorphism (from the name)
English
The single homomorphism is a monoid homomorphism of $\mathrm{Prod}$ applied to $R$ and $M$ and the set of monoid algebras of $R$ and $M$.
MonoidAlgebra.singleOneRingHomdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the single one ring homomorphism (from the name)
English
The single one ring homomorphism is a ring homomorphism of $R$ and the set of monoid algebras of $R$ and $M$.
MonoidAlgebra.uniqueRingEquivdefMathlib.Algebra.MonoidAlgebra.Defs, function or constantWording
the unique ring isomorphism of M (from the name)
English
Let $M$ be a set. Then the unique ring isomorphism of $M$ is a ring isomorphism of the set of monoid algebras of $R$ and $M$ and $R$.
MonoidAlgebra.updatedefMathlib.Algebra.MonoidAlgebra.Defs, function or constantEnglish
Let $m$ be an element of $M$. Let $r$ be an element of $R$. Let $x_{1}$ be a monoid algebra of $R$ and $M$. Then $\operatorname{update}$ applied to $m$, $r$ and $x_{1}$ is a monoid algebra of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $\operatorname{update}$ applied to the coefficient of $x_{1}$, $m$ and $r$.
AddMonoidAlgebra.MonicdefMathlib.Algebra.MonoidAlgebra.Degree, predicateEnglish
Let $D$ be a function from elements of $A$ to elements of $B$. Let $f$ be an additive monoid algebra of $R$ and $A$. Then $\operatorname{Monic}$ holds for $D$ and $f$, if the leading coefficient of $D$ and $f$ is equal to $1$.
AddMonoidAlgebra.infDegreedefMathlib.Algebra.MonoidAlgebra.Degree, function or constantWording
the infimum degree of D and f (from the name)
English
Let $D$ be a function from elements of $A$ to elements of $T$. Let $f$ be an additive monoid algebra of $R$ and $A$. Then the infimum degree of $D$ and $f$ is an element of $T$ defined as the infimum of the support of the coefficient of $f$ and $D$.
AddMonoidAlgebra.leadingCoeffdefMathlib.Algebra.MonoidAlgebra.Degree, function or constantWording
the leading coefficient of D and f (from the name)
English
Let $D$ be a function from elements of $A$ to elements of $B$. Let $f$ be an additive monoid algebra of $R$ and $A$. Then the leading coefficient of $D$ and $f$ is an element of $R$ defined as $\operatorname{coeff}$ applied to $f$ and the inverse of $D$ and the supremum degree of $D$ and $f$.
AddMonoidAlgebra.supDegreedefMathlib.Algebra.MonoidAlgebra.Degree, function or constantWording
the supremum degree of D and f (from the name)
English
Let $D$ be a function from elements of $A$ to elements of $B$. Let $f$ be an additive monoid algebra of $R$ and $A$. Then the supremum degree of $D$ and $f$ is an element of $B$ defined as the supremum of the support of the coefficient of $f$ and $D$.
AddMonoidAlgebra.divOfdefMathlib.Algebra.MonoidAlgebra.Division, function or constantWording
the quotient of x2 and g (from the name)
English
Let $x_{2}$ be an additive monoid algebra of $k$ and $G$. Let $g$ be an element of $G$. Then the quotient of $x_{2}$ and $g$ is an additive monoid algebra of $k$ and $G$.
AddMonoidAlgebra.divOfHomdefMathlib.Algebra.MonoidAlgebra.Division, function or constantWording
the quotient (from the name)
English
The quotient is a monoid homomorphism of the set of multiplicatives of $G$ and the set of ends of the set of additive monoid algebras of $k$ and $G$.
AddMonoidAlgebra.modOfdefMathlib.Algebra.MonoidAlgebra.Division, function or constantEnglish
Let $x_{2}$ be an additive monoid algebra of $k$ and $G$. Let $g$ be an element of $G$. Then $\operatorname{modOf}$ applied to $x_{2}$ and $g$ is an additive monoid algebra of $k$ and $G$ defined as $\operatorname{ofCoeff}$ applied to the filter of the function that maps $x_{3}$ to the proposition that it is not the case that there exists an element $x_{4}$ of $G$, such that $\EqtMACRoH {x_{3}}{g + x_{4}}$ and the coefficient of $x_{2}$.
AddMonoidAlgebra.gradedefMathlib.Algebra.MonoidAlgebra.Grading, function or constantEnglish
Let $R$ be a set. Let $m$ be an element of $M$. Then $\operatorname{grade}$ applied to $R$ and $m$ is a submodule of $R$ and the set of additive monoid algebras of $R$ and $M$ defined as $\operatorname{gradeBy}$ applied to $R$, $\mathrm{id}$ and $m$.
AddMonoidAlgebra.gradeBydefMathlib.Algebra.MonoidAlgebra.Grading, function or constantEnglish
Let $R$ be a set. Let $f$ be a function from elements of $M$ to elements of $x$. Let $i$ be an element of $x$. Then $\operatorname{gradeBy}$ applied to $R$, $f$ and $i$ is a submodule of $R$ and the set of additive monoid algebras of $R$ and $M$.
AddMonoidAlgebra.liftNCdefMathlib.Algebra.MonoidAlgebra.Lift, function or constantEnglish
Let $f$ be an additive monoid homomorphism of $k$ and $R$. Let $g$ be a function from multiplicatives of $G$ to elements of $R$. Then $\operatorname{liftNC}$ applied to $f$ and $g$ is an additive monoid homomorphism of the set of additive monoid algebras of $k$ and $G$ 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 $\operatorname{ofAdd}$ applied to $x_{3}$ and $f$ and the additive monoid homomorphism of the coefficient additive equivalence.
AddMonoidAlgebra.liftNCRingHomdefMathlib.Algebra.MonoidAlgebra.Lift, function or constantEnglish
Let $f$ be a ring homomorphism of $k$ and $R$. Let $g$ be a monoid homomorphism of the set of multiplicatives of $G$ and $R$ such that for all elements $x_{3}$ of $k$, for all multiplicatives $y$ of $G$, $\mathrm{Commute}$ holds for $f$ applied to $x_{3}$ and $g$ applied to $y$. Then $\operatorname{liftNCRingHom}$ applied to $f$, $g$ and $\mathrm{h\_comm}$ is a ring homomorphism of the set of additive monoid algebras of $k$ and $G$ and $R$.
MonoidAlgebra.liftNCdefMathlib.Algebra.MonoidAlgebra.Lift, function or constantEnglish
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 monoid algebras of $k$ and $G$ 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.
MonoidAlgebra.liftNCRingHomdefMathlib.Algebra.MonoidAlgebra.Lift, function or constantEnglish
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_{3}$ of $k$, for all elements $y$ of $G$, $\mathrm{Commute}$ holds for $f$ applied to $x_{3}$ and $g$ applied to $y$. Then $\operatorname{liftNCRingHom}$ applied to $f$, $g$ and $\mathrm{h\_comm}$ is a ring homomorphism of the set of monoid algebras of $k$ and $G$ and $R$.
AddMonoidAlgebra.comapDomaindefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the preimage domain of f and x1 (from the name)
English
Let $f$ be an injective function from elements of $M$ to elements of $N$. Let $x_{1}$ be an additive monoid algebra of $R$ and $N$. Then the preimage domain of $f$ and $x_{1}$ is an additive monoid algebra of $R$ and $M$.
AddMonoidAlgebra.comapDomainAddMonoidHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the preimage domain additive monoid homomorphism of f and hf (from the name)
English
Let $f$ be an injective function from elements of $M$ to elements of $N$. Then the preimage domain additive monoid homomorphism of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of additive monoid algebras of $R$ and $N$ and the set of additive monoid algebras of $R$ and $M$.
AddMonoidAlgebra.commRingEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the commutative ring isomorphism (from the name)
English
The commutative ring isomorphism is a ring isomorphism of the set of additive monoid algebras of the set of additive monoid algebras of $R$ and $M$ and $N$ and the set of additive monoid algebras of the set of additive monoid algebras of $R$ and $N$ and $M$ defined as the composition of the inverse of the curry ring isomorphism and the composition of the map domain ring isomorphism of $R$ and $\operatorname{prodComm}$ and the curry ring isomorphism.
AddMonoidAlgebra.mapdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map of f and x2 (from the name)
English
Let $f$ be an additive monoid homomorphism of $R$ and $S$. Let $x_{2}$ be an additive monoid algebra of $R$ and $M$. Then the map of $f$ and $x_{2}$ is an additive monoid algebra of $S$ and $M$.
AddMonoidAlgebra.mapAddEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map additive equivalence of M and e (from the name)
English
Let $M$ be a set. Let $e$ be an additive equivalence of $R$ and $S$. Then the map additive equivalence of $M$ and $e$ is an additive equivalence of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $S$ and $M$.
AddMonoidAlgebra.mapDomaindefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain of f and x1 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$. Let $x_{1}$ be an additive monoid algebra of $R$ and $M$. Then the map domain of $f$ and $x_{1}$ is an additive monoid algebra of $R$ and $N$ defined as $\operatorname{ofCoeff}$ applied to the map domain of $f$ and the coefficient of $x_{1}$.
AddMonoidAlgebra.mapDomainAddEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain additive equivalence of R and e (from the name)
English
Let $R$ be a set. Let $e$ be an equivalence from $M$ to $N$. Then the map domain additive equivalence of $R$ and $e$ is an additive equivalence of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $N$.
AddMonoidAlgebra.mapDomainNonUnitalRingHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain non unital ring homomorphism of R and f (from the name)
English
Let $R$ be a set. Let $f$ be an additive homomorphism of $M$ and $N$. Then the map domain non unital ring homomorphism of $R$ and $f$ is a non unital ring homomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $N$.
AddMonoidAlgebra.mapDomainRingEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain ring isomorphism of R and e (from the name)
English
Let $R$ be a set. Let $e$ be an additive equivalence of $M$ and $N$. Then the map domain ring isomorphism of $R$ and $e$ is a ring isomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $N$.
AddMonoidAlgebra.mapDomainRingHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain ring homomorphism of R and f (from the name)
English
Let $R$ be a set. Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then the map domain ring homomorphism of $R$ and $f$ is a ring homomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $N$.
AddMonoidAlgebra.mapRingEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map ring isomorphism of M and e (from the name)
English
Let $M$ be a set. Let $e$ be a ring isomorphism of $R$ and $S$. Then the map ring isomorphism of $M$ and $e$ is a ring isomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $S$ and $M$.
AddMonoidAlgebra.mapRingHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map ring homomorphism of M and f (from the name)
English
Let $M$ be a set. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map ring homomorphism of $M$ and $f$ is a ring homomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $S$ and $M$.
AddMonoidAlgebra.toMultiplicativedefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the multiplicative of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the multiplicative of $R$ and $M$ is a ring isomorphism of the set of additive monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and the set of multiplicatives of $M$.
MonoidAlgebra.comapDomaindefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the preimage domain of f and x1 (from the name)
English
Let $f$ be an injective function from elements of $M$ to elements of $N$. Let $x_{1}$ be a monoid algebra of $R$ and $N$. Then the preimage domain of $f$ and $x_{1}$ is a monoid algebra of $R$ and $M$.
MonoidAlgebra.comapDomainAddMonoidHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the preimage domain additive monoid homomorphism of f and hf (from the name)
English
Let $f$ be an injective function from elements of $M$ to elements of $N$. Then the preimage domain additive monoid homomorphism of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of monoid algebras of $R$ and $N$ and the set of monoid algebras of $R$ and $M$.
MonoidAlgebra.commRingEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the commutative ring isomorphism (from the name)
English
The commutative ring isomorphism is a ring isomorphism of the set of monoid algebras of the set of monoid algebras of $R$ and $M$ and $N$ and the set of monoid algebras of the set of monoid algebras of $R$ and $N$ and $M$ defined as the composition of the inverse of the curry ring isomorphism and the composition of the map domain ring isomorphism of $R$ and $\operatorname{prodComm}$ and the curry ring isomorphism.
MonoidAlgebra.mapdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map of f and x2 (from the name)
English
Let $f$ be an additive monoid homomorphism of $R$ and $S$. Let $x_{2}$ be a monoid algebra of $R$ and $M$. Then the map of $f$ and $x_{2}$ is a monoid algebra of $S$ and $M$.
MonoidAlgebra.mapAddEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map additive equivalence of M and e (from the name)
English
Let $M$ be a set. Let $e$ be an additive equivalence of $R$ and $S$. Then the map additive equivalence of $M$ and $e$ is an additive equivalence of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $S$ and $M$.
MonoidAlgebra.mapDomaindefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain of f and x1 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$. Let $x_{1}$ be a monoid algebra of $R$ and $M$. Then the map domain of $f$ and $x_{1}$ is a monoid algebra of $R$ and $N$ defined as $\operatorname{ofCoeff}$ applied to the map domain of $f$ and the coefficient of $x_{1}$.
MonoidAlgebra.mapDomainAddEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain additive equivalence of R and e (from the name)
English
Let $R$ be a set. Let $e$ be an equivalence from $M$ to $N$. Then the map domain additive equivalence of $R$ and $e$ is an additive equivalence of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and $N$.
MonoidAlgebra.mapDomainNonUnitalRingHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain non unital ring homomorphism of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a multiplicative homomorphism of $M$ and $N$. Then the map domain non unital ring homomorphism of $R$ and $f$ is a non unital ring homomorphism of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and $N$.
MonoidAlgebra.mapDomainRingEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain ring isomorphism of R and e (from the name)
English
Let $R$ be a set. Let $e$ be a multiplicative equivalence of $M$ and $N$. Then the map domain ring isomorphism of $R$ and $e$ is a ring isomorphism of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and $N$.
MonoidAlgebra.mapDomainRingHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map domain ring homomorphism of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a monoid homomorphism of $M$ and $N$. Then the map domain ring homomorphism of $R$ and $f$ is a ring homomorphism of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $R$ and $N$.
MonoidAlgebra.mapRingEquivdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map ring isomorphism of M and e (from the name)
English
Let $M$ be a set. Let $e$ be a ring isomorphism of $R$ and $S$. Then the map ring isomorphism of $M$ and $e$ is a ring isomorphism of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $S$ and $M$.
MonoidAlgebra.mapRingHomdefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantWording
the map ring homomorphism of M and f (from the name)
English
Let $M$ be a set. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map ring homomorphism of $M$ and $f$ is a ring homomorphism of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of $S$ and $M$.
MonoidAlgebra.toAdditivedefMathlib.Algebra.MonoidAlgebra.MapDomain, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{toAdditive}$ applied to $R$ and $M$ is a ring isomorphism of the set of monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $\mathrm{Additive}$ applied to $M$.
AddMonoidAlgebra.basisdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the standard basis of R and k (from the docstring)
English
Let $R$ and $k$ be sets. Then the standard basis of $R$ and $k$ is a basis of $k$ and the set of additive monoid algebras of $k$ and $R$ defined as $\operatorname{ofRepr}$ applied to the coefficient linear equivalence of $k$.
AddMonoidAlgebra.coeffLinearEquivdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the coefficient linear equivalence of R (from the name)
English
Let $R$ be a set. Then the coefficient linear equivalence of $R$ is a linear equivalence of the set of additive monoid algebras of $S$ and $M$ and $\FinsuppMACRoQ {M}{S}$ defined as the linear equivalence of $R$ and the coefficient additive equivalence.
AddMonoidAlgebra.lsingledefMathlib.Algebra.MonoidAlgebra.Module, function or constantEnglish
Let $a$ be an element of $M$. Then $\operatorname{lsingle}$ applied to $a$ is a linear map of $S$ and the set of additive monoid algebras of $S$ and $M$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $R$ and $\operatorname{lsingle}$ applied to $a$.
AddMonoidAlgebra.mapDomainLinearEquivdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the map domain linear equivalence of e (from the name)
English
Let $R$ and $S$ be sets. Let $e$ be an equivalence from $M$ to $N$. Then the map domain linear equivalence of $e$ is a linear equivalence of the set of additive monoid algebras of $S$ and $M$ and the set of additive monoid algebras of $S$ and $N$ defined as the composition of the coefficient linear equivalence of $R$ and the composition of the domain congruence of $e$ and the inverse of the coefficient linear equivalence of $R$.
AddMonoidAlgebra.mapDomainLinearMapdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the map domain linear map of f (from the name)
English
Let $R$ and $S$ be sets. Let $f$ be a function from elements of $M$ to elements of $N$. Then the map domain linear map of $f$ is a linear map of the set of additive monoid algebras of $S$ and $M$ and the set of additive monoid algebras of $S$ and $N$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $R$ and the composition of $\operatorname{lmapDomain}$ applied to $S$, $R$ and $f$ and $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$.
AddMonoidAlgebra.singleDistribMulActionHomdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the single distributive multiplicative action homomorphism of a (from the name)
English
Let $a$ be an element of $M$. Then the single distributive multiplicative action homomorphism of $a$ is a distributive multiplicative action homomorphism of $S$ and the set of additive monoid algebras of $S$ and $M$.
AddMonoidAlgebra.supporteddefMathlib.Algebra.MonoidAlgebra.Module, function or constantEnglish
Let $R$ and $S$ be sets. Let $s$ be an element of $\wp M$. Then $\operatorname{supported}$ applied to $R$, $S$ and $s$ is a submodule of $R$ and the set of additive monoid algebras of $S$ and $M$ defined as the preimage of $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$ and $\operatorname{supported}$ applied to $S$, $R$ and $s$.
AddMonoidAlgebra.supportedEquivFinsuppdefMathlib.Algebra.MonoidAlgebra.Module, function or constantEnglish
Let $s$ be an element of $\wp M$. Then $\operatorname{supportedEquivFinsupp}$ applied to $s$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{supported} (R , S , s)}{x_{3}})}$ and the set of finitely supported functions from the set of elements of $s$ to $S$.
AddMonoidAlgebra.uniqueLinearEquivdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the unique linear equivalence of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the unique linear equivalence of $R$ and $M$ is a linear equivalence of the set of additive monoid algebras of $S$ and $M$ and $S$.
MonoidAlgebra.basisdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the standard basis of R and k (from the docstring)
English
Let $R$ and $k$ be sets. Then the standard basis of $R$ and $k$ is a basis of $k$ and the set of monoid algebras of $k$ and $R$ defined as $\operatorname{ofRepr}$ applied to the coefficient linear equivalence of $k$.
MonoidAlgebra.coeffLinearEquivdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the coefficient linear equivalence of R (from the name)
English
Let $R$ be a set. Then the coefficient linear equivalence of $R$ is a linear equivalence of the set of monoid algebras of $S$ and $M$ and $\FinsuppMACRoQ {M}{S}$ defined as the linear equivalence of $R$ and the coefficient additive equivalence.
MonoidAlgebra.lsingledefMathlib.Algebra.MonoidAlgebra.Module, function or constantEnglish
Let $a$ be an element of $M$. Then $\operatorname{lsingle}$ applied to $a$ is a linear map of $S$ and the set of monoid algebras of $S$ and $M$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $R$ and $\operatorname{lsingle}$ applied to $a$.
MonoidAlgebra.mapDomainLinearEquivdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the map domain linear equivalence of e (from the name)
English
Let $R$ and $S$ be sets. Let $e$ be an equivalence from $M$ to $N$. Then the map domain linear equivalence of $e$ is a linear equivalence of the set of monoid algebras of $S$ and $M$ and the set of monoid algebras of $S$ and $N$ defined as the composition of the coefficient linear equivalence of $R$ and the composition of the domain congruence of $e$ and the inverse of the coefficient linear equivalence of $R$.
MonoidAlgebra.mapDomainLinearMapdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the map domain linear map of f (from the name)
English
Let $R$ and $S$ be sets. Let $f$ be a function from elements of $M$ to elements of $N$. Then the map domain linear map of $f$ is a linear map of the set of monoid algebras of $S$ and $M$ and the set of monoid algebras of $S$ and $N$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $R$ and the composition of $\operatorname{lmapDomain}$ applied to $S$, $R$ and $f$ and $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$.
MonoidAlgebra.singleDistribMulActionHomdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the single distributive multiplicative action homomorphism of a (from the name)
English
Let $a$ be an element of $M$. Then the single distributive multiplicative action homomorphism of $a$ is a distributive multiplicative action homomorphism of $S$ and the set of monoid algebras of $S$ and $M$.
MonoidAlgebra.submoduleOfSMulMemdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the submodule of W and h1 (from the name)
English
Let $W$ be a submodule of $S$ and $V$ such that for all elements $g$ of $M$, for all elements $v$ of $V$, if $v$ is an element of $W$, then $\HSMulhSMulMACRoAL {\operatorname{of} (S , M , g)}{v}$ is an element of $W$. Then the submodule of $W$ and $h_{1}$ is a submodule of the set of monoid algebras of $S$ and $M$ and $V$.
MonoidAlgebra.supporteddefMathlib.Algebra.MonoidAlgebra.Module, function or constantEnglish
Let $R$ and $S$ be sets. Let $s$ be an element of $\wp M$. Then $\operatorname{supported}$ applied to $R$, $S$ and $s$ is a submodule of $R$ and the set of monoid algebras of $S$ and $M$ defined as the preimage of $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$ and $\operatorname{supported}$ applied to $S$, $R$ and $s$.
MonoidAlgebra.supportedEquivFinsuppdefMathlib.Algebra.MonoidAlgebra.Module, function or constantEnglish
Let $s$ be an element of $\wp M$. Then $\operatorname{supportedEquivFinsupp}$ applied to $s$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{supported} (R , S , s)}{x_{3}})}$ and the set of finitely supported functions from the set of elements of $s$ to $S$.
MonoidAlgebra.uniqueLinearEquivdefMathlib.Algebra.MonoidAlgebra.Module, function or constantWording
the unique linear equivalence of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the unique linear equivalence of $R$ and $M$ is a linear equivalence of the set of monoid algebras of $S$ and $M$ and $S$.
AddMonoidAlgebra.opRingEquivdefMathlib.Algebra.MonoidAlgebra.Opposite, function or constantWording
the opposite (from the docstring)
English
The opposite is a ring isomorphism of the set of multiplicative opposites of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of the set of multiplicative opposites of $R$ and the set of additive opposites of $M$.
MonoidAlgebra.opRingEquivdefMathlib.Algebra.MonoidAlgebra.Opposite, function or constantWording
the opposite (from the docstring)
English
The opposite is a ring isomorphism of the set of multiplicative opposites of the set of monoid algebras of $R$ and $M$ and the set of monoid algebras of the set of multiplicative opposites of $R$ and the set of multiplicative opposites of $M$.
AddMonoidAlgebra.toDirectSumdefMathlib.Algebra.MonoidAlgebra.ToDirectSum, function or constantWording
the direct sum of f (from the name)
English
Let $f$ be an additive monoid algebra of $M$ and $x$. Then the direct sum of $f$ is a direct sum of $x$ and the function that maps $x_{2}$ to $M$ defined as the finitely supported function of the coefficient of $f$.
DirectSum.toAddMonoidAlgebradefMathlib.Algebra.MonoidAlgebra.ToDirectSum, function or constantWording
the additive monoid algebra of f (from the name)
English
Let $f$ be a direct sum of $x$ and the function that maps $x_{4}$ to $M$. Then the additive monoid algebra of $f$ is an additive monoid algebra of $M$ and $x$ defined as $\operatorname{ofCoeff}$ applied to the finitely supported function of $f$.
addMonoidAlgebraAddEquivDirectSumdefMathlib.Algebra.MonoidAlgebra.ToDirectSum, function or constantWording
the additive monoid algebra additive equivalence direct sum (from the name)
English
The additive monoid algebra additive equivalence direct sum is an additive equivalence of the set of additive monoid algebras of $M$ and $x$ and the set of direct sums of $x$ and the function that maps $x_{4}$ to $M$ defined as $\operatorname{mk}$ applied to the additive monoid algebra equivalence direct sum and $\mathrm{AddMonoidAlgebra\_\_toDirectSum\_add}$.
addMonoidAlgebraAlgEquivDirectSumdefMathlib.Algebra.MonoidAlgebra.ToDirectSum, function or constantWording
the additive monoid algebra algebra isomorphism direct sum (from the name)
English
The additive monoid algebra algebra isomorphism direct sum is an algebra isomorphism of the set of additive monoid algebras of $A$ and $x$ and the set of direct sums of $x$ and the function that maps $x_{7}$ to $A$.
addMonoidAlgebraEquivDirectSumdefMathlib.Algebra.MonoidAlgebra.ToDirectSum, function or constantWording
the additive monoid algebra equivalence direct sum (from the name)
English
The additive monoid algebra equivalence direct sum is an equivalence from the set of additive monoid algebras of $M$ and $x$ to the set of direct sums of $x$ and the function that maps $x_{4}$ to $M$.
addMonoidAlgebraRingEquivDirectSumdefMathlib.Algebra.MonoidAlgebra.ToDirectSum, function or constantWording
the additive monoid algebra ring isomorphism direct sum (from the name)
English
The additive monoid algebra ring isomorphism direct sum is a ring isomorphism of the set of additive monoid algebras of $M$ and $x$ and the set of direct sums of $x$ and the function that maps $x_{5}$ to $M$.
MvPolynomialdefMathlib.Algebra.MvPolynomial.Basic, typeWording
multivariate polynomial of x and R (from the name)
English
Let $x$ and $R$ be sets. Then a multivariate polynomial of $x$ and $R$ is an element of the function that maps $x$ and $R$ to the set of additive monoid algebras of $R$ and $\FinsuppMACRoQ {x}{\Natural}$.
MvPolynomial.CdefMathlib.Algebra.MvPolynomial.Basic, function or constantEnglish
$\operatorname{C}$ is a ring homomorphism of $R$ and the set of multivariate polynomials of $x$ and $R$.
MvPolynomial.XdefMathlib.Algebra.MvPolynomial.Basic, function or constantEnglish
Let $n$ be an element of $x$. Then $\operatorname{X}$ applied to $n$ is a multivariate polynomial of $x$ and $R$ defined as $\operatorname{monomial}$ applied to $\FinsuppsingleMACRoS {n}{1}$ and $1$.
MvPolynomial.coeffAddMonoidHomdefMathlib.Algebra.MvPolynomial.Basic, function or constantWording
the coefficient additive monoid homomorphism of m (from the name)
English
Let $m$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then the coefficient additive monoid homomorphism of $m$ is an additive monoid homomorphism of the set of multivariate polynomials of $x$ and $R$ and $R$.
MvPolynomial.coeffsdefMathlib.Algebra.MvPolynomial.Basic, function or constantEnglish
Let $p$ be a multivariate polynomial of $x$ and $R$. Then $\operatorname{coeffs}$ applied to $p$ is a finite set of $R$ defined as the forward image of the support of $p$ under $\operatorname{coe}$ applied to the coefficient of $p$.
MvPolynomial.coeffsIndefMathlib.Algebra.MvPolynomial.Basic, function or constantEnglish
Let $x$ be a set. Let $M$ be a submodule of $R$ and $S$. Then $\operatorname{coeffsIn}$ applied to $x$ and $M$ is a submodule of $R$ and the set of multivariate polynomials of $x$ and $S$.
MvPolynomial.constantCoeffdefMathlib.Algebra.MvPolynomial.Basic, function or constantWording
the constant coefficient (from the name)
English
The constant coefficient is a ring homomorphism of the set of multivariate polynomials of $x$ and $R$ and $R$.
MvPolynomial.lcoeffdefMathlib.Algebra.MvPolynomial.Basic, function or constantEnglish
Let $R$ be a set. Let $m$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{lcoeff}$ applied to $R$ and $m$ is a linear map of the set of multivariate polynomials of $x$ and $R$ and $R$.
MvPolynomial.monomialdefMathlib.Algebra.MvPolynomial.Basic, function or constantWording
the monomial with coefficient of s (from the docstring)
English
Let $s$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then the monomial with coefficient of $s$ is a linear map of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{lsingle}$ applied to $s$.
MvPolynomial.monomialOneHomdefMathlib.Algebra.MvPolynomial.Basic, function or constantWording
the monomial one homomorphism of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the monomial one homomorphism of $R$ and $x$ is a monoid homomorphism of the set of multiplicatives of $\FinsuppMACRoQ {x}{\Natural}$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{of}$ applied to $R$ and $\FinsuppMACRoQ {x}{\Natural}$.
MvPolynomial.supportdefMathlib.Algebra.MvPolynomial.Basic, function or constantWording
the support of p (from the name)
English
Let $p$ be a multivariate polynomial of $x$ and $R$. Then the support of $p$ is a finite set of $\FinsuppMACRoQ {x}{\Natural}$ defined as the support of the coefficient of $p$.
MvPolynomial.comapdefMathlib.Algebra.MvPolynomial.Comap, function or constantWording
the preimage of x3 and x4 (from the name)
English
Let $f$ be an algebra homomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $R$. Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $R$. Let $x_{4}$ be an element of $x$. Then the preimage of $x_{3}$ and $x_{4}$ is an element of $R$ defined as $\operatorname{aeval}$ applied to $x_{3}$ and $f$ applied to $\operatorname{X}$ applied to $x_{4}$.
MvPolynomial.comapEquivdefMathlib.Algebra.MvPolynomial.Comap, function or constantWording
the preimage equivalence of f (from the name)
English
Let $f$ be an algebra isomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $R$. Then the preimage equivalence of $f$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x_{1})\rightarrow R)}{(\mathrm{Elem} (x)\rightarrow R)}$.
MvPolynomial.homEquivdefMathlib.Algebra.MvPolynomial.CommRing, function or constantWording
the homomorphism equivalence (from the name)
English
The homomorphism equivalence is an equivalence from the set of ring homomorphisms of the set of multivariate polynomials of $x$ and $\Integer$ and $S$ to the set of functions from elements of $x$ to elements of $S$.
MvPolynomial.ACounitdefMathlib.Algebra.MvPolynomial.Counit, function or constantWording
the counit of A and B (from the name)
English
Let $A$ and $B$ be sets. Then the counit of $A$ and $B$ is an algebra homomorphism of the set of multivariate polynomials of $B$ and $A$ and $B$ defined as the algebra evaluation of $\mathrm{id}$.
MvPolynomial.counitdefMathlib.Algebra.MvPolynomial.Counit, function or constantWording
the counit of R (from the name)
English
Let $R$ be a set. Then the counit of $R$ is a ring homomorphism of the set of multivariate polynomials of $R$ and $\Integer$ and $R$ defined as $\operatorname{toRingHom}$ applied to the counit of $\Integer$ and $R$.
MvPolynomial.counitNatdefMathlib.Algebra.MvPolynomial.Counit, function or constantWording
the natural surjective ring homomorphism of A (from the docstring)
English
Let $A$ be a set. Then the natural surjective ring homomorphism of $A$ is a ring homomorphism of the set of multivariate polynomials of $A$ and $\Natural$ and $A$ defined as the ring homomorphism of the counit of $\Natural$ and $A$.
MvPolynomial.degreeOfdefMathlib.Algebra.MvPolynomial.Degrees, function or constantWording
the degree of n and p (from the name)
English
Let $n$ be an element of $x$. Let $p$ be a multivariate polynomial of $x$ and $R$. Then the degree of $n$ and $p$ is a natural number defined as the count of $n$ and the degree of $p$.
MvPolynomial.degreesdefMathlib.Algebra.MvPolynomial.Degrees, function or constantWording
the degree of p (from the name)
English
Let $p$ be a multivariate polynomial of $x$ and $R$. Then the degree of $p$ is a multiset of $x$ defined as the supremum of the support of $p$ and the function that maps $s$ to $\operatorname{toMultiset}$ applied to $s$.
MvPolynomial.degreesLEdefMathlib.Algebra.MvPolynomial.Degrees, function or constantEnglish
Let $R$ and $x$ be sets. Let $s$ be a multiset of $x$. Then $\operatorname{degreesLE}$ applied to $R$, $x$ and $s$ is a submodule of $R$ and the set of multivariate polynomials of $x$ and $R$.
MvPolynomial.totalDegreedefMathlib.Algebra.MvPolynomial.Degrees, function or constantWording
the total degree of p (from the name)
English
Let $p$ be a multivariate polynomial of $x$ and $R$. Then the total degree of $p$ is a natural number defined as the supremum of the support of $p$ and the function that maps $s$ to the sum of $s$ and the function that maps $x_{2}$ and $e$ to $e$.
MvPolynomial.mkDerivationdefMathlib.Algebra.MvPolynomial.Derivation, function or constantWording
the derivation of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a function from elements of $x$ to elements of $A$. Then the derivation of $R$ and $f$ is a derivation of the set of multivariate polynomials of $x$ and $R$ and $A$.
MvPolynomial.mkDerivationEquivdefMathlib.Algebra.MvPolynomial.Derivation, function or constantWording
the derivation equivalence of R (from the name)
English
Let $R$ be a set. Then the derivation equivalence of $R$ is a linear equivalence of the set of functions from elements of $x$ to elements of $A$ and the set of derivations of the set of multivariate polynomials of $x$ and $R$ and $A$.
MvPolynomial.mkDerivationₗdefMathlib.Algebra.MvPolynomial.Derivation, function or constantWording
the derivation of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a function from elements of $x$ to elements of $A$. Then the derivation of $R$ and $f$ is a linear map of the set of multivariate polynomials of $x$ and $R$ and $A$ defined as the composition of $\operatorname{lsum}$ applied to $R$ and the function that maps $\mathrm{xs1}$ to $\operatorname{symm}$ applied to $\operatorname{ringLmapEquivSelf}$ applied to $R$, $R$ and $A$ and the sum of $\mathrm{xs1}$ and the function that maps $i$ and $k$ to $\HSMulhSMulMACRoAL {\operatorname{monomial} (\mathrm{xs1} - \FinsuppsingleMACRoS {i}{1}, k)}{f (i)}$ and $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$.
MvPolynomial.divMonomialdefMathlib.Algebra.MvPolynomial.Division, function or constantWording
the quotient monomial of p and s (from the name)
English
Let $p$ be a multivariate polynomial of $x$ and $R$. Let $s$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then the quotient monomial of $p$ and $s$ is a multivariate polynomial of $x$ and $R$ defined as the quotient of $p$ and $s$.
MvPolynomial.modMonomialdefMathlib.Algebra.MvPolynomial.Division, function or constantEnglish
Let $x_{2}$ be a multivariate polynomial of $x$ and $R$. Let $s$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{modMonomial}$ applied to $x_{2}$ and $s$ is a multivariate polynomial of $x$ and $R$ defined as $\operatorname{modOf}$ applied to $x_{2}$ and $s$.
MvPolynomial.commAlgEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the commutative algebra isomorphism of x and x1 (from the name)
English
Let $R$, $x$ and $x_{1}$ be sets. Then the commutative algebra isomorphism of $x$ and $x_{1}$ is an algebra isomorphism of the set of multivariate polynomials of $x$ and the set of multivariate polynomials of $x_{1}$ and $R$ and the set of multivariate polynomials of $x_{1}$ and the set of multivariate polynomials of $x$ and $R$ defined as the commutative algebra isomorphism of $R$.
MvPolynomial.finSuccEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the finite successor equivalence of R and n (from the name)
English
Let $R$ be a set. Let $n$ be a natural number. Then the finite successor equivalence of $R$ and $n$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n + 1$ and $R$ and the set of polynomials of the set of multivariate polynomials of $\mathrm{Fin}$ applied to $n$ and $R$ defined as the composition of $\operatorname{renameEquiv}$ applied to $R$ and the finite successor equivalence of $n$ and the left option equivalence of $R$ and $\mathrm{Fin}$ applied to $n$.
MvPolynomial.isEmptyAlgEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantEnglish
Let $R$ and $x$ be sets. Then $\operatorname{isEmptyAlgEquiv}$ applied to $R$ and $x$ is an algebra isomorphism of the set of multivariate polynomials of $x$ and $R$ and $R$ defined as the trivial monoid algebra of $R$ and $\FinsuppMACRoQ {x}{\Natural}$.
MvPolynomial.isEmptyRingEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantEnglish
Let $R$ and $x$ be sets. Then $\operatorname{isEmptyRingEquiv}$ applied to $R$ and $x$ is a ring isomorphism of the set of multivariate polynomials of $x$ and $R$ and $R$ defined as the unique ring isomorphism of $\FinsuppMACRoQ {x}{\Natural}$.
MvPolynomial.mapAlgEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the map algebra isomorphism of x and e (from the name)
English
Let $x$ be a set. Let $e$ be an algebra isomorphism of $x_{2}$ and $x_{3}$. Then the map algebra isomorphism of $x$ and $e$ is an algebra isomorphism of the set of multivariate polynomials of $x$ and $x_{2}$ and the set of multivariate polynomials of $x$ and $x_{3}$ defined as the map algebra isomorphism of $e$.
MvPolynomial.mapEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the map equivalence of x2 and e (from the name)
English
Let $x_{2}$ be a set. Let $e$ be a ring isomorphism of $x$ and $x_{1}$. Then the map equivalence of $x_{2}$ and $e$ is a ring isomorphism of the set of multivariate polynomials of $x_{2}$ and $x$ and the set of multivariate polynomials of $x_{2}$ and $x_{1}$ defined as the map ring isomorphism of $\FinsuppMACRoQ {x_{2}}{\Natural}$ and $e$.
MvPolynomial.mvPolynomialEquivMvPolynomialdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the multivariate polynomial equivalence multivariate polynomial of f and g (from the name)
English
Let $R$, $x$, $x_{1}$ and $x_{2}$ be sets. Let $f$ be a ring homomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $x_{2}$. Let $g$ be a ring homomorphism of the set of multivariate polynomials of $x_{1}$ and $x_{2}$ and the set of multivariate polynomials of $x$ and $R$ such that the composition of the composition of $f$ and $g$ and $\operatorname{C}$ is equal to $\operatorname{C}$, for all elements $n_{1}$ of $x_{1}$, $\EqtMACRoH {f (g (\operatorname{X} (n_{1})))}{\operatorname{X} (n_{1})}$, the composition of the composition of $g$ and $f$ and $\operatorname{C}$ is equal to $\operatorname{C}$ and for all elements $n$ of $x$, $\EqtMACRoH {g (f (\operatorname{X} (n)))}{\operatorname{X} (n)}$. Then the multivariate polynomial equivalence multivariate polynomial of $f$ and $g$ is a ring isomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $x_{2}$.
MvPolynomial.optionEquivLeftdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the left option equivalence of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the left option equivalence of $R$ and $x$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Option}$ applied to $x$ and $R$ and the set of polynomials of the set of multivariate polynomials of $x$ and $R$.
MvPolynomial.optionEquivRightdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the right option equivalence of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the right option equivalence of $R$ and $x$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Option}$ applied to $x$ and $R$ and the set of multivariate polynomials of $x$ and the set of polynomials of $R$.
MvPolynomial.sumAlgEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the sum algebra isomorphism of x and x1 (from the name)
English
Let $R$, $x$ and $x_{1}$ be sets. Then the sum algebra isomorphism of $x$ and $x_{1}$ is an algebra isomorphism of the set of multivariate polynomials of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $R$ and the set of multivariate polynomials of $x$ and the set of multivariate polynomials of $x_{1}$ and $R$ defined as the composition of the domain congruence of the sum finitely supported function additive equivalence product finitely supported function and the curry algebra isomorphism of $R$.
MvPolynomial.sumRingEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the sum ring isomorphism of x and x1 (from the name)
English
Let $R$, $x$ and $x_{1}$ be sets. Then the sum ring isomorphism of $x$ and $x_{1}$ is a ring isomorphism of the set of multivariate polynomials of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $R$ and the set of multivariate polynomials of $x$ and the set of multivariate polynomials of $x_{1}$ and $R$ defined as the composition of the map domain ring isomorphism of $R$ and the sum finitely supported function additive equivalence product finitely supported function and the curry ring isomorphism.
MvPolynomial.uniqueAlgEquivdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the unique algebra isomorphism of R and x1 (from the name)
English
Let $R$ and $x_{1}$ be sets. Then the unique algebra isomorphism of $R$ and $x_{1}$ is an algebra isomorphism of the set of multivariate polynomials of $x_{1}$ and $R$ and the set of polynomials of $R$.
Polynomial.toMvPolynomialdefMathlib.Algebra.MvPolynomial.Equiv, function or constantWording
the multivariate polynomial of i (from the name)
English
Let $i$ be an element of $x$. Then the multivariate polynomial of $i$ is an algebra homomorphism of the set of polynomials of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the algebra evaluation of $\operatorname{X}$ applied to $i$.
MvPolynomial.aevaldefMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the algebra evaluation of f (from the name)
English
Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the algebra evaluation of $f$ is an algebra homomorphism of the set of multivariate polynomials of $x_{1}$ and $R$ and $x$.
MvPolynomial.aevalTowerdefMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the algebra evaluation tower of f and X (from the name)
English
Let $f$ be an algebra homomorphism of $R$ and $A$. Let $X$ be a function from elements of $x$ to elements of $A$. Then the algebra evaluation tower of $f$ and $X$ is an algebra homomorphism of the set of multivariate polynomials of $x$ and $R$ and $A$.
MvPolynomial.evaldefMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the evaluation of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $R$. Then the evaluation of $f$ is a ring homomorphism of the set of multivariate polynomials of $x$ and $R$ and $R$ defined as the evaluation homomorphism of the identity ring homomorphism of $R$ and $f$.
MvPolynomial.eval₂defMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the evaluation of g and p (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $p$ be a multivariate polynomial of $x_{1}$ and $R$. Then the evaluation of $g$ and $p$ is an element of $x$ defined as the sum of the coefficient of $p$ and the function that maps $s$ and $a$ to $f (a)\times \FinsuppProd {s}{n}{e}{(g (n)^ {e})}$.
MvPolynomial.eval₂HomdefMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the evaluation homomorphism of f and g (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Then the evaluation homomorphism of $f$ and $g$ is a ring homomorphism of the set of multivariate polynomials of $x_{1}$ and $R$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{MvPolynomial\_\_eval\_u2082\_}$ applied to $g$ and $\mathrm{MvPolynomial\_\_eval\_u2082\_\_one}$ applied to $f$ and $g$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{MvPolynomial\_\_eval\_u2082\_\_mul}$ applied to $f$ and $g$, $\mathrm{MvPolynomial\_\_eval\_u2082\_\_zero}$ applied to $f$ and $g$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{MvPolynomial\_\_eval\_u2082\_\_add}$ applied to $f$ and $g$.
MvPolynomial.mapdefMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the map of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $x$. Then the map of $f$ is a ring homomorphism of the set of multivariate polynomials of $x_{1}$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $x$ defined as the map ring homomorphism of $\FinsuppMACRoQ {x_{1}}{\Natural}$ and $f$.
MvPolynomial.mapAlgHomdefMathlib.Algebra.MvPolynomial.Eval, function or constantWording
the map algebra homomorphism of f (from the name)
English
Let $f$ be an algebra homomorphism of $x$ and $x_{1}$. Then the map algebra homomorphism of $f$ is an algebra homomorphism of the set of multivariate polynomials of $x_{2}$ and $x$ and the set of multivariate polynomials of $x_{2}$ and $x_{1}$ defined as the map algebra homomorphism of $\FinsuppMACRoQ {x_{2}}{\Natural}$ and $f$.
MvPolynomial.expanddefMathlib.Algebra.MvPolynomial.Expand, function or constantWording
the expand of p (from the name)
English
Let $p$ be a natural number. Then the expand of $p$ is an algebra homomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\mathrm{MvPolynomial\_\_bind\_u2081\_}$ applied to the function that maps $i$ to $\operatorname{X} (i)^ {p}$.
MvPolynomial.bind₁defMathlib.Algebra.MvPolynomial.Monad, function or constantEnglish
Let $f$ be a function from elements of $x$ to multivariate polynomials of $x_{1}$ and $R$. Then $\mathrm{MvPolynomial\_\_bind\_u2081\_}$ applied to $f$ is an algebra homomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $R$ defined as the algebra evaluation of $f$.
MvPolynomial.bind₂defMathlib.Algebra.MvPolynomial.Monad, function or constantEnglish
Let $f$ be a ring homomorphism of $R$ and the set of multivariate polynomials of $x$ and $S$. Then $\mathrm{MvPolynomial\_\_bind\_u2082\_}$ applied to $f$ is a ring homomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x$ and $S$ defined as the evaluation homomorphism of $f$ and $\operatorname{X}$.
MvPolynomial.join₁defMathlib.Algebra.MvPolynomial.Monad, function or constantWording
the join (from the name)
English
The join is an algebra homomorphism of the set of multivariate polynomials of the set of multivariate polynomials of $x$ and $R$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the algebra evaluation of $\mathrm{id}$.
MvPolynomial.join₂defMathlib.Algebra.MvPolynomial.Monad, function or constantWording
the join (from the name)
English
The join is a ring homomorphism of the set of multivariate polynomials of $x$ and the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the evaluation homomorphism of the identity ring homomorphism of the set of multivariate polynomials of $x$ and $R$ and $\operatorname{X}$.
MvPolynomial.pderivdefMathlib.Algebra.MvPolynomial.PDeriv, function or constantEnglish
Let $i$ be an element of $x$. Then $\operatorname{pderiv}$ applied to $i$ is a derivation of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the derivation of $R$ and $\operatorname{single}$ applied to $i$ and $1$.
MvPolynomial.killCompldefMathlib.Algebra.MvPolynomial.Rename, function or constantEnglish
Assume that $f$ is injective. Then $\operatorname{killCompl}$ applied to $\mathrm{hf}$ is an algebra homomorphism of the set of multivariate polynomials of $x_{1}$ and $R$ and the set of multivariate polynomials of $x$ and $R$ defined as the algebra evaluation of the function that maps $i$ to $\mathrm{dite}$ applied to the proposition that $i$ is an element of the range of $f$, the function that maps $h$ to $\operatorname{X}$ applied to $\operatorname{symm}$ applied to the equivalence of $f$ and $\mathrm{hf}$ and $i$ and the function that maps $h_{1}$ to $0$.
MvPolynomial.renamedefMathlib.Algebra.MvPolynomial.Rename, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{rename}$ applied to $f$ is an algebra homomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $R$ defined as the map domain algebra homomorphism of the additive monoid homomorphism of $f$.
MvPolynomial.renameEquivdefMathlib.Algebra.MvPolynomial.Rename, function or constantEnglish
Let $R$ be a set. Let $f$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{renameEquiv}$ applied to $R$ and $f$ is an algebra isomorphism of the set of multivariate polynomials of $x$ and $R$ and the set of multivariate polynomials of $x_{1}$ and $R$.
MvPolynomial.supporteddefMathlib.Algebra.MvPolynomial.Supported, function or constantEnglish
Let $R$ be a set. Let $s$ be an element of $\wp x$. Then $\operatorname{supported}$ applied to $R$ and $s$ is a subalgebra of $R$ and the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{adjoin}$ applied to $R$ and the image of $\operatorname{X}$ and $s$.
MvPolynomial.supportedEquivMvPolynomialdefMathlib.Algebra.MvPolynomial.Supported, function or constantEnglish
Let $s$ be an element of $\wp x$. Then $\operatorname{supportedEquivMvPolynomial}$ applied to $s$ is an algebra isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{supported} (R , s)}{x_{2}})}$ and the set of multivariate polynomials of the set of elements of $s$ and $R$.
MvPolynomial.varsdefMathlib.Algebra.MvPolynomial.Variables, function or constantEnglish
Let $p$ be a multivariate polynomial of $x$ and $R$. Then $\operatorname{vars}$ applied to $p$ is a finite set of $x$ defined as the finite set of the degree of $p$.
NoZeroSMulDivisorsclassMathlib.Algebra.NoZeroSMulDivisors.Defs, predicateEnglish
Let $R$ and $M$ be sets. Then we can say that $\mathrm{NoZeroSMulDivisors}$ holds for $R$ and $M$.
LieAdmissibleAlgebraclassMathlib.Algebra.NonAssoc.LieAdmissible.Defs, predicateEnglish
Let $R$ and $L$ be sets. Then we can say that $\mathrm{LieAdmissibleAlgebra}$ holds for $R$ and $L$.
LieAdmissibleRingclassMathlib.Algebra.NonAssoc.LieAdmissible.Defs, predicateWording
L is a Lie admissible ring (from the name)
English
Let $L$ be a set. Then we can say that $L$ is a Lie admissible ring.
LeftPreLieAlgebraclassMathlib.Algebra.NonAssoc.PreLie.Basic, predicateEnglish
Let $R$ and $L$ be sets. Then we can say that $\mathrm{LeftPreLieAlgebra}$ holds for $R$ and $L$.
LeftPreLieRingclassMathlib.Algebra.NonAssoc.PreLie.Basic, predicateWording
L is a left Lie ring (from the name)
English
Let $L$ be a set. Then we can say that $L$ is a left Lie ring.
RightPreLieAlgebraclassMathlib.Algebra.NonAssoc.PreLie.Basic, predicateEnglish
Let $R$ and $L$ be sets. Then we can say that $\mathrm{RightPreLieAlgebra}$ holds for $R$ and $L$.
RightPreLieRingclassMathlib.Algebra.NonAssoc.PreLie.Basic, predicateWording
L is a right Lie ring (from the name)
English
Let $L$ be a set. Then we can say that $L$ is a right Lie ring.
LeOnePartclassMathlib.Algebra.Notation, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{LeOnePart}$ holds for $x$.
LeOnePart.leOnePartdefMathlib.Algebra.Notation, function or constantEnglish
Let $x_{1}$ be an element of $x$. Then $\operatorname{leOnePart}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
NegPartclassMathlib.Algebra.Notation, predicateWording
x is a negation part (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a negation part.
NegPart.negPartdefMathlib.Algebra.Notation, function or constantWording
the negation part of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the negation part of $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
OneLePartclassMathlib.Algebra.Notation, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{OneLePart}$ holds for $x$.
OneLePart.oneLePartdefMathlib.Algebra.Notation, function or constantEnglish
Let $x_{1}$ be an element of $x$. Then $\operatorname{oneLePart}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
PosPartclassMathlib.Algebra.Notation, predicateWording
x is a positive part part (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a positive part part.
PosPart.posPartdefMathlib.Algebra.Notation, function or constantWording
the positive part part of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the positive part part of $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
BracketclassMathlib.Algebra.Notation.Bracket, predicateEnglish
Let $L$ and $M$ be sets. Then we can say that $\mathrm{Bracket}$ holds for $L$ and $M$.
Bracket.bracketdefMathlib.Algebra.Notation.Bracket, function or constantWording
the bracket of x and x1 (from the name)
English
Let $x$ be an element of $L$. Let $x_{1}$ be an element of $M$. Then the bracket of $x$ and $x_{1}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.
HVAddclassMathlib.Algebra.Notation.Defs, predicateEnglish
Let $x$ and $x_{1}$ be sets. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{HVAdd}$ holds for $x$, $x_{1}$ and $x_{2}$.
HVAdd.hVAdddefMathlib.Algebra.Notation.Defs, function or constantWording
the sum of x3 and x4 (from the name)
English
Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $x_{1}$. Then the sum of $x_{3}$ and $x_{4}$ is an element of $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.
SDivclassMathlib.Algebra.Notation.Defs, predicateWording
G is a quotient (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 quotient.
SDiv.sdivdefMathlib.Algebra.Notation.Defs, function or constantEnglish
Let $x$ and $x_{1}$ be elements of $P$. Then $\operatorname{sdiv}$ applied to $x$ and $x_{1}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.
StarclassMathlib.Algebra.Notation.Defs, predicateWording
R is a star (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a star.
Star.stardefMathlib.Algebra.Notation.Defs, function or constantWording
the star of x (from the name)
English
Let $x$ be an element of $R$. Then the star of $x$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.
VAddclassMathlib.Algebra.Notation.Defs, predicateEnglish
Let $G$ and $P$ be sets. Then we can say that $\mathrm{VAdd}$ holds for $G$ and $P$.
VAdd.vadddefMathlib.Algebra.Notation.Defs, function or constantWording
the vector sum of x and x1 (from the name)
English
Let $x$ be an element of $G$. Let $x_{1}$ be an element of $P$. Then the vector sum of $x$ and $x_{1}$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.
VSubclassMathlib.Algebra.Notation.Defs, predicateWording
G is a difference (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 difference.
VSub.vsubdefMathlib.Algebra.Notation.Defs, function or constantWording
the vector difference of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be elements of $P$. Then the vector difference of $x$ and $x_{1}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.
Set.indicatordefMathlib.Algebra.Notation.Indicator, function or constantWording
the indicator of f and x2 (from the name)
English
Let $s$ be an element of $\wp x$. Let $f$ be a function from elements of $x$ to elements of $M$. Let $x_{2}$ be an element of $x$. Then the indicator of $f$ and $x_{2}$ is an element of $M$ defined as $\iteMACRoG {(\MembershipmemMACRoT {s}{x_{2}})}{f (x_{2})}{0}$.
Set.mulIndicatordefMathlib.Algebra.Notation.Indicator, function or constantWording
the multiplicative indicator of f and x2 (from the name)
English
Let $s$ be an element of $\wp x$. Let $f$ be a function from elements of $x$ to elements of $M$. Let $x_{2}$ be an element of $x$. Then the multiplicative indicator of $f$ and $x_{2}$ is an element of $M$ defined as $\iteMACRoG {(\MembershipmemMACRoT {s}{x_{2}})}{f (x_{2})}{1}$.
Pi.mulSingledefMathlib.Algebra.Notation.Pi.Basic, function or constantEnglish
Let $i$ and $j$ be elements of $x$. Let $x_{3}$ be an element of $M$ applied to $i$. Then $\operatorname{mulSingle}$ applied to $i$, $x_{3}$ and $j$ is an element of $M$ applied to $j$ defined as $\operatorname{update}$ applied to $1$, $i$, $x_{3}$ and $j$.
Pi.singledefMathlib.Algebra.Notation.Pi.Basic, function or constantEnglish
Let $i$ and $j$ be elements of $x$. Let $x_{3}$ be an element of $M$ applied to $i$. Then $\operatorname{single}$ applied to $i$, $x_{3}$ and $j$ is an element of $M$ applied to $j$ defined as $\operatorname{update}$ applied to $0$, $i$, $x_{3}$ and $j$.
Function.mulSupportdefMathlib.Algebra.Notation.Support, function or constantWording
the multiplicative support of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $M$. Then the multiplicative support of $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Neq} (f (x_{2}), 1)$.
Function.supportdefMathlib.Algebra.Notation.Support, function or constantWording
the support of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $M$. Then the support of $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Neq} (f (x_{2}), 0)$.
AddOppositedefMathlib.Algebra.Opposites, typeWording
additive opposite of x (from the name)
English
Let $x$ be a set. Then an additive opposite of $x$ is an element of the function that maps $x$ to $\mathrm{PreOpposite}$ applied to $x$.
AddOpposite.opdefMathlib.Algebra.Opposites, function or constantWording
the opposite of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the opposite of $x_{1}$ is an additive opposite of $x$ defined as $\operatorname{op'}$ applied to $x_{1}$.
AddOpposite.opEquivdefMathlib.Algebra.Opposites, function or constantWording
the opposite equivalence (from the name)
English
The opposite equivalence is an equivalence from $x$ to the set of additive opposites of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$, $\operatorname{unop}$, $\mathrm{AddOpposite\_\_unop\_op}$ and $\mathrm{AddOpposite\_\_op\_unop}$.
AddOpposite.rec'defMathlib.Algebra.Opposites, function or constantEnglish
Let $h$ be a function from elements $X_{1}$ of $x$ to elements of $F$ applied to the opposite of $X_{1}$. Let $X$ be an additive opposite of $x$. Then $\operatorname{rec'}$ 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 the opposite of $h$ and $X$.
AddOpposite.unopdefMathlib.Algebra.Opposites, function or constantWording
the opposite of x1 (from the name)
English
Let $x_{1}$ be an additive opposite of $x$. Then the opposite of $x_{1}$ is an element of $x$ defined as the opposite of $x_{1}$.
MulOppositedefMathlib.Algebra.Opposites, typeWording
multiplicative opposite of x (from the name)
English
Let $x$ be a set. Then a multiplicative opposite of $x$ is an element of the function that maps $x$ to $\mathrm{PreOpposite}$ applied to $x$.
MulOpposite.opdefMathlib.Algebra.Opposites, function or constantWording
the opposite of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the opposite of $x_{1}$ is a multiplicative opposite of $x$ defined as $\operatorname{op'}$ applied to $x_{1}$.
MulOpposite.opEquivdefMathlib.Algebra.Opposites, function or constantWording
the opposite equivalence (from the name)
English
The opposite equivalence is an equivalence from $x$ to the set of multiplicative opposites of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$, $\operatorname{unop}$, $\mathrm{MulOpposite\_\_unop\_op}$ and $\mathrm{MulOpposite\_\_op\_unop}$.
MulOpposite.rec'defMathlib.Algebra.Opposites, function or constantEnglish
Let $h$ be a function from elements $X_{1}$ of $x$ to elements of $F$ applied to the opposite of $X_{1}$. Let $X$ be a multiplicative opposite of $x$. Then $\operatorname{rec'}$ 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 the opposite of $h$ and $X$.
MulOpposite.unopdefMathlib.Algebra.Opposites, function or constantWording
the opposite of x1 (from the name)
English
Let $x_{1}$ be a multiplicative opposite of $x$. Then the opposite of $x_{1}$ is an element of $x$ defined as the opposite of $x_{1}$.
PreOpposite.unop'defMathlib.Algebra.Opposites, function or constantWording
the opposite of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{PreOpposite}$ applied to $x$. Then the opposite of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AbsoluteValuestructureMathlib.Algebra.Order.AbsoluteValue.Basic, typeWording
absolute value of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the absolute values of $R$ and $S$ are a basic type.
AbsoluteValue.IsNontrivialdefMathlib.Algebra.Order.AbsoluteValue.Basic, predicateWording
v is nontrivial (from the name)
English
Let $v$ be an absolute value of $R$ and $S$. Then $v$ is nontrivial, if there exists an element $x_{3}$ of $R$, such that $x_{3} \neq 0$ and $v (x_{3})\neq 1$.
AbsoluteValue.absdefMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantWording
the absolute value (from the name)
English
The absolute value is an absolute value of $S$ and $S$.
AbsoluteValue.toMonoidHomdefMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantWording
the monoid homomorphism of abv (from the name)
English
Let $\mathrm{abv}$ be an absolute value of $R$ and $S$. Then the monoid homomorphism of $\mathrm{abv}$ is a monoid homomorphism of $R$ and $S$ defined as the monoid homomorphism of $\mathrm{abv}$.
AbsoluteValue.toMonoidWithZeroHomdefMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantWording
the monoid with zero homomorphism of abv (from the name)
English
Let $\mathrm{abv}$ be an absolute value of $R$ and $S$. Then the monoid with zero homomorphism of $\mathrm{abv}$ is a monoid with zero homomorphism of $R$ and $S$.
AbsoluteValue.trivialdefMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantEnglish
$\operatorname{trivial}$ is an absolute value of $R$ and $S$.
IsAbsoluteValueclassMathlib.Algebra.Order.AbsoluteValue.Basic, predicateWording
f is a absolute value (from the name)
English
Let $f$ be a function from elements of $R$ to elements of $S$. Then we can say that $f$ is an absolute value.
IsAbsoluteValue.abvHomdefMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantEnglish
Let $\mathrm{abv}$ be a function from elements of $R$ to elements of $S$. Then $\operatorname{abvHom}$ applied to $\mathrm{abv}$ is a monoid with zero homomorphism of $R$ and $S$ defined as the monoid with zero homomorphism of the absolute value of $\mathrm{abv}$.
IsAbsoluteValue.abvHom'defMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantEnglish
Let $\mathrm{abv}$ be a function from elements of $R$ to elements of $S$. Then $\operatorname{abvHom'}$ applied to $\mathrm{abv}$ is a monoid with zero homomorphism of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{abv}$ and $\mathrm{IsAbsoluteValue\_\_abv\_zero}$ applied to $\mathrm{abv}$, $\mathrm{IsAbsoluteValue\_\_abv\_one'}$ applied to $\mathrm{abv}$ and $\mathrm{IsAbsoluteValue\_\_abv\_mul}$ applied to $\mathrm{abv}$.
IsAbsoluteValue.toAbsoluteValuedefMathlib.Algebra.Order.AbsoluteValue.Basic, function or constantWording
the absolute value of abv (from the name)
English
Let $\mathrm{abv}$ be a function from elements of $R$ to elements of $S$. Then the absolute value of $\mathrm{abv}$ is an absolute value of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{abv}$ and $\mathrm{IsAbsoluteValue\_\_abv\_mul'}$, $\mathrm{IsAbsoluteValue\_\_abv\_nonneg'}$, the function that maps $x_{3}$ to $\mathrm{IsAbsoluteValue\_\_abv\_eq\_zero'}$ and $\mathrm{IsAbsoluteValue\_\_abv\_add'}$.
AbsoluteValue.IsEuclideanstructureMathlib.Algebra.Order.AbsoluteValue.Euclidean, predicateWording
abv is Euclidean (from the name)
English
Let $\mathrm{abv}$ be an absolute value of $R$ and $S$. Then we can say that $\mathrm{abv}$ is Euclidean.
LinearOrderedAddCommGroupWithTopclassMathlib.Algebra.Order.AddGroupWithTop, predicateWording
x is a linear ordered additive commutative group with top (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a linear ordered additive commutative group with top.
LinearOrderedAddCommMonoidWithTopclassMathlib.Algebra.Order.AddGroupWithTop, predicateWording
x is a linear ordered additive commutative monoid with top (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a linear ordered additive commutative monoid with top.
IsOrderedCancelSMulclassMathlib.Algebra.Order.AddTorsor, predicateEnglish
Let $G$ and $P$ be sets. Then we can say that $\mathrm{IsOrderedCancelSMul}$ holds for $G$ and $P$.
IsOrderedCancelVAddclassMathlib.Algebra.Order.AddTorsor, predicateEnglish
Let $G$ and $P$ be sets. Then we can say that $\mathrm{IsOrderedCancelVAdd}$ holds for $G$ and $P$.
IsOrderedSMulclassMathlib.Algebra.Order.AddTorsor, predicateEnglish
Let $G$ and $P$ be sets. Then we can say that $\mathrm{IsOrderedSMul}$ holds for $G$ and $P$.
IsOrderedVAddclassMathlib.Algebra.Order.AddTorsor, predicateEnglish
Let $G$ and $P$ be sets. Then we can say that $\mathrm{IsOrderedVAdd}$ holds for $G$ and $P$.
Finset.finsuppAntidiagdefMathlib.Algebra.Order.Antidiag.Finsupp, function or constantEnglish
Let $s$ be a finite set of $x$. Let $n$ be an element of $x_{1}$. Then $\operatorname{finsuppAntidiag}$ applied to $s$ and $n$ is a finite set of $\FinsuppMACRoQ {x}{x_{1}}$.
Finset.finsuppAntidiagEquivdefMathlib.Algebra.Order.Antidiag.FinsuppEquiv, function or constantEnglish
Let $s$ be a finite set of $x$. Let $n$ be a natural number. Then $\operatorname{finsuppAntidiagEquiv}$ applied to $s$ and $n$ is an equivalence from $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{finsuppAntidiag} (s , n)}{x_{2}})}$ to the set of symmetric powers of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ and $n$ defined as the composition of $\operatorname{finsuppAntidiagEquivSubtype}$ applied to $s$ and $n$ and the inverse of the equivalence natural sum of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $n$.
Finset.finsuppAntidiagEquivSubtypedefMathlib.Algebra.Order.Antidiag.FinsuppEquiv, function or constantEnglish
Let $s$ be a finite set of $x$. Let $n$ be an element of $x_{1}$. Then $\operatorname{finsuppAntidiagEquivSubtype}$ applied to $s$ and $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{finsuppAntidiag} (s , n)}{x_{6}})})}{(\SubtypeSet {P}{(\EqtMACRoH {\operatorname{sum} (P , \lambda x_{7} . \mathrm{id})}{n})})}$.
Nat.finMulAntidiagdefMathlib.Algebra.Order.Antidiag.Nat, function or constantEnglish
Let $d$ and $n$ be natural numbers. Then $\operatorname{finMulAntidiag}$ applied to $d$ and $n$ is a finite set of the set of functions from elements of $\mathrm{Fin}$ applied to $d$ to natural numbers defined as $\mathrm{dite}$ applied to $\mathrm{Lt} (0 , n)$, the function that maps $\mathrm{hn}$ to the map of the right arrow congruence of the composition of the embedding of the product and $\operatorname{mk}$ applied to $\operatorname{val}$ and $\mathrm{PNat\_\_coe\_injective}$ and $\operatorname{finAntidiagonal}$ applied to $d$ and $\operatorname{ofMul}$ applied to $n$ and the function that maps $\mathrm{hn1}$ to $\operatorname{emptyCollection}$.
Finset.finAntidiagonaldefMathlib.Algebra.Order.Antidiag.Pi, function or constantEnglish
Let $d$ be a natural number. Let $n$ be an element of $x$. Then $\operatorname{finAntidiagonal}$ applied to $d$ and $n$ is a finite set of the set of functions from elements of $\mathrm{Fin}$ applied to $d$ to elements of $x$ defined as $\operatorname{aux}$ applied to $d$ and $n$.
Finset.piAntidiagdefMathlib.Algebra.Order.Antidiag.Pi, function or constantEnglish
Let $s$ be a finite set of $x$. Let $n$ be an element of $x_{1}$. Then $\operatorname{piAntidiag}$ applied to $s$ and $n$ is a finite set of the set of functions from elements of $x$ to elements of $x_{1}$.
Finset.HasAntidiagonalclassMathlib.Algebra.Order.Antidiag.Prod, predicateEnglish
Let $A$ be a set. Then we can say that $\operatorname{HasAntidiagonal}$ holds for $A$.
Finset.HasAntidiagonal.antidiagonaldefMathlib.Algebra.Order.Antidiag.Prod, function or constantEnglish
Let $x_{1}$ be an element of $A$. Then $\operatorname{antidiagonal}$ applied to $x_{1}$ is a finite set of $\mathrm{Prod}$ applied to $A$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProddefMathlib.Algebra.Order.Antidiag.Prod, function or constantWording
the sigma antidiagonal equivalence product (from the name)
English
The sigma antidiagonal equivalence product is an element of $\EquivMACRoAE {\Sigma (\lambda n . \SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{antidiagonal} (n)}{x_{2}})})}{\mathrm{Prod} (A , A)}$.
Finset.HasMulAntidiagonalclassMathlib.Algebra.Order.Antidiag.Prod, predicateEnglish
Let $A$ be a set. Then we can say that $\operatorname{HasMulAntidiagonal}$ holds for $A$.
Finset.HasMulAntidiagonal.mulAntidiagonaldefMathlib.Algebra.Order.Antidiag.Prod, function or constantEnglish
Let $x_{1}$ be an element of $A$. Then $\operatorname{mulAntidiagonal}$ applied to $x_{1}$ is a finite set of $\mathrm{Prod}$ applied to $A$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProddefMathlib.Algebra.Order.Antidiag.Prod, function or constantWording
the sigma multiplicative antidiagonal equivalence product (from the name)
English
The sigma multiplicative antidiagonal equivalence product is an element of $\EquivMACRoAE {\Sigma (\lambda n . \SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mulAntidiagonal} (n)}{x_{2}})})}{\mathrm{Prod} (A , A)}$.
ArchimedeanClassdefMathlib.Algebra.Order.Archimedean.Class, typeWording
archimedean class of M (from the name)
English
Let $M$ be a set. Then an archimedean class of $M$ is an element of the function that maps $M$ to the set of antisymmetrizations of the set of archimedean orders of $M$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$.
ArchimedeanClass.addSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the additive subgroup of s (from the name)
English
Let $s$ be a upper set of the set of archimedean classes of $M$. Then the additive subgroup of $s$ is an additive subgroup of $M$.
ArchimedeanClass.ballAddSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the ball additive subgroup of c (from the name)
English
Let $c$ be an archimedean class of $M$. Then the ball additive subgroup of $c$ is an additive subgroup of $M$ defined as the additive subgroup of $\operatorname{Ioi}$ applied to $c$.
ArchimedeanClass.closedBallAddSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the closed ball additive subgroup of c (from the name)
English
Let $c$ be an archimedean class of $M$. Then the closed ball additive subgroup of $c$ is an additive subgroup of $M$ defined as the additive subgroup of $\operatorname{Ici}$ applied to $c$.
ArchimedeanClass.liftdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift of f and x3 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $x_{2}$ such that for all elements $a$ and $b$ of $M$, if $\EqtMACRoH {\operatorname{mk} (a)}{\operatorname{mk} (b)}$, then $\EqtMACRoH {f (a)}{f (b)}$. Let $x_{3}$ be an archimedean class of $M$. Then the lift of $f$ and $x_{3}$ is an element of $x_{2}$.
ArchimedeanClass.liftOrderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift order homomorphism of f and h1 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $x_{2}$ such that for all elements $a$ and $b$ of $M$, if $\operatorname{mk} (a)\leq \operatorname{mk} (b)$, then $f (a)\leq f (b)$. Then the lift order homomorphism of $f$ and $h_{1}$ is an order homomorphism of the set of archimedean classes of $M$ and $x_{2}$.
ArchimedeanClass.lift₂defMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift of x3 and x4 (from the name)
English
Let $f$ be a function from elements of $M$ and elements of $M$ to elements of $x_{2}$ such that for all elements $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ of $M$, if $\EqtMACRoH {\operatorname{mk} (x_{5})}{\operatorname{mk} (x_{6})}$, then if $\EqtMACRoH {\operatorname{mk} (x_{7})}{\operatorname{mk} (x_{8})}$, then $\EqtMACRoH {f (x_{5} , x_{7})}{f (x_{6} , x_{8})}$. Let $x_{3}$ and $x_{4}$ be archimedean classes of $M$. Then the lift of $x_{3}$ and $x_{4}$ is an element of $x_{2}$.
ArchimedeanClass.mkdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $a$ be an element of $M$. Then $\operatorname{mk}$ applied to $a$ is an archimedean class of $M$ defined as the antisymmetrization of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $\operatorname{of}$ applied to $a$.
ArchimedeanClass.orderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be an order additive monoid homomorphism of $M$ and $N$. Then the order homomorphism of $f$ is an order homomorphism of the set of archimedean classes of $M$ and the set of archimedean classes of $N$ defined as the antisymmetrization of the order homomorphism of $f$.
ArchimedeanClass.outdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $A$ be an archimedean class of $M$. Then $\operatorname{out}$ applied to $A$ is an element of $M$ defined as $\operatorname{val}$ applied to $\operatorname{out}$ applied to $A$.
ArchimedeanClass.subsemigroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the subsemigroup of s (from the name)
English
Let $s$ be a upper set of the set of archimedean classes of $M$. Then the subsemigroup of $s$ is an additive subsemigroup of $M$.
ArchimedeanOrderdefMathlib.Algebra.Order.Archimedean.Class, typeWording
archimedean order of M (from the name)
English
Let $M$ be a set. Then an archimedean order of $M$ is an element of the function that maps $M$ to $M$.
ArchimedeanOrder.ofdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
$\operatorname{of}$ is an equivalence from $M$ to the set of archimedean orders of $M$ defined as the identity of $M$.
ArchimedeanOrder.orderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be an order additive monoid homomorphism of $M$ and $N$. Then the order homomorphism of $f$ is an order homomorphism of the set of archimedean orders of $M$ and the set of archimedean orders of $N$.
ArchimedeanOrder.valdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the value (from the name)
English
The value is an equivalence from the set of archimedean orders of $M$ to $M$ defined as the identity of the set of archimedean orders of $M$.
FiniteArchimedeanClassdefMathlib.Algebra.Order.Archimedean.Class, typeWording
finite archimedean class of M (from the name)
English
Let $M$ be a set. Then a finite archimedean class of $M$ is an element of the function that maps $M$ to $\SubtypeSet {A}{\mathrm{Neq} (A , \operatorname{top})}$.
FiniteArchimedeanClass.addSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the additive subgroup of s (from the name)
English
Let $s$ be a upper set of the set of finite archimedean classes of $M$. Then the additive subgroup of $s$ is an additive subgroup of $M$.
FiniteArchimedeanClass.ballAddSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the ball additive subgroup of c (from the name)
English
Let $c$ be a finite archimedean class of $M$. Then the ball additive subgroup of $c$ is an additive subgroup of $M$ defined as the additive subgroup of $\operatorname{Ioi}$ applied to $c$.
FiniteArchimedeanClass.closedBallAddSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the closed ball additive subgroup of c (from the name)
English
Let $c$ be a finite archimedean class of $M$. Then the closed ball additive subgroup of $c$ is an additive subgroup of $M$ defined as the additive subgroup of $\operatorname{Ici}$ applied to $c$.
FiniteArchimedeanClass.congrOrderIsodefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the congruence order isomorphism of e (from the name)
English
Let $e$ be an order isomorphism of the set of archimedean classes of $M$ and the set of archimedean classes of $N$. Then the congruence order isomorphism of $e$ is an order isomorphism of the set of finite archimedean classes of $M$ and the set of finite archimedean classes of $N$.
FiniteArchimedeanClass.liftdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift of f and x3 (from the name)
English
Let $f$ be a function from elements of $\SubtypeSet {a_{3}}{\mathrm{Neq} (a_{3} , 0)}$ to elements of $x_{2}$ such that for all elements $a$ of $\SubtypeSet {a_{2}}{\mathrm{Neq} (a_{2} , 0)}$, for all elements $b$ of $\SubtypeSet {a_{1}}{\mathrm{Neq} (a_{1} , 0)}$, if $\EqtMACRoH {\operatorname{mk} (a , \operatorname{prop} (a))}{\operatorname{mk} (b , \operatorname{prop} (b))}$, then $\EqtMACRoH {f (a)}{f (b)}$. Let $x_{3}$ be a finite archimedean class of $M$. Then the lift of $f$ and $x_{3}$ is an element of $x_{2}$.
FiniteArchimedeanClass.liftOrderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift order homomorphism of f and h1 (from the name)
English
Let $f$ be a function from elements of $\SubtypeSet {a_{3}}{\mathrm{Neq} (a_{3} , 0)}$ to elements of $x_{2}$ such that for all elements $a$ of $\SubtypeSet {a_{2}}{\mathrm{Neq} (a_{2} , 0)}$, for all elements $b$ of $\SubtypeSet {a_{1}}{\mathrm{Neq} (a_{1} , 0)}$, if $\operatorname{mk} (a , \operatorname{prop} (a))\leq \operatorname{mk} (b , \operatorname{prop} (b))$, then $f (a)\leq f (b)$. Then the lift order homomorphism of $f$ and $h_{1}$ is an order homomorphism of the set of finite archimedean classes of $M$ and $x_{2}$.
FiniteArchimedeanClass.mkdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $a$ be an element of $M$ such that $a \neq 0$. Then $\operatorname{mk}$ applied to $a$ and $h_{1}$ is a finite archimedean class of $M$ defined as $\operatorname{mk}$ applied to $a$.
FiniteArchimedeanClass.toUpperSetAddArchimedeanClassdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the upper set additive archimedean class (from the name)
English
The upper set additive archimedean class is an order embedding of the set of upper sets of the set of finite archimedean classes of $M$ and the set of upper sets of the set of archimedean classes of $M$.
FiniteArchimedeanClass.withTopOrderIsodefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $M$ be a set. Then $\operatorname{withTopOrderIso}$ applied to $M$ is an order isomorphism of $\mathrm{WithTop}$ applied to the set of finite archimedean classes of $M$ and the set of archimedean classes of $M$ defined as the subtype order isomorphism.
FiniteMulArchimedeanClassdefMathlib.Algebra.Order.Archimedean.Class, typeWording
finite multiplicative archimedean class of M (from the name)
English
Let $M$ be a set. Then a finite multiplicative archimedean class of $M$ is an element of the function that maps $M$ to $\SubtypeSet {A}{\mathrm{Neq} (A , \operatorname{top})}$.
FiniteMulArchimedeanClass.ballSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the ball subgroup of c (from the name)
English
Let $c$ be a finite multiplicative archimedean class of $M$. Then the ball subgroup of $c$ is a subgroup of $M$ defined as the subgroup of $\operatorname{Ioi}$ applied to $c$.
FiniteMulArchimedeanClass.closedBallSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the closed ball subgroup of c (from the name)
English
Let $c$ be a finite multiplicative archimedean class of $M$. Then the closed ball subgroup of $c$ is a subgroup of $M$ defined as the subgroup of $\operatorname{Ici}$ applied to $c$.
FiniteMulArchimedeanClass.congrOrderIsodefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the congruence order isomorphism of e (from the name)
English
Let $e$ be an order isomorphism of the set of multiplicative archimedean classes of $M$ and the set of multiplicative archimedean classes of $N$. Then the congruence order isomorphism of $e$ is an order isomorphism of the set of finite multiplicative archimedean classes of $M$ and the set of finite multiplicative archimedean classes of $N$.
FiniteMulArchimedeanClass.liftdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift of f and x3 (from the name)
English
Let $f$ be a function from elements of $\SubtypeSet {a_{3}}{\mathrm{Neq} (a_{3} , 1)}$ to elements of $x_{2}$ such that for all elements $a$ of $\SubtypeSet {a_{2}}{\mathrm{Neq} (a_{2} , 1)}$, for all elements $b$ of $\SubtypeSet {a_{1}}{\mathrm{Neq} (a_{1} , 1)}$, if $\EqtMACRoH {\operatorname{mk} (a , \operatorname{prop} (a))}{\operatorname{mk} (b , \operatorname{prop} (b))}$, then $\EqtMACRoH {f (a)}{f (b)}$. Let $x_{3}$ be a finite multiplicative archimedean class of $M$. Then the lift of $f$ and $x_{3}$ is an element of $x_{2}$.
FiniteMulArchimedeanClass.liftOrderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift order homomorphism of f and h1 (from the name)
English
Let $f$ be a function from elements of $\SubtypeSet {a_{3}}{\mathrm{Neq} (a_{3} , 1)}$ to elements of $x_{2}$ such that for all elements $a$ of $\SubtypeSet {a_{2}}{\mathrm{Neq} (a_{2} , 1)}$, for all elements $b$ of $\SubtypeSet {a_{1}}{\mathrm{Neq} (a_{1} , 1)}$, if $\operatorname{mk} (a , \operatorname{prop} (a))\leq \operatorname{mk} (b , \operatorname{prop} (b))$, then $f (a)\leq f (b)$. Then the lift order homomorphism of $f$ and $h_{1}$ is an order homomorphism of the set of finite multiplicative archimedean classes of $M$ and $x_{2}$.
FiniteMulArchimedeanClass.mkdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $a$ be an element of $M$ such that $a \neq 1$. Then $\operatorname{mk}$ applied to $a$ and $h_{1}$ is a finite multiplicative archimedean class of $M$ defined as $\operatorname{mk}$ applied to $a$.
FiniteMulArchimedeanClass.subgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the subgroup of s (from the name)
English
Let $s$ be a upper set of the set of finite multiplicative archimedean classes of $M$. Then the subgroup of $s$ is a subgroup of $M$.
FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClassdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the upper set multiplicative archimedean class (from the name)
English
The upper set multiplicative archimedean class is an order embedding of the set of upper sets of the set of finite multiplicative archimedean classes of $M$ and the set of upper sets of the set of multiplicative archimedean classes of $M$.
FiniteMulArchimedeanClass.withTopOrderIsodefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $M$ be a set. Then $\operatorname{withTopOrderIso}$ applied to $M$ is an order isomorphism of $\mathrm{WithTop}$ applied to the set of finite multiplicative archimedean classes of $M$ and the set of multiplicative archimedean classes of $M$ defined as the subtype order isomorphism.
MulArchimedeanClassdefMathlib.Algebra.Order.Archimedean.Class, typeWording
multiplicative archimedean class of M (from the name)
English
Let $M$ be a set. Then a multiplicative archimedean class of $M$ is an element of the function that maps $M$ to the set of antisymmetrizations of the set of multiplicative archimedean orders of $M$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$.
MulArchimedeanClass.ballSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the ball subgroup of c (from the name)
English
Let $c$ be a multiplicative archimedean class of $M$. Then the ball subgroup of $c$ is a subgroup of $M$ defined as the subgroup of $\operatorname{Ioi}$ applied to $c$.
MulArchimedeanClass.closedBallSubgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the closed ball subgroup of c (from the name)
English
Let $c$ be a multiplicative archimedean class of $M$. Then the closed ball subgroup of $c$ is a subgroup of $M$ defined as the subgroup of $\operatorname{Ici}$ applied to $c$.
MulArchimedeanClass.liftdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift of f and x3 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $x_{2}$ such that for all elements $a$ and $b$ of $M$, if $\EqtMACRoH {\operatorname{mk} (a)}{\operatorname{mk} (b)}$, then $\EqtMACRoH {f (a)}{f (b)}$. Let $x_{3}$ be a multiplicative archimedean class of $M$. Then the lift of $f$ and $x_{3}$ is an element of $x_{2}$.
MulArchimedeanClass.liftOrderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift order homomorphism of f and h1 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $x_{2}$ such that for all elements $a$ and $b$ of $M$, if $\operatorname{mk} (a)\leq \operatorname{mk} (b)$, then $f (a)\leq f (b)$. Then the lift order homomorphism of $f$ and $h_{1}$ is an order homomorphism of the set of multiplicative archimedean classes of $M$ and $x_{2}$.
MulArchimedeanClass.lift₂defMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the lift of x3 and x4 (from the name)
English
Let $f$ be a function from elements of $M$ and elements of $M$ to elements of $x_{2}$ such that for all elements $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ of $M$, if $\EqtMACRoH {\operatorname{mk} (x_{5})}{\operatorname{mk} (x_{6})}$, then if $\EqtMACRoH {\operatorname{mk} (x_{7})}{\operatorname{mk} (x_{8})}$, then $\EqtMACRoH {f (x_{5} , x_{7})}{f (x_{6} , x_{8})}$. Let $x_{3}$ and $x_{4}$ be multiplicative archimedean classes of $M$. Then the lift of $x_{3}$ and $x_{4}$ is an element of $x_{2}$.
MulArchimedeanClass.mkdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $a$ be an element of $M$. Then $\operatorname{mk}$ applied to $a$ is a multiplicative archimedean class of $M$ defined as the antisymmetrization of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $\operatorname{of}$ applied to $a$.
MulArchimedeanClass.orderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be an order monoid homomorphism of $M$ and $N$. Then the order homomorphism of $f$ is an order homomorphism of the set of multiplicative archimedean classes of $M$ and the set of multiplicative archimedean classes of $N$ defined as the antisymmetrization of the order homomorphism of $f$.
MulArchimedeanClass.outdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
Let $A$ be a multiplicative archimedean class of $M$. Then $\operatorname{out}$ applied to $A$ is an element of $M$ defined as $\operatorname{val}$ applied to $\operatorname{out}$ applied to $A$.
MulArchimedeanClass.subgroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the subgroup of s (from the name)
English
Let $s$ be a upper set of the set of multiplicative archimedean classes of $M$. Then the subgroup of $s$ is a subgroup of $M$.
MulArchimedeanClass.subsemigroupdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the subsemigroup of s (from the name)
English
Let $s$ be a upper set of the set of multiplicative archimedean classes of $M$. Then the subsemigroup of $s$ is a subsemigroup of $M$.
MulArchimedeanOrderdefMathlib.Algebra.Order.Archimedean.Class, typeWording
multiplicative archimedean order of M (from the name)
English
Let $M$ be a set. Then a multiplicative archimedean order of $M$ is an element of the function that maps $M$ to $M$.
MulArchimedeanOrder.ofdefMathlib.Algebra.Order.Archimedean.Class, function or constantEnglish
$\operatorname{of}$ is an equivalence from $M$ to the set of multiplicative archimedean orders of $M$ defined as the identity of $M$.
MulArchimedeanOrder.orderHomdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be an order monoid homomorphism of $M$ and $N$. Then the order homomorphism of $f$ is an order homomorphism of the set of multiplicative archimedean orders of $M$ and the set of multiplicative archimedean orders of $N$.
MulArchimedeanOrder.valdefMathlib.Algebra.Order.Archimedean.Class, function or constantWording
the value (from the name)
English
The value is an equivalence from the set of multiplicative archimedean orders of $M$ to $M$ defined as the identity of the set of multiplicative archimedean orders of $M$.
ArchimedeanclassMathlib.Algebra.Order.Archimedean.Defs, predicateWording
R is a archimedean (from the name)
English
Let $R$ be a set. Then we can say that $R$ is an archimedean.
MulArchimedeanclassMathlib.Algebra.Order.Archimedean.Defs, predicateWording
R is a multiplicative archimedean (from the name)
English
Let $R$ be a set. Then we can say that $R$ is a multiplicative archimedean.
CauSeqdefMathlib.Algebra.Order.CauSeq.Basic, typeEnglish
Let $x_{3}$ be a set. Let $\mathrm{abv}$ be a function from elements of $x_{3}$ to elements of $x$. Then an element of $\mathrm{CauSeq}$ applied to $x_{3}$ and $\mathrm{abv}$ is an element of the function that maps $x_{3}$ and $\mathrm{abv}$ to $\SubtypeSet {f}{\mathrm{IsCauSeq} (\mathrm{abv} , f)}$.
CauSeq.LimZerodefMathlib.Algebra.Order.CauSeq.Basic, predicateWording
f is a limit zero (from the name)
English
Let $f$ be an element of $\mathrm{CauSeq}$ applied to $x_{1}$ and $\mathrm{abv}$. Then $f$ is a limit zero, if for all elements $x_{5}$ of $x$, if $x_{5} > 0$, then there exists a natural number $i$, such that for all natural numbers $j$, if $j \geq i$, then $\mathrm{abv} (j)< x_{5}$.
CauSeq.PosdefMathlib.Algebra.Order.CauSeq.Basic, predicateWording
f is a positive part (from the name)
English
Let $f$ be an element of $\mathrm{CauSeq}$ applied to $x$ and $\mathrm{abs}$. Then $f$ is a positive part, if there exists an element $K$ of $x$, such that $K > 0$ and there exists a natural number $i$ such that for all natural numbers $j$, if $j \geq i$, then $K \leq j$.
CauSeq.constdefMathlib.Algebra.Order.CauSeq.Basic, function or constantWording
the constant Cauchy sequence of abv and x5 (from the docstring)
English
Let $\mathrm{abv}$ be a function from elements of $x_{1}$ to elements of $x$. Let $x_{5}$ be an element of $x_{1}$. Then the constant Cauchy sequence of $\mathrm{abv}$ and $x_{5}$ is an element of $\mathrm{CauSeq}$ applied to $x_{1}$ and $\mathrm{abv}$ defined as the function that maps $x_{6}$ to $x_{5}$.
CauSeq.invdefMathlib.Algebra.Order.CauSeq.Basic, function or constantWording
the inverse of f and hf (from the name)
English
Let $f$ be an element of $\mathrm{CauSeq}$ applied to $x_{1}$ and $\mathrm{abv}$ such that $f$ is not a limit zero. Then the inverse of $f$ and $\mathrm{hf}$ is an element of $\mathrm{CauSeq}$ applied to $x_{1}$ and $\mathrm{abv}$ defined as the function that maps $j$ to $\operatorname{inv}$ applied to $j$.
CauSeq.ofEqdefMathlib.Algebra.Order.CauSeq.Basic, function or constantEnglish
Let $f$ be an element of $\mathrm{CauSeq}$ applied to $x_{1}$ and $\mathrm{abv}$. Let $g$ be a function from natural numbers to elements of $x_{1}$ such that for all natural numbers $i$, $\EqtMACRoH {i}{g (i)}$. Then $\operatorname{ofEq}$ applied to $f$, $g$ and $e$ is an element of $\mathrm{CauSeq}$ applied to $x_{1}$ and $\mathrm{abv}$ defined as $g$.
IsCauSeqdefMathlib.Algebra.Order.CauSeq.Basic, predicateEnglish
Let $\mathrm{abv}$ be a function from elements of $x_{3}$ to elements of $x$. Let $f$ be a function from natural numbers to elements of $x_{3}$. Then $\mathrm{IsCauSeq}$ holds for $\mathrm{abv}$ and $f$, if for all elements $x_{5}$ of $x$, if $x_{5} > 0$, then there exists a natural number $i$, such that for all natural numbers $j$, if $j \geq i$, then $\mathrm{abv} (f (j)- f (i))< x_{5}$.
CauSeq.Completion.CauchydefMathlib.Algebra.Order.CauSeq.Completion, typeEnglish
Let $\mathrm{abv}$ be a function from elements of $x_{3}$ to elements of $x$. Then an element of $\operatorname{Cauchy}$ applied to $\mathrm{abv}$ is an element of the function that maps $\mathrm{abv}$ to $\mathrm{Quotient}$ applied to $\operatorname{equiv}$.
CauSeq.Completion.mkdefMathlib.Algebra.Order.CauSeq.Completion, function or constantEnglish
Let $x_{5}$ be an element of $\mathrm{CauSeq}$ applied to $x_{3}$ and $\mathrm{abv}$. Then $\operatorname{mk}$ applied to $x_{5}$ is an element of $\operatorname{Cauchy}$ applied to $\mathrm{abv}$ defined as $\operatorname{mk''}$ applied to $x_{5}$.
CauSeq.Completion.ofRatdefMathlib.Algebra.Order.CauSeq.Completion, function or constantWording
the map from the original ring into the Cauchy completion of x5 (from the docstring)
English
Let $x_{5}$ be an element of $x_{3}$. Then the map from the original ring into the Cauchy completion of $x_{5}$ is an element of $\operatorname{Cauchy}$ applied to $\mathrm{abv}$ defined as $\operatorname{mk}$ applied to the constant Cauchy sequence of $\mathrm{abv}$ and $x_{5}$.
CauSeq.Completion.ofRatRingHomdefMathlib.Algebra.Order.CauSeq.Completion, function or constantWording
the completion (from the name)
English
The completion is a ring homomorphism of $x_{3}$ and $\operatorname{Cauchy}$ applied to $\mathrm{abv}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofRat}$ and $\mathrm{CauSeq\_\_Completion\_\_ofRat\_one}$ and $\mathrm{CauSeq\_\_Completion\_\_ofRat\_mul}$, $\mathrm{CauSeq\_\_Completion\_\_ofRat\_zero}$ and $\mathrm{CauSeq\_\_Completion\_\_ofRat\_add}$.
CauSeq.IsCompleteclassMathlib.Algebra.Order.CauSeq.Completion, predicateWording
abv is complete (from the name)
English
Let $x_{3}$ be a set. Let $\mathrm{abv}$ be a function from elements of $x_{3}$ to elements of $x$. Then we can say that $\mathrm{abv}$ is complete.
CauSeq.limdefMathlib.Algebra.Order.CauSeq.Completion, function or constantWording
the limit of a Cauchy sequence of s (from the docstring)
English
Let $s$ be an element of $\mathrm{CauSeq}$ applied to $x_{3}$ and $\mathrm{abv}$. Then the limit of a Cauchy sequence of $s$ is an element of $x_{3}$ defined as $\operatorname{choose}$ applied to $\operatorname{complete}$ applied to $s$.
ConditionallyCompleteLinearOrderedField.inducedAddHomdefMathlib.Algebra.Order.CompleteField, function or constantWording
the induced additive homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the induced additive homomorphism of $x$ and $x_{1}$ is an additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inducedMap}$ and $\mathrm{ConditionallyCompleteLinearOrderedField\_\_inducedMap\_zero}$ applied to $x$ and $x_{1}$ and $\mathrm{ConditionallyCompleteLinearOrderedField\_\_inducedMap\_add}$ applied to $x$ and $x_{1}$.
ConditionallyCompleteLinearOrderedField.inducedMapdefMathlib.Algebra.Order.CompleteField, function or constantWording
the induced map of x6 (from the name)
English
Let $x$ and $x_{1}$ be sets. Let $x_{6}$ be an element of $x$. Then the induced map of $x_{6}$ is an element of $x_{1}$ defined as the supremum of the cut map of $x_{1}$ and $x_{6}$.
ConditionallyCompleteLinearOrderedField.inducedOrderRingHomdefMathlib.Algebra.Order.CompleteField, function or constantWording
the induced order ring homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the induced order ring homomorphism of $x$ and $x_{1}$ is an order ring homomorphism of $x$ and $x_{1}$.
ConditionallyCompleteLinearOrderedField.inducedOrderRingIsodefMathlib.Algebra.Order.CompleteField, function or constantWording
the induced order ring isomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the induced order ring isomorphism of $x$ and $x_{1}$ is an order ring isomorphism of $x$ and $x_{1}$.
LinearOrderedField.cutMapdefMathlib.Algebra.Order.CompleteField, function or constantWording
the cut map of x1 and a (from the name)
English
Let $x_{1}$ be a set. Let $a$ be an element of $x$. Then the cut map of $x_{1}$ and $a$ is an element of $\wp x_{1}$ defined as the image of $\operatorname{cast}$ and $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Lt} (\operatorname{cast} (t), a)$.
Nat.disjointedRecdefMathlib.Algebra.Order.Disjointed, function or constantEnglish
Let $\mathrm{hdiff}$ be a function from elements $t$ of $x$ and natural numbers $i$ and elements of $p$ applied to $t$ to elements of $p$ applied to $\operatorname{sdiff}$ applied to $t$ and $f$ applied to $i$. Let $x_{2}$ be an element of $p$ applied to $f$ applied to $n$. Then $\operatorname{disjointedRec}$ applied to $t$, $i$, $\mathrm{hdiff}$ and $x_{2}$ is an element of $p$ applied to $\mathrm{disjointed}$ applied to $f$ and $n$.
FloorRingclassMathlib.Algebra.Order.Floor.Defs, predicateWording
x is a floor ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a floor ring.
FloorRing.ceildefMathlib.Algebra.Order.Floor.Defs, function or constantEnglish
Let $x_{3}$ be an element of $x$. Then $\operatorname{ceil}$ applied to $x_{3}$ is an integer defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{3}$.
FloorRing.floordefMathlib.Algebra.Order.Floor.Defs, function or constantWording
the floor of x3 (from the name)
English
Let $x_{3}$ be an element of $x$. Then the floor of $x_{3}$ is an integer defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.
FloorSemiringclassMathlib.Algebra.Order.Floor.Defs, predicateWording
x is a floor semiring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a floor semiring.
FloorSemiring.ceildefMathlib.Algebra.Order.Floor.Defs, function or constantEnglish
Let $x_{3}$ be an element of $x$. Then $\operatorname{ceil}$ applied to $x_{3}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{3}$.
FloorSemiring.floordefMathlib.Algebra.Order.Floor.Defs, function or constantWording
the floor of x3 (from the name)
English
Let $x_{3}$ be an element of $x$. Then the floor of $x_{3}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.
Int.ceildefMathlib.Algebra.Order.Floor.Defs, function or constantEnglish
Let $x_{4}$ be an element of $x$. Then $\operatorname{ceil}$ applied to $x_{4}$ is an integer defined as $\operatorname{ceil}$ applied to $x_{4}$.
Int.floordefMathlib.Algebra.Order.Floor.Defs, function or constantWording
the floor of x4 (from the name)
English
Let $x_{4}$ be an element of $x$. Then the floor of $x_{4}$ is an integer defined as the floor of $x_{4}$.
Int.fractdefMathlib.Algebra.Order.Floor.Defs, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{fract}$ applied to $a$ is an element of $x$ defined as the difference between $a$ and the floor of $a$.
Nat.ceildefMathlib.Algebra.Order.Floor.Defs, function or constantEnglish
Let $x_{4}$ be an element of $x$. Then $\operatorname{ceil}$ applied to $x_{4}$ is a natural number defined as $\operatorname{ceil}$ applied to $x_{4}$.
Nat.floordefMathlib.Algebra.Order.Floor.Defs, function or constantWording
the floor of x4 (from the name)
English
Let $x_{4}$ be an element of $x$. Then the floor of $x_{4}$ is a natural number defined as the floor of $x_{4}$.
CeilDivclassMathlib.Algebra.Order.Floor.Div, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{CeilDiv}$ holds for $x$ and $x_{1}$.
CeilDiv.ceilDivdefMathlib.Algebra.Order.Floor.Div, function or constantEnglish
Let $x_{7}$ be an element of $x_{1}$. Let $x_{8}$ be an element of $x$. Then $\operatorname{ceilDiv}$ applied to $x_{7}$ and $x_{8}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{7}$ and $x_{8}$.
FloorDivclassMathlib.Algebra.Order.Floor.Div, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{FloorDiv}$ holds for $x$ and $x_{1}$.
FloorDiv.floorDivdefMathlib.Algebra.Order.Floor.Div, function or constantWording
the floor quotient of x7 and x8 (from the name)
English
Let $x_{7}$ be an element of $x_{1}$. Let $x_{8}$ be an element of $x$. Then the floor quotient of $x_{7}$ and $x_{8}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{7}$ and $x_{8}$.
ENat.ceildefMathlib.Algebra.Order.Floor.Extended, function or constantEnglish
Let $x$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{ceil}$ applied to $x$ is a natural number.
ENat.floordefMathlib.Algebra.Order.Floor.Extended, function or constantWording
the floor of x (from the name)
English
Let $x$ be an element of $\mathrm{ENNReal}$. Then the floor of $x$ is a natural number.
AddGroupConestructureMathlib.Algebra.Order.Group.Cone, typeWording
additive group cone of G (from the name)
English
Let $G$ be a set. Then the additive group cones of $G$ are a basic type.
AddGroupCone.nonnegdefMathlib.Algebra.Order.Group.Cone, function or constantEnglish
Let $H$ be a set. Then $\operatorname{nonneg}$ applied to $H$ is an additive group cone of $H$.
AddGroupConeClassclassMathlib.Algebra.Order.Group.Cone, predicateWording
G is a additive group cone class (from the name)
English
Let $S$ be a set. Let $G$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $G$ is an additive group cone class.
GroupConestructureMathlib.Algebra.Order.Group.Cone, typeWording
group cone of G (from the name)
English
Let $G$ be a set. Then the group cones of $G$ are a basic type.
GroupCone.oneLEdefMathlib.Algebra.Order.Group.Cone, function or constantEnglish
Let $H$ be a set. Then $\operatorname{oneLE}$ applied to $H$ is a group cone of $H$.
GroupConeClassclassMathlib.Algebra.Order.Group.Cone, predicateWording
G is a group cone class (from the name)
English
Let $S$ be a set. Let $G$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $G$ is a group cone class.
LinearOrderedAddCommGroup.Subgroup.negGendefMathlib.Algebra.Order.Group.Cyclic, function or constantWording
the negation generator of H (from the name)
English
Let $H$ be an additive subgroup of $G$. Then the negation generator of $H$ is an element of $G$ defined as $\operatorname{choose}$ applied to $\mathrm{LinearOrderedAddCommGroup\_\_Subgroup\_\_exists\_neg\_generator}$ applied to $H$.
LinearOrderedAddCommGroup.negGendefMathlib.Algebra.Order.Group.Cyclic, function or constantWording
the negation generator of G (from the name)
English
Let $G$ be a set. Then the negation generator of $G$ is an element of $G$ defined as the negation generator of the top.
LinearOrderedCommGroup.Subgroup.genLTOnedefMathlib.Algebra.Order.Group.Cyclic, function or constantEnglish
Let $H$ be a subgroup of $G$. Then $\operatorname{genLTOne}$ applied to $H$ is an element of $G$ defined as $\operatorname{choose}$ applied to $\mathrm{LinearOrderedCommGroup\_\_Subgroup\_\_exists\_generator\_lt\_one}$ applied to $H$.
LinearOrderedCommGroup.genLTOnedefMathlib.Algebra.Order.Group.Cyclic, function or constantEnglish
Let $G$ be a set. Then $\operatorname{genLTOne}$ applied to $G$ is an element of $G$ defined as $\operatorname{genLTOne}$ applied to the top.
ofLexAddEquivdefMathlib.Algebra.Order.Group.Equiv, function or constantWording
the lexicographic additive equivalence of x (from the name)
English
Let $x$ be a set. Then the lexicographic additive equivalence of $x$ is an additive equivalence of $\mathrm{Lex}$ applied to $x$ and $x$.
ofLexMulEquivdefMathlib.Algebra.Order.Group.Equiv, function or constantWording
the lexicographic multiplicative equivalence of x (from the name)
English
Let $x$ be a set. Then the lexicographic multiplicative equivalence of $x$ is a multiplicative equivalence of $\mathrm{Lex}$ applied to $x$ and $x$.
toLexAddEquivdefMathlib.Algebra.Order.Group.Equiv, function or constantWording
the lexicographic additive equivalence of x (from the name)
English
Let $x$ be a set. Then the lexicographic additive equivalence of $x$ is an additive equivalence of $x$ and $\mathrm{Lex}$ applied to $x$.
toLexMulEquivdefMathlib.Algebra.Order.Group.Equiv, function or constantWording
the lexicographic multiplicative equivalence of x (from the name)
English
Let $x$ be a set. Then the lexicographic multiplicative equivalence of $x$ is a multiplicative equivalence of $x$ and $\mathrm{Lex}$ applied to $x$.
Multiset.cardHomdefMathlib.Algebra.Order.Group.Multiset, function or constantWording
the cardinality homomorphism (from the name)
English
The cardinality homomorphism is an additive monoid homomorphism of the set of multisets of $x$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{card}$ and $\mathrm{Multiset\_\_card\_zero}$ and $\mathrm{Multiset\_\_card\_add}$.
Multiset.countAddMonoidHomdefMathlib.Algebra.Order.Group.Multiset, function or constantWording
the count additive monoid homomorphism of a (from the name)
English
Let $a$ be an element of $x$. Then the count additive monoid homomorphism of $a$ is an additive monoid homomorphism of the set of multisets of $x$ and $\Natural$ defined as the count additive monoid homomorphism of the function that maps $x_{2}$ to $\EqtMACRoH {a}{x_{2}}$.
Multiset.countPAddMonoidHomdefMathlib.Algebra.Order.Group.Multiset, function or constantWording
the count additive monoid homomorphism of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Then the count additive monoid homomorphism of $p$ is an additive monoid homomorphism of the set of multisets of $x$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{countP}$ applied to $p$ and $\mathrm{Multiset\_\_countP\_zero}$ applied to $p$ and $\mathrm{Multiset\_\_countP\_add}$ applied to $p$.
Multiset.mapAddMonoidHomdefMathlib.Algebra.Order.Group.Multiset, function or constantWording
the map additive monoid homomorphism of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map additive monoid homomorphism of $f$ is an additive monoid homomorphism of the set of multisets of $x$ and the set of multisets of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{map}$ applied to $f$ and $\mathrm{Multiset\_\_map\_zero}$ applied to $f$ and $\mathrm{Multiset\_\_map\_add}$ applied to $f$.
Multiset.replicateAddMonoidHomdefMathlib.Algebra.Order.Group.Multiset, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{replicateAddMonoidHom}$ applied to $a$ is an additive monoid homomorphism of $\Natural$ and the set of multisets of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $n$ to $\operatorname{replicate}$ applied to $n$ and $a$ and $\mathrm{Multiset\_\_replicate\_zero}$ applied to $a$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Multiset\_\_replicate\_add}$ applied to $x_{1}$, $x_{2}$ and $a$.
OrderIso.addLeftdefMathlib.Algebra.Order.Group.OrderIso, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{addLeft}$ applied to $a$ is an order isomorphism of $x$ and $x$.
OrderIso.addRightdefMathlib.Algebra.Order.Group.OrderIso, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{addRight}$ applied to $a$ is an order isomorphism of $x$ and $x$.
OrderIso.divLeftdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the left quotient of a (from the name)
English
Let $a$ be an element of $x$. Then the left quotient of $a$ is an order isomorphism of $x$ and the set of order duals of $x$ defined as $\operatorname{mk}$ applied to the composition of the left quotient of $a$ and the dual and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{div\_le\_div\_iff\_left}$ applied to $a$.
OrderIso.divRightdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the right quotient of a (from the name)
English
Let $a$ be an element of $x$. Then the right quotient of $a$ is an order isomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the right quotient of $a$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{div\_le\_div\_iff\_right}$ applied to $a$.
OrderIso.invdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the inverse of x (from the name)
English
Let $x$ be a set. Then the inverse of $x$ is an order isomorphism of $x$ and the set of order duals of $x$ defined as $\operatorname{mk}$ applied to the composition of the inverse of $x$ and the dual and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{inv\_le\_inv\_iff}$.
OrderIso.mulLeftdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the left multiplicative of a (from the name)
English
Let $a$ be an element of $x$. Then the left multiplicative of $a$ is an order isomorphism of $x$ and $x$.
OrderIso.mulRightdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the right multiplicative of a (from the name)
English
Let $a$ be an element of $x$. Then the right multiplicative of $a$ is an order isomorphism of $x$ and $x$.
OrderIso.negdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the negation of x (from the name)
English
Let $x$ be a set. Then the negation of $x$ is an order isomorphism of $x$ and the set of order duals of $x$ defined as $\operatorname{mk}$ applied to the composition of the negation of $x$ and the dual and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{neg\_le\_neg\_iff}$.
OrderIso.subLeftdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the left difference of a (from the name)
English
Let $a$ be an element of $x$. Then the left difference of $a$ is an order isomorphism of $x$ and the set of order duals of $x$ defined as $\operatorname{mk}$ applied to the composition of the left difference of $a$ and the dual and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{sub\_le\_sub\_iff\_left}$ applied to $a$.
OrderIso.subRightdefMathlib.Algebra.Order.Group.OrderIso, function or constantWording
the right difference of a (from the name)
English
Let $a$ be an element of $x$. Then the right difference of $a$ is an order isomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the right difference of $a$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{sub\_le\_sub\_iff\_right}$ applied to $a$.
Subgroup.topOrderMonoidIsodefMathlib.Algebra.Order.Group.Subgroup, function or constantWording
the order preserving isomorphism from the top subgroup to the group of G (from the docstring)
English
Let $G$ be a set. Then the order preserving isomorphism from the top subgroup to the group of $G$ is an order monoid isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{2}})}$ and $G$.
LatticeOrderedAddCommGroup.IsSoliddefMathlib.Algebra.Order.Group.Unbundled.Abs, predicateWording
s is solid (from the name)
English
Let $s$ be an element of $\wp x$. Then $s$ is solid, if for all elements $x_{3}$ of $x$, if $x_{3}$ is an element of $s$, then for all elements $y$ of $x$, if the absolute value of $y$ is less than or equal to the absolute value of $x_{3}$, then $y$ is an element of $s$.
LatticeOrderedAddCommGroup.solidClosuredefMathlib.Algebra.Order.Group.Unbundled.Abs, function or constantWording
the solid closure of s (from the docstring)
English
Let $s$ be an element of $\wp x$. Then the solid closure of $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that there exists an element $x_{3}$ of $x$, such that $x_{3}$ is an element of $s$ and the absolute value of $y$ is less than or equal to the absolute value of $x_{3}$.
absdefMathlib.Algebra.Order.Group.Unbundled.Abs, function or constantWording
the absolute value of a (from the name)
English
Let $a$ be an element of $x$. Then the absolute value of $a$ is an element of $x$ defined as $\MaxmaxMACRoAF {a}{\operatorname{neg} (a)}$.
mabsdefMathlib.Algebra.Order.Group.Unbundled.Abs, function or constantEnglish
Let $a$ be an element of $x$. Then $\mathrm{mabs}$ applied to $a$ is an element of $x$ defined as $\MaxmaxMACRoAF {a}{\operatorname{inv} (a)}$.
LinearOrderedCommGroupWithZeroclassMathlib.Algebra.Order.GroupWithZero.Canonical, predicateWording
x is a linear ordered commutative group with zero (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a linear ordered commutative group with zero.
LinearOrderedCommMonoidWithZeroclassMathlib.Algebra.Order.GroupWithZero.Canonical, predicateWording
x is a linear ordered commutative monoid with zero (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a linear ordered commutative monoid with zero.
WithZero.expOrderIsodefMathlib.Algebra.Order.GroupWithZero.Canonical, function or constantWording
the exponential map (from the docstring)
English
The exponential map is an order isomorphism of $G$ and the set of units of $\mathrm{WithZero}$ applied to the set of multiplicatives of $G$.
WithZero.logOrderIsodefMathlib.Algebra.Order.GroupWithZero.Canonical, function or constantWording
the logarithm (from the docstring)
English
The logarithm is an order isomorphism of the set of units of $\mathrm{WithZero}$ applied to the set of multiplicatives of $G$ and $G$.
MulPosMonoclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{MulPosMono}$ holds for $x$.
MulPosReflectLEclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{MulPosReflectLE}$ holds for $x$.
MulPosReflectLTclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{MulPosReflectLT}$ holds for $x$.
MulPosStrictMonoclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{MulPosStrictMono}$ holds for $x$.
PosMulMonoclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{PosMulMono}$ holds for $x$.
PosMulReflectLEclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{PosMulReflectLE}$ holds for $x$.
PosMulReflectLTclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{PosMulReflectLT}$ holds for $x$.
PosMulStrictMonoclassMathlib.Algebra.Order.GroupWithZero.Defs, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{PosMulStrictMono}$ holds for $x$.
LinearOrderedCommGroupWithZero.fstdefMathlib.Algebra.Order.GroupWithZero.Lex, function or constantWording
the first component of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is an order monoid with zero homomorphism of $\mathrm{WithZero}$ applied to $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ and $x$.
LinearOrderedCommGroupWithZero.inldefMathlib.Algebra.Order.GroupWithZero.Lex, function or constantWording
the left injection of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is an order monoid with zero homomorphism of $x$ and $\mathrm{WithZero}$ applied to $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$.
LinearOrderedCommGroupWithZero.inrdefMathlib.Algebra.Order.GroupWithZero.Lex, function or constantWording
the right injection of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is an order monoid with zero homomorphism of $x_{1}$ and $\mathrm{WithZero}$ applied to $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$.
OrderIso.divRight₀defMathlib.Algebra.Order.GroupWithZero.OrderIso, function or constantWording
the right quotient of a and ha (from the name)
English
Let $a$ be an element of $x$ such that $0 < a$. Then the right quotient of $a$ and $\mathrm{ha}$ is an order isomorphism of $x$ and $x$.
OrderIso.mulLeft₀defMathlib.Algebra.Order.GroupWithZero.OrderIso, function or constantWording
the left multiplicative of a and ha (from the name)
English
Let $a$ be an element of $x$ such that $0 < a$. Then the left multiplicative of $a$ and $\mathrm{ha}$ is an order isomorphism of $x$ and $x$.
OrderIso.mulRight₀defMathlib.Algebra.Order.GroupWithZero.OrderIso, function or constantWording
the right multiplicative of a and ha (from the name)
English
Let $a$ be an element of $x$ such that $0 < a$. Then the right multiplicative of $a$ and $\mathrm{ha}$ is an order isomorphism of $x$ and $x$.
MonoidWithZeroHom.ValueGroup₀.orderMonoidWithZeroHomdefMathlib.Algebra.Order.GroupWithZero.Range, function or constantWording
the order monoid with zero homomorphism of f (from the name)
English
Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Then the order monoid with zero homomorphism of $f$ is an order monoid with zero homomorphism of the set of value groups of $f$ and $\mathrm{WithZero}$ applied to $\UnitsMACRoAO {B}$.
Submonoid.posdefMathlib.Algebra.Order.GroupWithZero.Submonoid, function or constantWording
the positive part of x (from the name)
English
Let $x$ be a set. Then the positive part of $x$ is a submonoid of $x$.
OrderIso.withZeroUnitsdefMathlib.Algebra.Order.GroupWithZero.WithZero, function or constantEnglish
$\operatorname{withZeroUnits}$ is an order isomorphism of $\mathrm{WithZero}$ applied to $\UnitsMACRoAO {x}$ and $x$.
MulLEAddHomClassclassMathlib.Algebra.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulLEAddHomClass}$ holds for $F$, $x$ and $x_{1}$.
NonarchimedeanHomClassclassMathlib.Algebra.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{NonarchimedeanHomClass}$ holds for $F$, $x$ and $x_{1}$.
NonnegHomClassclassMathlib.Algebra.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{NonnegHomClass}$ holds for $F$, $x$ and $x_{1}$.
SubadditiveHomClassclassMathlib.Algebra.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SubadditiveHomClass}$ holds for $F$, $x$ and $x_{1}$.
SubmultiplicativeHomClassclassMathlib.Algebra.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SubmultiplicativeHomClass}$ holds for $F$, $x$ and $x_{1}$.
AddGroupNormClassclassMathlib.Algebra.Order.Hom.GroupNorm, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{AddGroupNormClass}$ holds for $F$, $x$ and $x_{1}$.
AddGroupSeminormClassclassMathlib.Algebra.Order.Hom.GroupNorm, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{AddGroupSeminormClass}$ holds for $F$, $x$ and $x_{1}$.
GroupNormClassclassMathlib.Algebra.Order.Hom.GroupNorm, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{GroupNormClass}$ holds for $F$, $x$ and $x_{1}$.
GroupSeminormClassclassMathlib.Algebra.Order.Hom.GroupNorm, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{GroupSeminormClass}$ holds for $F$, $x$ and $x_{1}$.