Definitions: Mathlib.Algebra, part 16 of 17

sequence of R (from the name)

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

the basis of S and hCoeff (from the name)

Let $S$ be a sequence of $R$ such that for all natural numbers $i$, the leading coefficient of $\operatorname{elems'}$ applied to $S$ and $i$ is a unit. Then the basis of $S$ and $\mathrm{hCoeff}$ is a basis of $R$ and the set of polynomials of $R$.

Let $\mathrm{self}$ be a sequence of $R$. Let $x_{1}$ be a natural number. Then $\operatorname{elems'}$ applied to $\mathrm{self}$ and $x_{1}$ is a polynomial of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

Let $p$ be a polynomial of $R$. Let $x_{4}$ be an element of $S$. Then $\operatorname{smeval}$ applied to $p$ and $x_{4}$ is an element of $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{Polynomial\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_Polynomial\_\_Smeval\_\_3997496041\_\_\_hygCtx\_\_\_hyg\_\_2}$, $p$ and $x_{4}$.

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

Let $R$ be a set. Let $x_{4}$ be an element of $S$. Then the linear map of $R$ and $x_{4}$ is a linear map of the set of polynomials of $R$ and $S$.

the scalar multiple power of x5 and x6 (from the name)

Let $x_{4}$ be an element of $S$. Let $x_{5}$ be a natural number. Let $x_{6}$ be an element of $R$. Then the scalar multiple power of $x_{5}$ and $x_{6}$ is an element of $S$ defined as $\HSMulhSMulMACRoAL {x_{6}}{(x_{4} ^ {x_{5}})}$.

Let $f$ be a polynomial of $R$. Then $\operatorname{Splits}$ holds for $f$, if $f$ is an element of the closure of $\UnionunionMACRoAB {\operatorname{ofPred} (\lambda x_{1} . \mathrm{exists} (R , \lambda a . \EqtMACRoH {\operatorname{C} (a)}{x_{1}}))}{\operatorname{ofPred} (\lambda x_{2} . \mathrm{exists} (R , \lambda a_{1} . \EqtMACRoH {(\operatorname{X} + \operatorname{C} (a_{1}))}{x_{2}}))}$.

the root of hf and hfd (from the name)

Assume that $\operatorname{Splits}$ holds for $f$. Assume that the degree of $f$ is distinct from $0$. Then the root of $\mathrm{hf}$ and $\mathrm{hfd}$ is an element of $R$ defined as $\operatorname{choose}$ applied to $\mathrm{Polynomial\_\_Splits\_\_exists\_eval\_eq\_zero}$ applied to $\mathrm{hf}$ and $\mathrm{hfd}$.

the Sturm sequence of p and q (from the name)

Let $p$ and $q$ be polynomials of $K$. Then the Sturm sequence of $p$ and $q$ is a list of polynomials of $K$ defined as $\mathrm{Polynomial\_\_sturmSeq\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $p$ and $q$.

the sum derivative (from the name)

The sum derivative is a linear map of the set of polynomials of $R$ and the set of polynomials of $R$ defined as the composition of $\operatorname{lsum}$ applied to $\Natural$ and the function that maps $x_{2}$ to the identity and the derivative finitely supported function.

the Taylor expansion of r (from the docstring)

Let $r$ be an element of $R$. Then the Taylor expansion of $r$ is a linear map of the set of polynomials of $R$ and the set of polynomials of $R$.

the Taylor algebra homomorphism of r (from the name)

Let $r$ be an element of $R$. Then the Taylor algebra homomorphism of $r$ is an algebra homomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

the Taylor equivalence of r (from the name)

Let $r$ be an element of $R$. Then the Taylor equivalence of $r$ is an algebra isomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

Let $p$ be a polynomial of $\Integer$. Then $\operatorname{IsUnitTrinomial}$ holds for $p$, if there exist elements $k$, $m$ and $n$ of $\Natural$, such that there exists an element $h$ of $\mathrm{Lt} (k , m)$, such that there exists an element $h_{1}$ of $\mathrm{Lt} (m , n)$, such that there exist units $u$, $v$ and $w$ of $\Integer$, such that $p$ is equal to $\operatorname{trinomial}$ applied to $k$, $m$, $n$, the underlying value in the base of $u$, the underlying value in the base of $v$ and the underlying value in the base of $w$.

Let $k$, $m$ and $n$ be natural numbers. Let $u$, $v$ and $w$ be elements of $R$. Then $\operatorname{trinomial}$ applied to $k$, $m$, $n$, $u$, $v$ and $w$ is a polynomial of $R$ defined as $\operatorname{C} (u)\times \operatorname{X} ^ {k}+ \operatorname{C} (v)\times \operatorname{X} ^ {m}+ \operatorname{C} (w)\times \operatorname{X} ^ {n}$.

presented additive monoid of rels (from the name)

Let $\mathrm{rels}$ be a function from free additive monoids of $x$ and free additive monoids of $x$ to propositions. Then a presented additive monoid of $\mathrm{rels}$ is an element of the function that maps $\mathrm{rels}$ to the set of quotients of the additive congruence relation generator of $\mathrm{rels}$.

the lift of f and h (from the name)

Let $f$ be a function from elements of $x$ to elements of $M$ such that for all free additive monoids $a$ and $b$ of $x$, if $\mathrm{rels}$ holds for $a$ and $b$, then $\operatorname{coe}$ applied to the lift, $f$ and $a$ is equal to $\operatorname{coe}$ applied to the lift, $f$ and $b$. Then the lift of $f$ and $h$ is an additive monoid homomorphism of the set of presented additive monoids of $\mathrm{rels}$ and $M$.

Let $\mathrm{rels}$ be a function from free additive monoids of $x$ and free additive monoids of $x$ to propositions. Then $\operatorname{mk}$ applied to $\mathrm{rels}$ is an additive monoid homomorphism of the set of free additive monoids of $x$ and the set of presented additive monoids of $\mathrm{rels}$.

Let $\mathrm{rels}$ be a function from free additive monoids of $x$ and free additive monoids of $x$ to propositions. Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $\mathrm{rels}$ and $x_{1}$ is a presented additive monoid of $\mathrm{rels}$ defined as $\operatorname{mk}$ applied to $\mathrm{rels}$ and $\operatorname{of}$ applied to $x_{1}$.

presented monoid of rels (from the name)

Let $\mathrm{rels}$ be a function from free monoids of $x$ and free monoids of $x$ to propositions. Then a presented monoid of $\mathrm{rels}$ is an element of the function that maps $\mathrm{rels}$ to the set of quotients of the congruence relation generator of $\mathrm{rels}$.

the lift of f and h (from the name)

Let $f$ be a function from elements of $x$ to elements of $M$ such that for all free monoids $a$ and $b$ of $x$, if $\mathrm{rels}$ holds for $a$ and $b$, then $\operatorname{coe}$ applied to the lift, $f$ and $a$ is equal to $\operatorname{coe}$ applied to the lift, $f$ and $b$. Then the lift of $f$ and $h$ is a monoid homomorphism of the set of presented monoids of $\mathrm{rels}$ and $M$.

Let $\mathrm{rels}$ be a function from free monoids of $x$ and free monoids of $x$ to propositions. Then $\operatorname{mk}$ applied to $\mathrm{rels}$ is a monoid homomorphism of the set of free monoids of $x$ and the set of presented monoids of $\mathrm{rels}$.

Let $\mathrm{rels}$ be a function from free monoids of $x$ and free monoids of $x$ to propositions. Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $\mathrm{rels}$ and $x_{1}$ is a presented monoid of $\mathrm{rels}$ defined as $\operatorname{mk}$ applied to $\mathrm{rels}$ and $\operatorname{of}$ applied to $x_{1}$.

p is prime (by hand)

Let $p$ be an element of $M$. Then $p$ is prime, if $p \neq 0$, $p$ is not a unit and for all elements $a$ of $M$, for all elements $b$ of $M$, if $p$ divides $a \times b$, then $p$ divides $a$ or $p$ divides $b$.

the base change of S (from the docstring)

Let $S$ be a set. Let $a$ and $b$ be elements of $R$. Then the base change of $S$ is an algebra isomorphism of the set of tensor products of $S$ and the set of quadratic algebras of $a$ and $b$ and the set of quadratic algebras of $\operatorname{algebraMap}$ applied to $R$, $S$ and $a$ and $\operatorname{algebraMap}$ applied to $R$, $S$ and $b$ defined as the equivalence of the set of quadratic algebras of $a$ and $b$ and the set of quadratic algebras of $\operatorname{algebraMap}$ applied to $R$, $S$ and $a$ and $\operatorname{algebraMap}$ applied to $R$, $S$ and $b$.

the base change of a and b (from the name)

Let $S$ be a set. Let $a$ and $b$ be elements of $R$. Then the base change of $a$ and $b$ is an algebra homomorphism of the set of quadratic algebras of $a$ and $b$ and the set of quadratic algebras of $\operatorname{algebraMap}$ applied to $R$, $S$ and $a$ and $\operatorname{algebraMap}$ applied to $R$, $S$ and $b$.

the change generator of u and k (from the name)

Let $a$, $b$, $u$ and $k$ be elements of $R$ such that $\EqtMACRoH {\mathrm{a'}}{u ^ {2}\times a - u \times b \times k - k ^ {2}}$ and $\EqtMACRoH {\mathrm{b'}}{u \times b + 2 \times k}$. Then the change generator of $u$ and $k$ is an algebra homomorphism of the set of quadratic algebras of $\mathrm{a'}$ and $\mathrm{b'}$ and the set of quadratic algebras of $a$ and $b$ defined as $\operatorname{lift}$ applied to $\HSMulhSMulMACRoAL {u}{\operatorname{omega}}+ \operatorname{algebraMap} (R , \mathrm{QuadraticAlgebra} (a , b), k)$.

the change generator equivalence of u and k (from the name)

Let $a$, $b$ and $k$ be elements of $R$. Let $u$ be a unit of $R$ such that $\mathrm{a'}$ is equal to the difference between the difference between the product of the exponentiation of the underlying value in the base of $u$ to $2$ and $a$ and the product of the product of the underlying value in the base of $u$ and $b$ and $k$ and $k ^ {2}$ and $\mathrm{b'}$ is equal to the sum of the product of the underlying value in the base of $u$ and $b$ and $2 \times k$. Then the change generator equivalence of $u$ and $k$ is an algebra isomorphism of the set of quadratic algebras of $\mathrm{a'}$ and $\mathrm{b'}$ and the set of quadratic algebras of $a$ and $b$.

the lift (from the name)

The lift is an equivalence from $\SubtypeSet {u}{(\EqtMACRoH {(u \times u)}{(\HSMulhSMulMACRoAL {a}{1}+ \HSMulhSMulMACRoAL {b}{u})})}$ to the set of algebra homomorphisms of the set of quadratic algebras of $a$ and $b$ and $A$.

the map ring homomorphism of a and b (from the name)

Let $f$ be a ring homomorphism of $R$ and $S$. Let $a$ and $b$ be elements of $R$. Then the map ring homomorphism of $a$ and $b$ is a ring homomorphism of the set of quadratic algebras of $a$ and $b$ and the set of quadratic algebras of $f$ applied to $a$ and $f$ applied to $b$.

the norm (from the name)

The norm is a monoid homomorphism of the set of quadratic algebras of $a$ and $b$ and $R$.

the omega (from the name)

The omega is a quadratic algebra of $a$ and $b$ defined as $\operatorname{mk}$ applied to $0$ and $1$.

the trace (from the name)

The trace is a linear map of the set of quadratic algebras of $a$ and $b$ and $R$.

quadratic algebra of a and b (from the name)

Let $R$ be a set. Let $a$ and $b$ be elements of $R$. Then the quadratic algebras of $a$ and $b$ are a basic type.

Let $x_{1}$ be an element of $R$. Then $\operatorname{C}$ applied to $x_{1}$ is a quadratic algebra of $a$ and $b$ defined as $\operatorname{mk}$ applied to $x_{1}$ and $0$.

the basis of a and b (from the name)

Let $a$ and $b$ be elements of $R$. Then the basis of $a$ and $b$ is a basis of $R$ and the set of quadratic algebras of $a$ and $b$ defined as the basis of the linear equivalence tuple of $a$ and $b$.

the equivalence product of a and b (from the name)

Let $a$ and $b$ be elements of $R$. Then the equivalence product of $a$ and $b$ is an equivalence from the set of quadratic algebras of $a$ and $b$ to $\mathrm{Prod}$ applied to $R$ and $R$.

the imaginary part of self (from the name)

Let $\mathrm{self}$ be a quadratic algebra of $a$ and $b$. Then the imaginary part of $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the imaginary part of a and b (from the name)

Let $a$ and $b$ be elements of $R$. Then the imaginary part of $a$ and $b$ is a linear map of the set of quadratic algebras of $a$ and $b$ and $R$.

the linear equivalence tuple of a and b (from the name)

Let $a$ and $b$ be elements of $R$. Then the linear equivalence tuple of $a$ and $b$ is a linear equivalence of the set of quadratic algebras of $a$ and $b$ and the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $R$.

the real part of self (from the name)

Let $\mathrm{self}$ be a quadratic algebra of $a$ and $b$. Then the real part of $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the real part of a and b (from the name)

Let $a$ and $b$ be elements of $R$. Then the real part of $a$ and $b$ is a linear map of the set of quadratic algebras of $a$ and $b$ and $R$.

Let $a$ and $b$ be elements of $R$. Then $\operatorname{algEquivDiscrZero}$ applied to $a$ and $b$ is an algebra isomorphism of the set of quadratic algebras of $a$ and $b$ and the set of quadratic algebras of the discriminant of the quadratic algebra of $a$ and $b$ and $0$.

Let $a$ and $b$ be integers. Then $\operatorname{algEquivEdivEmod}$ applied to $a$ and $b$ is an algebra isomorphism of the set of quadratic algebras of $a$ and $b$ and the set of quadratic algebras of the quotient of the discriminant of the quadratic algebra of $a$ and $b$ and $4$ and the remainder of the discriminant of the quadratic algebra of $a$ and $b$ modulo $4$.

the discriminant of the quadratic algebra of a and b (from the docstring)

Let $a$ and $b$ be elements of $R$. Then the discriminant of the quadratic algebra of $a$ and $b$ is an element of $R$ defined as $b ^ {2}+ 4 \times a$.

Let $a$, $b$ and $c$ be elements of $R$. Then $\mathrm{discrim}$ applied to $a$, $b$ and $c$ is an element of $R$ defined as $b ^ {2}- 4 \times a \times c$.

x is a quandle (from the name)

Let $x$ be a set. Then we can say that $x$ is a quandle.

conjugate of G (from the name)

Let $G$ be a set. Then a conjugate of $G$ is an element of the function that maps $G$ to $G$.

the map of f (from the name)

Let $f$ be a monoid homomorphism of $G$ and $H$. Then the map of $f$ is an element of $\mathrm{ShelfHom}$ applied to the set of conjugates of $G$ and the set of conjugates of $H$.

dihedral of n (from the name)

Let $n$ be a natural number. Then a dihedral of $n$ is an element of the function that maps $n$ to $\mathrm{ZMod}$ applied to $n$.

Let $n$ be a natural number. Let $a$ and $x$ be elements of $\mathrm{ZMod}$ applied to $n$. Then $\operatorname{dihedralAct}$ applied to $n$, $a$ and $x$ is an element of $\mathrm{ZMod}$ applied to $n$ defined as $2 \times a - x$.

Let $x$ be a set. Then we can say that $\mathrm{Rack}$ holds for $x$.

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

R is Abelian (from the name)

Let $R$ be a set. Then $R$ is Abelian, if for all elements $x_{1}$, $y$, $z$ and $w$ of $R$, $\EqtMACRoH {\operatorname{act} (\operatorname{act} (x_{1} , y), \operatorname{act} (z , w))}{\operatorname{act} (\operatorname{act} (x_{1} , z), \operatorname{act} (y , w))}$.

Let $R$ be a set. Then $\operatorname{IsInvolutory}$ holds for $R$, if for all elements $x_{1}$ of $R$, $\operatorname{act}$ applied to $x_{1}$ is involutive.

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

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the unit and $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $R$ to elements of $\mathrm{motive}$ applied to the inclusion of $x$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $a$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $b$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to the product of $a$ and $b$ and $\mathrm{PULift}$ applied to the set of functions from elements $a_{1}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to the inverse of $a_{1}$.

the inclusion of x (from the name)

Let $x$ be an element of $R$. Then the inclusion of $x$ is an element of $\operatorname{PreEnvelGroup}$ applied to $R$.

the inverse of a (from the name)

Let $a$ be an element of $\operatorname{PreEnvelGroup}$ applied to $R$. Then the inverse of $a$ is an element of $\operatorname{PreEnvelGroup}$ applied to $R$.

the product of a and b (from the name)

Let $a$ and $b$ be elements of $\operatorname{PreEnvelGroup}$ applied to $R$. Then the product of $a$ and $b$ is an element of $\operatorname{PreEnvelGroup}$ applied to $R$.

the unit (from the name)

The unit is an element of $\operatorname{PreEnvelGroup}$ applied to $R$.

Let $R$ be a set. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{PreEnvelGroup}$ applied to $R$. Then we can say that $\operatorname{PreEnvelGroupRel}$ holds for $R$, $x_{1}$ and $x_{2}$.

Let $R$ be a set. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{PreEnvelGroup}$ applied to $R$. Then the elements of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $x_{1}$ and $x_{2}$ are a basic type.

Let $x_{1}$ and $y$ be elements of $R$. Then $\mathrm{Rack\_\_PreEnvelGroupRel'\_\_act\_incl}$ applied to $x_{1}$ and $y$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the product of the product of the inclusion of $x_{1}$ and the inclusion of $y$ and the inverse of the inclusion of $x_{1}$ and the inclusion of $\operatorname{act}$ applied to $x_{1}$ and $y$.

the associator of b and c (from the name)

Let $a$, $b$ and $c$ be elements of $\operatorname{PreEnvelGroup}$ applied to $R$. Then the associator of $b$ and $c$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the product of the product of $a$ and $b$ and $c$ and the product of $a$ and the product of $b$ and $c$.

the congruence inverse of ha (from the name)

Let $\mathrm{ha}$ be an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a$ and $\mathrm{a'}$. Then the congruence inverse of $\mathrm{ha}$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the inverse of $a$ and the inverse of $\mathrm{a'}$.

the congruence product of ha and hb (from the name)

Let $\mathrm{ha}$ be an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a$ and $\mathrm{a'}$. Let $\mathrm{hb}$ be an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $b$ and $\mathrm{b'}$. Then the congruence product of $\mathrm{ha}$ and $\mathrm{hb}$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the product of $a$ and $b$ and the product of $\mathrm{a'}$ and $\mathrm{b'}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $a$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to $a$, $a$ and the identity and $\mathrm{PULift}$ applied to the set of functions from elements $a_{1}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $b$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{hab}$ of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a_{1}$ and $b$ to elements of $\mathrm{motive}$ applied to $b$, $a_{1}$ and the inverse of $\mathrm{hab}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $a_{2}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $b_{1}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $c$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{hab1}$ of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a_{2}$ and $b_{1}$ and elements $\mathrm{hbc}$ of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $b_{1}$ and $c$ to elements of $\mathrm{motive}$ applied to $a_{2}$, $c$ and the composition of $\mathrm{hab1}$ and $\mathrm{hbc}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from elements $a_{3}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $b_{2}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{a'}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{b'}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{ha}$ of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a_{3}$ and $\mathrm{a'}$ and elements $\mathrm{hb}$ of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $b_{2}$ and $\mathrm{b'}$ to elements of $\mathrm{motive}$ applied to the product of $a_{3}$ and $b_{2}$, the product of $\mathrm{a'}$ and $\mathrm{b'}$ and the congruence product of $\mathrm{ha}$ and $\mathrm{hb}$ and $\mathrm{PULift}$ applied to the set of functions from elements $a_{4}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{a'1}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $\mathrm{ha1}$ of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a_{4}$ and $\mathrm{a'1}$ to elements of $\mathrm{motive}$ applied to the inverse of $a_{4}$, the inverse of $\mathrm{a'1}$ and the congruence inverse of $\mathrm{ha1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $6$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $5$, $\mathrm{PULift}$ applied to the set of functions from elements $a_{5}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $b_{3}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ and elements $c_{1}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to the product of the product of $a_{5}$ and $b_{3}$ and $c_{1}$, the product of $a_{5}$ and the product of $b_{3}$ and $c_{1}$ and the associator of $b_{3}$ and $c_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $a_{6}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to the product of the unit and $a_{6}$, $a_{6}$ and the one product of $a_{6}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $7$, $\mathrm{PULift}$ applied to the set of functions from elements $a_{7}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to the product of $a_{7}$ and the unit, $a_{7}$ and the multiplicative one of $a_{7}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $8$, $\mathrm{PULift}$ applied to the set of functions from elements $a_{8}$ of $\operatorname{PreEnvelGroup}$ applied to $R$ to elements of $\mathrm{motive}$ applied to the product of the inverse of $a_{8}$ and $a_{8}$, the unit and $\mathrm{Rack\_\_PreEnvelGroupRel'\_\_inv\_mul\_cancel}$ applied to $a_{8}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $R$ and elements $y$ of $R$ to elements of $\mathrm{motive}$ applied to the product of the product of the inclusion of $x_{1}$ and the inclusion of $y$ and the inverse of the inclusion of $x_{1}$, the inclusion of $\operatorname{act}$ applied to $x_{1}$ and $y$ and $\mathrm{Rack\_\_PreEnvelGroupRel'\_\_act\_incl}$ applied to $x_{1}$ and $y$.

Let $a$ be an element of $\operatorname{PreEnvelGroup}$ applied to $R$. Then $\mathrm{Rack\_\_PreEnvelGroupRel'\_\_inv\_mul\_cancel}$ applied to $a$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the product of the inverse of $a$ and $a$ and the unit.

the multiplicative one of a (from the name)

Let $a$ be an element of $\operatorname{PreEnvelGroup}$ applied to $R$. Then the multiplicative one of $a$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the product of $a$ and the unit and $a$.

the one product of a (from the name)

Let $a$ be an element of $\operatorname{PreEnvelGroup}$ applied to $R$. Then the one product of $a$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, the product of the unit and $a$ and $a$.

the identity (from the name)

The identity is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a$ and $a$.

the inverse of hab (from the name)

Let $\mathrm{hab}$ be an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a$ and $b$. Then the inverse of $\mathrm{hab}$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $b$ and $a$.

the composition of hab and hbc (from the name)

Let $\mathrm{hab}$ be an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a$ and $b$. Let $\mathrm{hbc}$ be an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $b$ and $c$. Then the composition of $\mathrm{hab}$ and $\mathrm{hbc}$ is an element of $\operatorname{PreEnvelGroupRel'}$ applied to $R$, $a$ and $c$.

Let $x_{1}$ be an element of $R$. Then $\operatorname{act'}$ applied to $x_{1}$ is an equivalence from $R$ to $R$ defined as $\operatorname{mk}$ applied to $\operatorname{act}$ applied to $x_{1}$, $\operatorname{invAct}$ applied to $x_{1}$, $\mathrm{Rack\_\_left\_inv}$ applied to $x_{1}$ and $\mathrm{Rack\_\_right\_inv}$ applied to $x_{1}$.

$\operatorname{envelAction}$ is a monoid homomorphism of $\operatorname{EnvelGroup}$ applied to $R$ and $\EquivMACRoAE {R}{R}$ defined as $\operatorname{map}$ applied to the conjugate of $R$.

Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{invAct}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

Let $R$ be a set. Then $\operatorname{selfApplyEquiv}$ applied to $R$ is an equivalence from $R$ to $R$.

the conjugate of R (from the name)

Let $R$ be a set. Then the conjugate of $R$ is an element of $\mathrm{ShelfHom}$ applied to $R$ and the set of conjugates of $\EquivMACRoAE {R}{R}$.

the canonical homomorphism of R (from the docstring)

Let $R$ be a set. Then the canonical homomorphism of $R$ is an element of $\mathrm{ShelfHom}$ applied to $R$ and the set of conjugates of $\operatorname{EnvelGroup}$ applied to $R$.

the map (from the name)

The map is an equivalence from $\mathrm{ShelfHom}$ applied to $R$ and the set of conjugates of $G$ to the set of monoid homomorphisms of $\operatorname{EnvelGroup}$ applied to $R$ and $G$.

Let $x$ be a set. Then we can say that $\mathrm{Shelf}$ holds for $x$.

Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{act}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{ShelfHom}$ applied to $x$ and $x_{1}$ are a basic type.

the composition of g and f (from the name)

Let $g$ be an element of $\mathrm{ShelfHom}$ applied to $x_{1}$ and $x_{2}$. Let $f$ be an element of $\mathrm{ShelfHom}$ applied to $x$ and $x_{1}$. Then the composition of $g$ and $f$ is an element of $\mathrm{ShelfHom}$ applied to $x$ and $x_{2}$.

the identity homomorphism of S (from the docstring)

Let $S$ be a set. Then the identity homomorphism of $S$ is an element of $\mathrm{ShelfHom}$ applied to $S$ and $S$.

Let $\mathrm{self}$ be an element of $\mathrm{ShelfHom}$ applied to $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

Let $x$ be a set. Then we can say that $\mathrm{UnitalShelf}$ holds for $x$.

quaternion of R (from the name)

Let $R$ be a set. Then a quaternion of $R$ is an element of the function that maps $R$ to the set of quaternion algebras of $0$ and $\operatorname{neg}$ applied to $1$.

the coercion of x1 (from the name)

Let $x_{1}$ be an element of $R$. Then the coercion of $x_{1}$ is a quaternion of $R$ defined as the coercion of $x_{1}$.

the equivalence product of R (from the name)

Let $R$ be a set. Then the equivalence product of $R$ is an equivalence from the set of quaternions of $R$ to $\mathrm{Prod}$ applied to $R$ and $\mathrm{Prod}$ applied to $R$ and $\mathrm{Prod}$ applied to $R$ and $R$ defined as the equivalence product of $0$ and $\operatorname{neg}$ applied to $1$.

the equivalence tuple of R (from the name)

Let $R$ be a set. Then the equivalence tuple of $R$ is an equivalence from the set of quaternions of $R$ to the set of functions from elements of $\mathrm{Fin}$ applied to $4$ to elements of $R$ defined as the equivalence tuple of $0$ and $\operatorname{neg}$ applied to $1$.

the imaginary part of x1 (from the docstring)

Let $x_{1}$ be a quaternion of $R$. Then the imaginary part of $x_{1}$ is a quaternion of $R$ defined as the imaginary part of $x_{1}$.

the norm square (from the name)

The norm square is a monoid with zero homomorphism of the set of quaternions of $R$ and $R$.

$\operatorname{starAe}$ is an algebra isomorphism of the set of quaternions of $R$ and the set of multiplicative opposites of the set of quaternions of $R$ defined as $\operatorname{starAe}$.

quaternion algebra of b and c (from the name)

Let $R$ be a set. Let $a$, $b$ and $c$ be elements of $R$. Then the quaternion algebras of $b$ and $c$ are a basic type.

the additive equivalence product of x2 and x3 (from the name)

Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $R$. Then the additive equivalence product of $x_{2}$ and $x_{3}$ is an additive equivalence of the set of quaternion algebras of $x_{2}$ and $x_{3}$ and $\mathrm{Prod}$ applied to $R$ and $\mathrm{Prod}$ applied to $R$ and $\mathrm{Prod}$ applied to $R$ and $R$ defined as the additive equivalence of the equivalence product of $x_{2}$ and $x_{3}$.

the additive equivalence tuple of x2 and x3 (from the name)

Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $R$. Then the additive equivalence tuple of $x_{2}$ and $x_{3}$ is an additive equivalence of the set of quaternion algebras of $x_{2}$ and $x_{3}$ and the set of functions from elements of $\mathrm{Fin}$ applied to $4$ to elements of $R$ defined as the additive equivalence of the equivalence tuple of $x_{2}$ and $x_{3}$.

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then $\operatorname{basisOneIJK}$ applied to $x$, $x_{1}$ and $x_{2}$ is a basis of $R$ and the set of quaternion algebras of $x_{1}$ and $x_{2}$ defined as the basis of the linear equivalence tuple of $x_{1}$ and $x_{2}$.

the coercion of x4 (from the name)

Let $x_{4}$ be an element of $R$. Then the coercion of $x_{4}$ is a quaternion algebra of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $x_{4}$, $0$, $0$ and $0$.

the equivalence product of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the equivalence product of $x_{1}$ and $x_{2}$ is an equivalence from the set of quaternion algebras of $x_{1}$ and $x_{2}$ to $\mathrm{Prod}$ applied to $R$ and $\mathrm{Prod}$ applied to $R$ and $\mathrm{Prod}$ applied to $R$ and $R$.

the equivalence tuple of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the equivalence tuple of $x_{1}$ and $x_{2}$ is an equivalence from the set of quaternion algebras of $x_{1}$ and $x_{2}$ to the set of functions from elements of $\mathrm{Fin}$ applied to $4$ to elements of $R$.

the imaginary part of x4 (from the docstring)

Let $x_{4}$ be a quaternion algebra of $x_{1}$ and $x_{2}$. Then the imaginary part of $x_{4}$ is a quaternion algebra of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $0$, the imaginary part of $x_{4}$, the imaginary part of $x_{4}$ and the imaginary part of $x_{4}$.

the imaginary part of self (from the name)

Let $\mathrm{self}$ be a quaternion algebra of $b$ and $c$. Then the imaginary part of $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the imaginary part of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the imaginary part of $x_{1}$ and $x_{2}$ is a linear map of the set of quaternion algebras of $x_{1}$ and $x_{2}$ and $R$.

the imaginary part of self (from the name)

Let $\mathrm{self}$ be a quaternion algebra of $b$ and $c$. Then the imaginary part of $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the imaginary part of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the imaginary part of $x_{1}$ and $x_{2}$ is a linear map of the set of quaternion algebras of $x_{1}$ and $x_{2}$ and $R$.

the imaginary part of self (from the name)

Let $\mathrm{self}$ be a quaternion algebra of $b$ and $c$. Then the imaginary part of $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the imaginary part of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the imaginary part of $x_{1}$ and $x_{2}$ is a linear map of the set of quaternion algebras of $x_{1}$ and $x_{2}$ and $R$.

the linear equivalence tuple of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the linear equivalence tuple of $x_{1}$ and $x_{2}$ is a linear equivalence of the set of quaternion algebras of $x_{1}$ and $x_{2}$ and the set of functions from elements of $\mathrm{Fin}$ applied to $4$ to elements of $R$ defined as the linear equivalence of $R$ and the additive equivalence tuple of $x_{1}$ and $x_{2}$.

the real part of self (from the name)

Let $\mathrm{self}$ be a quaternion algebra of $b$ and $c$. Then the real part of $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the real part of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be elements of $R$. Then the real part of $x_{1}$ and $x_{2}$ is a linear map of the set of quaternion algebras of $x_{1}$ and $x_{2}$ and $R$.

$\operatorname{starAe}$ is an algebra isomorphism of the set of quaternion algebras of $x_{1}$ and $x_{2}$ and the set of multiplicative opposites of the set of quaternion algebras of $x_{1}$ and $x_{2}$.

the swap equivalence of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of $R$. Then the swap equivalence of $x$ and $x_{1}$ is an algebra isomorphism of the set of quaternion algebras of $0$ and $x_{1}$ and the set of quaternion algebras of $0$ and $x$.

basis of x4 and x5 (from the name)

Let $A$ be a set. Let $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $R$. Then the bases of $x_{4}$ and $x_{5}$ are a basic type.

the composition homomorphism of q and F (from the name)

Let $q$ be a basis of $x_{6}$ and $x_{7}$. Let $F$ be an algebra homomorphism of $A$ and $B$. Then the composition homomorphism of $q$ and $F$ is a basis of $x_{6}$ and $x_{7}$.

Let $\mathrm{self}$ be a basis of $x_{4}$ and $x_{5}$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a basis of $x_{4}$ and $x_{5}$. Then $\operatorname{j}$ applied to $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a basis of $x_{4}$ and $x_{5}$. Then $\operatorname{k}$ applied to $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the lift of q and x6 (from the name)

Let $q$ be a basis of $x_{4}$ and $x_{5}$. Let $x_{6}$ be a quaternion algebra of $x_{4}$ and $x_{5}$. Then the lift of $q$ and $x_{6}$ is an element of $A$ defined as $\operatorname{algebraMap} (R , A , \operatorname{re} (x_{6}))+ \HSMulhSMulMACRoAL {\operatorname{imI} (x_{6})}{\operatorname{i} (q)}+ \HSMulhSMulMACRoAL {\operatorname{imJ} (x_{6})}{\operatorname{j} (q)}+ \HSMulhSMulMACRoAL {\operatorname{imK} (x_{6})}{\operatorname{k} (q)}$.

the lift homomorphism of q (from the name)

Let $q$ be a basis of $x_{4}$ and $x_{5}$. Then the lift homomorphism of $q$ is an algebra homomorphism of the set of quaternion algebras of $x_{4}$ and $x_{5}$ and $A$ defined as $\operatorname{mk'}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{lift}$ applied to $q$ and $\mathrm{QuaternionAlgebra\_\_Basis\_\_lift\_one}$ applied to $q$ and $\mathrm{QuaternionAlgebra\_\_Basis\_\_lift\_mul}$ applied to $q$, $\mathrm{QuaternionAlgebra\_\_Basis\_\_lift\_zero}$ applied to $q$ and $\mathrm{QuaternionAlgebra\_\_Basis\_\_lift\_add}$ applied to $q$ and $\mathrm{QuaternionAlgebra\_\_Basis\_\_lift\_smul}$ applied to $q$.

the self of R (from the name)

Let $R$ be a set. Then the self of $R$ is a basis of $x_{2}$ and $x_{3}$.

the lift (from the name)

The lift is an equivalence from the set of bases of $x_{4}$ and $x_{5}$ to the set of algebra homomorphisms of the set of quaternion algebras of $x_{4}$ and $x_{5}$ and $A$.

A has quotients (from the name)

Let $A$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $B$ be a set. Then we can say that $A$ has quotients.

quotient of A and x (from the name)

Let $A$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $x$ be an element of $B$. Then a quotient of $A$ and $x$ is an element of the function that maps $A$ and $x$ to $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

c is a additive left regular (from the name)

Let $c$ be an element of $R$. Then $c$ is an additive left regular, if the function that maps $x_{1}$ to $c + x_{1}$ is injective.

c is a additive regular (from the name)

Let $c$ be an element of $R$. Then we can say that $c$ is an additive regular.

c is a additive right regular (from the name)

Let $c$ be an element of $R$. Then $c$ is an additive right regular, if the function that maps $x_{1}$ to $x_{1} + c$ is injective.

c is a left regular (from the name)

Let $c$ be an element of $R$. Then $c$ is a left regular, if the function that maps $x_{1}$ to $c \times x_{1}$ is injective.

c is a regular (from the name)

Let $c$ be an element of $R$. Then we can say that $c$ is a regular.

c is a right regular (from the name)

Let $c$ be an element of $R$. Then $c$ is a right regular, if the function that maps $x_{1}$ to $x_{1} \times c$ is injective.

c is a multiplicative regular (from the name)

Let $M$ be a set. Let $c$ be an element of $R$. Then $c$ is a multiplicative regular, if the function that maps $x_{1}$ to $\HSMulhSMulMACRoAL {c}{x_{1}}$ is injective.

c is a additive regular (from the name)

Let $M$ be a set. Let $c$ be an element of $R$. Then $c$ is an additive regular, if the function that maps $x_{1}$ to the sum of $c$ and $x_{1}$ is injective.

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

the ring homomorphism of x3 (from the name)

Let $M$ and $R$ be sets. Let $x_{3}$ be an element of $M$. Then the ring homomorphism of $x_{3}$ is a ring homomorphism of $R$ and $R$.

the ring automorphism of G and R (from the name)

Let $G$ and $R$ be sets. Then the ring automorphism of $G$ and $R$ is a monoid homomorphism of $G$ and the set of ring automorphisms of $R$.

the ring isomorphism of G and R (from the name)

Let $G$ and $R$ be sets. Then the ring isomorphism of $G$ and $R$ is a monoid homomorphism of $G$ and the set of ring isomorphisms of $R$ and $R$.

S is a invariant subring (from the name)

Let $M$ be a set. Let $S$ be a subring of $R$. Then we can say that $S$ is an invariant subring.

the subtype homomorphism of M and U (from the name)

Let $M$ be a set. Let $U$ be a subring of $\mathrm{R'}$. Then the subtype homomorphism of $M$ and $U$ is a multiplicative semiring action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {U}{x_{3}})}$ and $\mathrm{R'}$.

the additive subgroup of M and x (from the name)

Let $M$ and $x$ be sets. Then the additive subgroup of $M$ and $x$ is an additive subgroup of $x$.

the additive submonoid of M and x (from the name)

Let $M$ and $x$ be sets. Then the additive submonoid of $M$ and $x$ is an additive submonoid of $x$.

the left multiplicative (from the name)

The left multiplicative is a monoid homomorphism of $\UnitsMACRoAO {R}$ and the set of multiplicatives of the set of additive automorphisms of $R$ defined as the additive automorphism of $\UnitsMACRoAO {R}$ and $R$.

the right multiplicative of u (from the name)

Let $u$ be a unit of $R$. Then the right multiplicative of $u$ is an additive automorphism of $R$ defined as $\operatorname{toAddAut}$ applied to the set of units of the set of multiplicative opposites of $R$, $R$ and $\operatorname{symm}$ applied to the opposite equivalence and the opposite of $u$.

the associator (from the docstring)

The associator is an additive monoid homomorphism of $R$ and the set of additive monoid homomorphisms of $R$ and the set of additive monoid homomorphisms of $R$ and $R$ defined as the difference between the multiplication and the multiplication.

the multiplication (from the docstring)

The multiplication is an additive monoid homomorphism of $R$ and the set of additive monoid homomorphisms of $R$ and the set of additive monoid homomorphisms of $R$ and $R$.

the multiplication (from the docstring)

The multiplication is an additive monoid homomorphism of $R$ and the set of additive monoid homomorphisms of $R$ and the set of additive monoid homomorphisms of $R$ and $R$.

the associator of y and z (from the name)

Let $x_{1}$, $y$ and $z$ be elements of $R$. Then the associator of $y$ and $z$ is an element of $R$ defined as $x_{1} \times y \times z - x_{1} \times (y \times z)$.

ring automorphism of R (from the name)

Let $R$ be a set. Then a ring automorphism of $R$ is an element of the function that maps $R$ to the set of ring isomorphisms of $R$ and $R$.

the additive automorphism of R (from the name)

Let $R$ be a set. Then the additive automorphism of $R$ is a monoid homomorphism of the set of ring automorphisms of $R$ and the set of multiplicatives of the set of additive automorphisms of $R$.

the multiplicative automorphism of R (from the name)

Let $R$ be a set. Then the multiplicative automorphism of $R$ is a monoid homomorphism of the set of ring automorphisms of $R$ and the set of multiplicative automorphisms of $R$.

the permutation of R (from the name)

Let $R$ be a set. Then the permutation of $R$ is a monoid homomorphism of the set of ring automorphisms of $R$ and the set of permutations of $R$.

the left multiplicative of r (from the name)

Let $r$ be an element of $R$. Then the left multiplicative of $r$ is an additive homomorphism of $R$ and $R$.

the right multiplicative of r (from the name)

Let $r$ be an element of $R$. Then the right multiplicative of $r$ is an additive homomorphism of $R$ and $R$.

the left multiplicative (from the name)

The left multiplicative is an additive monoid homomorphism of $R$ and the set of ends of $R$ defined as the product.

the right multiplicative (from the name)

The right multiplicative is an additive monoid homomorphism of $R$ and the set of ends of $R$ defined as the flip of the product.

the product (from the name)

The product is an additive monoid homomorphism of $R$ and the set of additive monoid homomorphisms of $R$ and $R$.

the left multiplicative of r (from the name)

Let $r$ be an element of $R$. Then the left multiplicative of $r$ is an additive monoid homomorphism of $R$ and $R$.

the right multiplicative of r (from the name)

Let $r$ be an element of $R$. Then the right multiplicative of $r$ is an additive monoid homomorphism of $R$ and $R$.

Let $x$ be a set. Then an element of $\mathrm{AsBoolAlg}$ applied to $x$ is an element of the function that maps $x$ to $x$.

Let $x$ be a set. Then an element of $\mathrm{AsBoolRing}$ applied to $x$ is an element of the function that maps $x$ to $x$.

x is a boolean ring (from the name)

Let $x$ be a set. Then we can say that $x$ is a boolean ring.

Let $f$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{asBoolRing}$ applied to $f$ is a ring homomorphism of $\mathrm{AsBoolRing}$ applied to $x$ and $\mathrm{AsBoolRing}$ applied to $x_{1}$.

Let $x$ be a set. Then $\operatorname{asBoolAlgAsBoolRing}$ applied to $x$ is an order isomorphism of $\mathrm{AsBoolAlg}$ applied to $\mathrm{AsBoolRing}$ applied to $x$ and $x$.

Let $x$ be a set. Then $\operatorname{asBoolRingAsBoolAlg}$ applied to $x$ is a ring isomorphism of $\mathrm{AsBoolRing}$ applied to $\mathrm{AsBoolAlg}$ applied to $x$ and $x$.

Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Then $\operatorname{asBoolAlg}$ applied to $f$ is a bounded lattice homomorphism of $\mathrm{AsBoolAlg}$ applied to $x$ and $\mathrm{AsBoolAlg}$ applied to $x_{1}$.

the bool algebra (from the name)

The bool algebra is an element of $\EquivMACRoAE {\mathrm{AsBoolAlg} (x)}{x}$ defined as the identity of $\mathrm{AsBoolAlg}$ applied to $x$.

the bool ring (from the name)

The bool ring is an element of $\EquivMACRoAE {\mathrm{AsBoolRing} (x)}{x}$ defined as the identity of $\mathrm{AsBoolRing}$ applied to $x$.

the bool algebra (from the name)

The bool algebra is an element of $\EquivMACRoAE {x}{\mathrm{AsBoolAlg} (x)}$ defined as the identity of $x$.

the bool ring (from the name)

The bool ring is an element of $\EquivMACRoAE {x}{\mathrm{AsBoolRing} (x)}$ defined as the identity of $x$.

centroid homomorphism of x (from the name)

Let $x$ be a set. Then the centroid homomorphisms of $x$ are a basic type.

the canonical isomorphism from the center (from the docstring)

The canonical isomorphism from the center is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{2}})}$ and the set of centroid homomorphisms of $x$.

the canonical homomorphism from the center into the centroid (from the docstring)

The canonical homomorphism from the center into the centroid is a non unital ring homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{2}})}$ and the set of centroid homomorphisms of $x$ defined as the composition of the non unital ring homomorphism of the subtype of the center of the set of centroid homomorphisms of $x$ and the canonical homomorphism from the center into the center of the centroid.

the canonical homomorphism from the center into the center of the centroid (from the docstring)

The canonical homomorphism from the center into the center of the centroid is a non unital ring homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{CentroidHom} (x))}{x_{3}})}$.

the composition of g and f (from the name)

Let $g$ and $f$ be centroid homomorphisms of $x$. Then the composition of $g$ and $f$ is a centroid homomorphism of $x$.

the copy of f and h (from the name)

Let $f$ be a centroid homomorphism of $x$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a centroid homomorphism of $x$.

the identity of x (from the name)

Let $x$ be a set. Then the identity of $x$ is a centroid homomorphism of $x$.

the end of f (from the name)

Let $f$ be a centroid homomorphism of $x$. Then the end of $f$ is an end of $x$ defined as the additive monoid homomorphism of $f$.

the end ring homomorphism of x (from the name)

Let $x$ be a set. Then the end ring homomorphism of $x$ is a ring homomorphism of the set of centroid homomorphisms of $x$ and the set of ends of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toEnd}$ and $\mathrm{CentroidHom\_\_toEnd\_one}$ and $\mathrm{CentroidHom\_\_toEnd\_mul}$, $\mathrm{CentroidHom\_\_toEnd\_zero}$ and $\mathrm{CentroidHom\_\_toEnd\_add}$.

x is a centroid homomorphism class (from the name)

Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $x$ is a centroid homomorphism class.

the centroid homomorphism (from the name)

The centroid homomorphism is a ring homomorphism of $R$ and the set of centroid homomorphisms of $x$ defined as the scalar multiple one homomorphism.

the cast embedding (from the name)

The cast embedding is an embedding of $\Natural$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toNatCast}$ and $\mathrm{Nat\_\_cast\_injective}$.

Let $x_{6}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{7}$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Let $x_{8}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $x$ and $x_{2}$. Then we can say that $\mathrm{RingHomCompTriple}$ holds for $x_{6}$, $x_{7}$ and $x_{8}$.

x1 is a ring homomorphism identity (from the name)

Let $x_{1}$ be a ring homomorphism of $R$ and $R$. Then we can say that $x_{1}$ is a ring homomorphism identity.

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{5}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $x_{1}$ and $x$. Then we can say that $\mathrm{RingHomInvPair}$ holds for $x_{4}$ and $x_{5}$.

the ring isomorphism of x4 and x5 (from the name)

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{5}$ be a ring homomorphism of $x_{1}$ and $x$. Then the ring isomorphism of $x_{4}$ and $x_{5}$ is a ring isomorphism of $x$ and $x_{1}$ defined as the ring isomorphism of $x_{4}$ and $x_{5}$.

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Then we can say that $\mathrm{RingHomSurjective}$ holds for $x_{4}$.

x is a commutative ring (from the name)

Let $x$ be a set. Then we can say that $x$ is a commutative ring.

R is a commutative semiring (from the name)

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

R is distributive (from the name)

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

x has distributive negations (from the name)

Let $x$ be a set. Then we can say that $x$ has distributive negations.

x is a domain (from the name)

Let $x$ be a set. Then we can say that $x$ is a domain.

R is a left distributive class (from the name)

Let $R$ be a set. Then we can say that $R$ is a left distributive class.

Let $x$ be a set. Then we can say that $\mathrm{NonAssocCommRing}$ holds for $x$.

Let $x$ be a set. Then we can say that $\mathrm{NonAssocCommSemiring}$ holds for $x$.

Let $x$ be a set. Then we can say that $\mathrm{NonAssocRing}$ holds for $x$.

Let $x$ be a set. Then we can say that $\mathrm{NonAssocSemiring}$ holds for $x$.

x is a non unital commutative ring (from the name)

Let $x$ be a set. Then we can say that $x$ is a non unital commutative ring.

x is a non unital commutative semiring (from the name)

Let $x$ be a set. Then we can say that $x$ is a non unital commutative semiring.

Let $x$ be a set. Then we can say that $\mathrm{NonUnitalNonAssocCommRing}$ holds for $x$.

Let $x$ be a set. Then we can say that $\mathrm{NonUnitalNonAssocCommSemiring}$ holds for $x$.

Let $x$ be a set. Then we can say that $\mathrm{NonUnitalNonAssocRing}$ holds for $x$.

Let $x$ be a set. Then we can say that $\mathrm{NonUnitalNonAssocSemiring}$ holds for $x$.

x is a non unital ring (from the name)

Let $x$ be a set. Then we can say that $x$ is a non unital ring.

x is a non unital semiring (from the name)

Let $x$ be a set. Then we can say that $x$ is a non unital semiring.

R is a right distributive class (from the name)

Let $R$ be a set. Then we can say that $R$ is a right distributive class.

R is a ring (from the name)

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

x is a semiring (from the name)

Let $x$ be a set. Then we can say that $x$ is a semiring.

the divisibility of g (from the name)

Let $g$ be an element of $G$. Then the divisibility of $g$ is an equivalence from $G$ to $\SubtypeSet {a}{(\divides {g}{a})}$.

the ring isomorphism of f and H (from the name)

Let $f$ be an element of $F$ such that for all elements $x_{5}$ and $y$ of $R$, $\EqtMACRoH {f (x_{5} \times y)}{f (x_{5})\times f (y)}$. Then the ring isomorphism of $f$ and $H$ is a ring isomorphism of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the additive equivalence of $f$, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to $\operatorname{mk'}$ applied to $\operatorname{toEquiv}$ applied to the additive equivalence of $f$ and $H$ and $\mathrm{AddEquiv\_\_map\_add'}$ applied to the additive equivalence of $f$.

the ring isomorphism of f and H (from the name)

Let $f$ be an element of $F$ such that for all elements $x_{5}$ and $y$ of $R$, $\EqtMACRoH {f (x_{5} + y)}{f (x_{5})+ f (y)}$. Then the ring isomorphism of $f$ and $H$ is a ring isomorphism of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the multiplicative equivalence of $f$, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to the multiplicative equivalence of $f$ and $\mathrm{AddEquiv\_\_map\_add'}$ applied to $\operatorname{mk'}$ applied to $\operatorname{toEquiv}$ applied to the multiplicative equivalence of $f$ and $H$.

the inverse of f and g (from the name)

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

ring isomorphism of R and S (from the name)

Let $R$ and $S$ be sets. Then the ring isomorphisms of $R$ and $S$ are a basic type.

the cast of h (from the name)

Assume that $\EqtMACRoH {i}{j}$. Then the cast of $h$ is a ring isomorphism of $R$ applied to $i$ and $R$ applied to $j$.

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

Let $f$ be an element of $F$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the ring isomorphism of $f$ and $\mathrm{hf}$ is a ring isomorphism of $R$ and $S$.

the ring isomorphism of hom and inv (from the name)

Let $\mathrm{hom}$ be a non unital ring homomorphism of $R$ and $S$. Let $\mathrm{inv}$ be a non unital ring homomorphism of $S$ and $R$ such that the composition of $\mathrm{inv}$ and $\mathrm{hom}$ is equal to the identity of $R$ and the composition of $\mathrm{hom}$ and $\mathrm{inv}$ is equal to the identity of $S$. Then the ring isomorphism of $\mathrm{hom}$ and $\mathrm{inv}$ is a ring isomorphism of $R$ and $S$.

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

Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a ring homomorphism of $S$ and $R$ such that the composition of $f$ and $g$ is equal to the identity ring homomorphism of $S$ and the composition of $g$ and $f$ is equal to the identity ring homomorphism of $R$. Then the ring isomorphism of $f$ and $g$ is a ring isomorphism of $R$ and $S$.

the ring isomorphism (from the name)

The ring isomorphism is a ring isomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the additive equivalence, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to the multiplicative equivalence and $\mathrm{AddEquiv\_\_map\_add'}$ applied to the additive equivalence.

the opposite (from the name)

The opposite is an equivalence from the set of ring isomorphisms of $x$ and $x_{1}$ to the set of ring isomorphisms of the set of multiplicative opposites of $x$ and the set of multiplicative opposites of $x_{1}$.

the opposite opposite of R (from the name)

Let $R$ be a set. Then the opposite opposite of $R$ is a ring isomorphism of $R$ and the set of multiplicative opposites of the set of multiplicative opposites of $R$.

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

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

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

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

the right product congruence of e (from the name)

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

the product equivalence product subtype product of p and Y (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $Y$ be a function from elements of $x$ to sets. Then the product equivalence product subtype product of $p$ and $Y$ is a ring isomorphism of the set of functions from elements $i$ of $x$ to elements of $Y$ applied to $i$ and $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{3}}{p (x_{3})}$ to elements of $Y$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{4}}{\mathrm{not} (p (x_{4}))}$ to elements of $Y$ applied to $i_{2}$.

the opposite of S (from the docstring)

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

the product option equivalence product (from the name)

The product option equivalence product is a ring isomorphism of the set of functions from elements $i$ of $\mathrm{Option}$ applied to $x$ to elements of $R$ applied to $i$ and $\mathrm{Prod}$ applied to $R$ applied to $\operatorname{none}$ and the set of functions from elements $i_{1}$ of $x$ to elements of $R$ applied to $\operatorname{some}$ applied to $i_{1}$.

Let $R$ be a function from elements of $x$ to sets. Then $\operatorname{piUnique}$ applied to $R$ is a ring isomorphism of the set of functions from elements $i$ of $x$ to elements of $R$ applied to $i$ and $R$ applied to $\operatorname{default}$.

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

Let $f$ be a ring isomorphism of $R$ and $\mathrm{R'}$. Let $g$ be a ring isomorphism of $S$ and $\mathrm{S'}$. Then the product congruence of $f$ and $g$ is a ring isomorphism of $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Prod}$ applied to $\mathrm{R'}$ and $\mathrm{S'}$.

the identity map of R (from the docstring)

Let $R$ be a set. Then the identity map of $R$ is a ring isomorphism of $R$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the identity map of $R$, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to the identity map of $R$ and $\mathrm{AddEquiv\_\_map\_add'}$ applied to the identity map of $R$.

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

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

the inverse of e (from the docstring)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the inverse of $e$ is a ring isomorphism of $S$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the inverse of the multiplicative equivalence of $e$, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to the inverse of the multiplicative equivalence of $e$ and $\mathrm{AddEquiv\_\_map\_add'}$ applied to the inverse of the additive equivalence of $e$.

the additive equivalence of self (from the name)

Let $\mathrm{self}$ be a ring isomorphism of $R$ and $S$. Then the additive equivalence of $\mathrm{self}$ is an additive equivalence of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{RingEquiv\_\_map\_add'}$ applied to $\mathrm{self}$.

the additive monoid homomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the additive monoid homomorphism of $e$ is an additive monoid homomorphism of $R$ and $S$ defined as the additive monoid homomorphism of the ring homomorphism of $e$.

the monoid homomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the monoid homomorphism of $e$ is a monoid homomorphism of $R$ and $S$ defined as $\operatorname{toMonoidHom}$ applied to the ring homomorphism of $e$.

the multiplicative equivalence of self (from the name)

Let $\mathrm{self}$ be a ring isomorphism of $R$ and $S$. Then the multiplicative equivalence of $\mathrm{self}$ is a multiplicative equivalence of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{RingEquiv\_\_map\_mul'}$ applied to $\mathrm{self}$.

the non unital ring homomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the non unital ring homomorphism of $e$ is a non unital ring homomorphism of $R$ and $S$.

the opposite of R (from the name)

Let $R$ be a set. Then the opposite of $R$ is a ring isomorphism of $R$ and the set of multiplicative opposites of $R$.

the ring homomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the ring homomorphism of $e$ is a ring homomorphism of $R$ and $S$.

the composition of x6 and x7 (from the name)

Let $x_{6}$ be a ring isomorphism of $R$ and $S$. Let $x_{7}$ be a ring isomorphism of $S$ and $\mathrm{S'}$. Then the composition of $x_{6}$ and $x_{7}$ is a ring isomorphism of $R$ and $\mathrm{S'}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the composition of the multiplicative equivalence of $x_{6}$ and the multiplicative equivalence of $x_{7}$, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to the composition of the multiplicative equivalence of $x_{6}$ and the multiplicative equivalence of $x_{7}$ and $\mathrm{AddEquiv\_\_map\_add'}$ applied to the composition of the additive equivalence of $x_{6}$ and the additive equivalence of $x_{7}$.

the opposite (from the name)

The opposite is an equivalence from the set of ring isomorphisms of the set of multiplicative opposites of $x$ and the set of multiplicative opposites of $x_{1}$ to the set of ring isomorphisms of $x$ and $x_{1}$ defined as the inverse of the opposite.

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

the ring isomorphism of f (from the name)

Let $f$ be an element of $F$. Then the ring isomorphism of $f$ is a ring isomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to the multiplicative equivalence of $f$, $\mathrm{MulEquiv\_\_map\_mul'}$ applied to the multiplicative equivalence of $f$ and $\mathrm{AddEquiv\_\_map\_add'}$ applied to the additive equivalence of $f$.

the inverse of f and g (from the name)

Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a function from elements of $S$ to elements of $R$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$ and $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is a ring homomorphism of $S$ and $R$.

Let $R$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwo}$ applied to $R$ is a ring isomorphism of the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $2$ to elements of $R$ applied to $i$ and $\mathrm{Prod}$ applied to $R$ applied to $0$ and $R$ applied to $1$.

the ring homomorphism of f (from the name)

Let $f$ be an additive monoid homomorphism of $x_{1}$ and $x$ such that for all elements $x_{4}$ of $x_{1}$, $\EqtMACRoH {f (x_{4} \times x_{4})}{f (x_{4})\times f (x_{4})}$. Assume that $2 \neq 0$. Assume that $\EqtMACRoH {f (1)}{1}$. Then the ring homomorphism of $f$ is a ring homomorphism of $x_{1}$ and $x$.

non unital ring homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the non unital ring homomorphisms of $x$ and $x_{1}$ are a basic type.

the composition of g and f (from the name)

Let $g$ be a non unital ring homomorphism of $x_{1}$ and $x_{2}$. Let $f$ be a non unital ring homomorphism of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a non unital ring homomorphism of $x$ and $x_{2}$.

the copy of f and h (from the name)

Let $f$ be a non unital ring homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a non unital ring homomorphism of $x$ and $x_{1}$.

the identity of x (from the name)

Let $x$ be a set. Then the identity of $x$ is a non unital ring homomorphism of $x$ and $x$.

the additive monoid homomorphism of self (from the name)

Let $\mathrm{self}$ be a non unital ring homomorphism of $x$ and $x_{1}$. Then the additive monoid homomorphism of $\mathrm{self}$ is an additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toMulHom}$ applied to $\mathrm{self}$ and $\mathrm{NonUnitalRingHom\_\_map\_zero'}$ applied to $\mathrm{self}$ and $\mathrm{NonUnitalRingHom\_\_map\_add'}$ applied to $\mathrm{self}$.

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{NonUnitalRingHomClass}$ holds for $F$, $x$ and $x_{1}$.

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

Let $f$ be an element of $F$. Then the non unital ring homomorphism of $f$ is a non unital ring homomorphism of $x$ and $x_{1}$.

ring homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the ring homomorphisms of $x$ and $x_{1}$ are a basic type.

the composition of g and f (from the name)

Let $g$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a ring homomorphism of $x$ and $x_{2}$.

the copy of f and h (from the name)

Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a ring homomorphism of $x$ and $x_{1}$.

the identity ring homomorphism of x (from the docstring)

Let $x$ be a set. Then the identity ring homomorphism of $x$ is a ring homomorphism of $x$ and $x$.

Let $f$ be a monoid homomorphism of $x$ and $x_{1}$ such that for all elements $a$ and $b$ of $x$, $\EqtMACRoH {f (a + b)}{f (a)+ f (b)}$. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_add}$ is a ring homomorphism of $x$ and $x_{1}$.

the additive monoid homomorphism of self (from the name)

Let $\mathrm{self}$ be a ring homomorphism of $x$ and $x_{1}$. Then the additive monoid homomorphism of $\mathrm{self}$ is an additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{RingHom\_\_map\_zero'}$ applied to $\mathrm{self}$ and $\mathrm{RingHom\_\_map\_add'}$ applied to $\mathrm{self}$.

the monoid with zero homomorphism of self (from the name)

Let $\mathrm{self}$ be a ring homomorphism of $x$ and $x_{1}$. Then the monoid with zero homomorphism of $\mathrm{self}$ is a monoid with zero homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{RingHom\_\_map\_zero'}$ applied to $\mathrm{self}$, $\mathrm{OneHom\_\_map\_one'}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{MonoidHom\_\_map\_mul'}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$.

the non unital ring homomorphism of self (from the name)

Let $\mathrm{self}$ be a ring homomorphism of $x$ and $x_{1}$. Then the non unital ring homomorphism of $\mathrm{self}$ is a non unital ring homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{MonoidHom\_\_map\_mul'}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$, $\mathrm{RingHom\_\_map\_zero'}$ applied to $\mathrm{self}$ and $\mathrm{RingHom\_\_map\_add'}$ applied to $\mathrm{self}$.

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{RingHomClass}$ holds for $F$, $x$ and $x_{1}$.

the ring homomorphism of f (from the name)

Let $f$ be an element of $F$. Then the ring homomorphism of $f$ is a ring homomorphism of $x$ and $x_{1}$.

the left multiplicative of x1 and y (from the name)

Let $x_{1}$ be an additive unit of $R$. Let $y$ be an element of $R$. Then the left multiplicative of $x_{1}$ and $y$ is an additive unit of $R$.

the right multiplicative of x1 and y (from the name)

Let $x_{1}$ be an additive unit of $R$. Let $y$ be an element of $R$. Then the right multiplicative of $x_{1}$ and $y$ is an additive unit of $R$.

the sum nonzero square of R (from the name)

Let $R$ be a set. Then the sum nonzero square of $R$ is an additive subsemigroup of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a sum nonzero square and the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{add}$.

R is formally real (from the docstring)

x3 is a sum nonzero square (from the name)

Let $x_{3}$ be an element of $R$. Then we can say that $x_{3}$ is a sum nonzero square.

Assume that $x_{3}$ is a sum nonzero square. Then we can say that $\operatorname{below}$ holds for $t$.

the negation one power of n (from the name)

Let $n$ be an integer. Then the negation one power of $n$ is a unit of $\Integer$ defined as $\operatorname{neg} (1)^ {n}$.

Let $f$ be a non unital ring homomorphism of $R$ and $S$ such that for all elements $x_{2}$ and $y$ of $R$, $\mathrm{Commute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then $\operatorname{fromOpposite}$ applied to $f$ and $\mathrm{hf}$ is a non unital ring homomorphism of the set of multiplicative opposites of $R$ and $S$.

the opposite (from the name)

The opposite is an equivalence from the set of non unital ring homomorphisms of $R$ and $S$ to the set of non unital ring homomorphisms of the set of multiplicative opposites of $R$ and the set of multiplicative opposites of $S$.

the opposite of f and hf (from the name)

Let $f$ be a non unital ring homomorphism of $R$ and $S$ such that for all elements $x_{2}$ and $y$ of $R$, $\mathrm{Commute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then the opposite of $f$ and $\mathrm{hf}$ is a non unital ring homomorphism of $R$ and the set of multiplicative opposites of $S$.

the opposite (from the name)

The opposite is an equivalence from the set of non unital ring homomorphisms of the set of multiplicative opposites of $R$ and the set of multiplicative opposites of $S$ to the set of non unital ring homomorphisms of $R$ and $S$ defined as the inverse of the opposite.

Let $f$ be a ring homomorphism of $R$ and $S$ such that for all elements $x_{2}$ and $y$ of $R$, $\mathrm{Commute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then $\operatorname{fromOpposite}$ applied to $f$ and $\mathrm{hf}$ is a ring homomorphism of the set of multiplicative opposites of $R$ and $S$.

the opposite (from the name)

The opposite is an equivalence from the set of ring homomorphisms of $R$ and $S$ to the set of ring homomorphisms of the set of multiplicative opposites of $R$ and the set of multiplicative opposites of $S$.

the opposite of f and hf (from the name)

Let $f$ be a ring homomorphism of $R$ and $S$ such that for all elements $x_{2}$ and $y$ of $R$, $\mathrm{Commute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then the opposite of $f$ and $\mathrm{hf}$ is a ring homomorphism of $R$ and the set of multiplicative opposites of $S$.

the opposite (from the name)

The opposite is an equivalence from the set of ring homomorphisms of the set of multiplicative opposites of $R$ and the set of multiplicative opposites of $S$ to the set of ring homomorphisms of $R$ and $S$ defined as the inverse of the opposite.

Let $a$ be an element of $x$. Then $\mathrm{Odd}$ holds for $a$, if there exists an element $k$ of $x$, such that $\EqtMACRoH {a}{2 \times k + 1}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $c$ be an element of $x$. Then $\operatorname{Antiperiodic}$ holds for $f$ and $c$, if for all elements $x_{4}$ of $x$, $\EqtMACRoH {f (x_{4} + c)}{\operatorname{neg} (f (x_{4}))}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $c$ be an element of $x$. Then $\operatorname{Periodic}$ holds for $f$ and $c$, if for all elements $x_{3}$ of $x$, $\EqtMACRoH {f (x_{3} + c)}{f (x_{3})}$.

the lift of h and x3 (from the name)

Assume that $\operatorname{Periodic}$ holds for $f$ and $c$. Let $x_{3}$ be a quotient of $x$ and $\operatorname{zmultiples}$ applied to $c$. Then the lift of $h$ and $x_{3}$ is an element of $x_{1}$.

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

Let $f$ be a non unital ring homomorphism of $x$ and $x_{1}$. Let $I$ be a set. Then the left composition of $f$ and $I$ is a non unital ring homomorphism of the set of functions from elements of $I$ to elements of $x$ and the set of functions from elements of $I$ to elements of $x_{1}$.

the product of g (from the name)

Let $g$ be a function from elements $i_{1}$ of $I$ to non unital ring homomorphisms of $x$ and $f$ applied to $i_{1}$. Then the product of $i_{1}$ is a non unital ring homomorphism of $x$ and the set of functions from elements $i$ of $I$ to elements of $f$ applied to $i$.

the constant non unital ring homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the constant non unital ring homomorphism of $x$ and $x_{1}$ is a non unital ring homomorphism of $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

the constant ring homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the constant ring homomorphism of $x$ and $x_{1}$ is a ring homomorphism of $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

the evaluation non unital ring homomorphism of f and i (from the name)

Let $f$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then the evaluation non unital ring homomorphism of $f$ and $i$ is a non unital ring homomorphism of the set of functions from elements $i_{1}$ of $I$ to elements of $f$ applied to $i_{1}$ and $f$ applied to $i$.

the evaluation ring homomorphism of f and i (from the name)

Let $f$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then the evaluation ring homomorphism of $f$ and $i$ is a ring homomorphism of the set of functions from elements $i_{1}$ of $I$ to elements of $f$ applied to $i_{1}$ and $f$ applied to $i$.

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

Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Let $I$ be a set. Then the left composition of $f$ and $I$ is a ring homomorphism of the set of functions from elements of $I$ to elements of $x$ and the set of functions from elements of $I$ to elements of $x_{1}$.

the product of g (from the name)

Let $g$ be a function from elements $i_{1}$ of $I$ to ring homomorphisms of $x$ and $f$ applied to $i_{1}$. Then the product of $i_{1}$ is a ring homomorphism of $x$ and the set of functions from elements $i$ of $I$ to elements of $f$ applied to $i$.

the first component of R and S (from the name)

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

the product of f and g (from the name)

Let $f$ be a non unital ring homomorphism of $R$ and $S$. Let $g$ be a non unital ring homomorphism of $R$ and $T$. Then the product of $f$ and $g$ is a non unital ring homomorphism of $R$ and $\mathrm{Prod}$ applied to $S$ and $T$.

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

Let $f$ be a non unital ring homomorphism of $R$ and $\mathrm{R'}$. Let $g$ be a non unital ring homomorphism of $S$ and $\mathrm{S'}$. Then the product map of $f$ and $g$ is a non unital ring homomorphism of $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Prod}$ applied to $\mathrm{R'}$ and $\mathrm{S'}$ defined as the product of the composition of $f$ and the first component of $R$ and $S$ and the composition of $g$ and the second component of $R$ and $S$.

the second component of R and S (from the name)

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

$\operatorname{prodComm}$ is a ring isomorphism of $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Prod}$ applied to $S$ and $R$.

Let $R$, $\mathrm{R'}$, $S$ and $\mathrm{S'}$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $R$, $\mathrm{R'}$, $S$ and $\mathrm{S'}$ is a ring isomorphism of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $R$ and $\mathrm{R'}$ and $\mathrm{Prod}$ applied to $S$ and $\mathrm{S'}$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Prod}$ applied to $\mathrm{R'}$ and $\mathrm{S'}$.

the product zero ring of R and S (from the name)

Let $R$ and $S$ be sets. Then the product zero ring of $R$ and $S$ is a ring isomorphism of $R$ and $\mathrm{Prod}$ applied to $R$ and $S$.

the zero ring product of R and S (from the name)

Let $R$ and $S$ be sets. Then the zero ring product of $R$ and $S$ is a ring isomorphism of $R$ and $\mathrm{Prod}$ applied to $S$ and $R$.

the first component of R and S (from the name)

Let $R$ and $S$ be sets. Then the first component of $R$ and $S$ is a ring homomorphism of $\mathrm{Prod}$ applied to $R$ and $S$ and $R$.

the product of f and g (from the name)

Let $f$ be a ring homomorphism of $R$ and $S$. Let $g$ be a ring homomorphism of $R$ and $T$. Then the product of $f$ and $g$ is a ring homomorphism of $R$ and $\mathrm{Prod}$ applied to $S$ and $T$.

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

Let $f$ be a ring homomorphism of $R$ and $\mathrm{R'}$. Let $g$ be a ring homomorphism of $S$ and $\mathrm{S'}$. Then the product map of $f$ and $g$ is a ring homomorphism of $\mathrm{Prod}$ applied to $R$ and $S$ and $\mathrm{Prod}$ applied to $\mathrm{R'}$ and $\mathrm{S'}$ defined as the product of the composition of $f$ and the first component of $R$ and $S$ and the composition of $g$ and the second component of $R$ and $S$.

the second component of R and S (from the name)

Let $R$ and $S$ be sets. Then the second component of $R$ and $S$ is a ring homomorphism of $\mathrm{Prod}$ applied to $R$ and $S$ and $S$.

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

the ring isomorphism of x (from the name)

Let $x$ be a set. Then the ring isomorphism of $x$ is a ring isomorphism of the set of shrinks of $x$ and $x$ defined as the ring isomorphism of the inverse of the equivalence shrink of $x$.

the ring isomorphism of h (from the name)

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

Let $e$ be a ring isomorphism of $R$ and $S$. Let $\mathrm{s'}$ be an element of $x_{2}$. Let $s$ be an element of $x_{3}$ such that for all elements $x_{8}$ of $R$, $x_{8}$ is an element of $\mathrm{s'}$, if and only if $\MembershipmemMACRoT {s}{e (x_{8})}$. Then $\operatorname{restrict}$ applied to $e$, $\mathrm{s'}$, $s$ and $h_{2}$ is a ring isomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{s'}}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {s}{x_{7}})}$.

the subring congruence of h (from the name)

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

the subring map of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the subring map of $e$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toRingHom} (e), s)}{x_{3}})}$ defined as the subsemiring map of $e$ and $\operatorname{toSubsemiring}$ applied to $s$.

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

the range of f (from the docstring)

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

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

the center of R (from the docstring)

Let $R$ be a set. Then the center of $R$ is a subring of $R$.

the center congruence of e (from the name)

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

the center (from the docstring)

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

the centralizer of s (from the docstring)

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

the closure of s (from the name)

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

the preimage of f and s (from the docstring)

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

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

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

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

the inclusion of h (from the name)

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

the map of f and s (from the name)

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

the product of s and t (from the name)

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

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

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

the top equivalence (from the name)

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

the subring of S and h1 (from the name)

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

subring of R (from the name)

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

the copy of S and s (from the name)

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

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

the subring of s (from the name)

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

the subtype of s (from the name)

Let $s$ be a subring of $R$. Then the subtype of $s$ is a ring homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $R$.

the additive subgroup of self (from the name)

Let $\mathrm{self}$ be a subring of $R$. Then the additive subgroup of $\mathrm{self}$ is an additive subgroup of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the carrier of $\operatorname{toSubsemigroup}$ applied to $\operatorname{toSubmonoid}$ applied to $\operatorname{toSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{Subsemiring\_\_add\_mem'}$ applied to $\operatorname{toSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{Subsemiring\_\_zero\_mem'}$ applied to $\operatorname{toSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{Subring\_\_neg\_mem'}$ applied to $\mathrm{self}$.

the non unital subring of S (from the name)

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

R is a subring class (from the name)

Let $S$ be a set. Let $R$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $R$ is a subring class.

the subtype of s (from the name)

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

the subring of s and hneg (from the name)

Let $s$ be a subsemiring of $R$ such that $\MembershipmemMACRoT {s}{\operatorname{neg} (1)}$. Then the subring of $s$ and $\mathrm{hneg}$ is a subring of $R$.

the integer of R and P (from the name)

Let $R$ be a subring of $K$. Let $P$ be a polynomial of $K$ such that for all natural numbers $n$, $\MembershipmemMACRoT {R}{\operatorname{coeff} (P , n)}$. Then the integer of $R$ and $P$ is a polynomial of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {R}{x_{1}})}$.

the additive equivalence opposite of S (from the name)

Let $S$ be a subring of $R$. Then the additive equivalence opposite of $S$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{2}})}$ defined as the additive equivalence opposite of $\operatorname{toSubsemiring}$ applied to $S$.

Let $S$ be a subring of $R$. Then $\operatorname{mopRingEquivOp}$ applied to $S$ is a ring isomorphism of the set of multiplicative opposites of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{2}})}$ defined as $\operatorname{mopRingEquivOp}$ applied to $\operatorname{toSubsemiring}$ applied to $S$.

the opposite of S (from the name)

Let $S$ be a subring of $R$. Then the opposite of $S$ is a subring of the set of multiplicative opposites of $R$.

the opposite equivalence (from the name)

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

Let $S$ be a subring of $R$. Then $\operatorname{ringEquivOpMop}$ applied to $S$ is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and the set of multiplicative opposites of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{2}})}$ defined as $\operatorname{ringEquivOpMop}$ applied to $\operatorname{toSubsemiring}$ applied to $S$.

the opposite of S (from the name)

Let $S$ be a subring of the set of multiplicative opposites of $R$. Then the opposite of $S$ is a subring of $R$.

the ordered subtype of s (from the name)

Let $s$ be a subring of $R$. Then the ordered subtype of $s$ is an order ring homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $R$ defined as $\operatorname{mk}$ applied to the subtype of $s$ and the function that maps $x_{2}$, $x_{3}$ and $h$ to $h$.

the positive part subgroup of R (from the name)

Let $R$ be a set. Then the positive part subgroup of $R$ is a subgroup of $\UnitsMACRoAO {R}$.

the ring isomorphism of h (from the name)

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

the subsemiring congruence of h (from the name)

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

the subsemiring map of e and s (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Let $s$ be a subsemiring of $R$. Then the subsemiring map of $e$ and $s$ is a ring isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toRingHom} (e), s)}{x_{3}})}$.

Let $f$ be a ring homomorphism of $R$ and $S$. Let $s$ be an element of $x_{2}$ such that for all elements $x_{5}$ of $R$, $\MembershipmemMACRoT {s}{f (x_{5})}$. Then $\operatorname{codRestrict}$ applied to $f$, $s$ and $h_{1}$ is a ring homomorphism of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$.

the range of f (from the docstring)

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

Let $f$ be a ring homomorphism of $R$ and $S$. Then $\operatorname{rangeSRestrict}$ applied to $f$ is a ring homomorphism of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{rangeS} (f)}{x_{2}})}$ defined as $\operatorname{codRestrict}$ applied to $f$, the range of $f$ and $\mathrm{RingHom\_\_mem\_rangeS\_self}$ applied to $f$.

Let $f$ be a ring homomorphism of $R$ and $S$. Let $\mathrm{s'}$ be an element of $x_{2}$. Let $s$ be an element of $x_{3}$ such that for all elements $x_{8}$ of $R$, if $x_{8}$ is an element of $\mathrm{s'}$, then $\MembershipmemMACRoT {s}{f (x_{8})}$. Then $\operatorname{restrict}$ applied to $f$, $\mathrm{s'}$, $s$ and $h_{2}$ is a ring homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{s'}}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {s}{x_{7}})}$.

the additive closure of M (from the docstring)

Let $M$ be a submonoid of $R$. Then the additive closure of $M$ is a subsemiring of $R$.

the center of R (from the docstring)

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

the center congruence of e (from the name)

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

the center (from the docstring)

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

the centralizer of s (from the docstring)

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

the closure of s (from the name)

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

the preimage of f and s (from the docstring)

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

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

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

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

the inclusion of h (from the name)

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

the map of f and s (from the name)

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

the product of s and t (from the name)

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

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

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

the top equivalence (from the name)

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

R is a additive submonoid with one class (from the name)

Let $S$ be a set. Let $R$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $R$ is an additive submonoid with one class.

the subsemiring of S and h1 (from the name)

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

Let $f$ be a ring homomorphism of $R$ and $S$. Let $s$ be an element of $x_{2}$. Then $\operatorname{domRestrict}$ applied to $f$ and $s$ is a ring homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ and $S$ defined as the composition of $f$ and the subtype of $s$.

Let $f$ and $g$ be ring homomorphisms of $R$ and $S$. Then $\operatorname{eqLocusS}$ applied to $f$ and $g$ is a subsemiring of $R$.

subsemiring of R (from the name)

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

the copy of S and s (from the name)

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

Let $s$ be an element of $\wp R$. Let $\mathrm{sm}$ be a submonoid of $R$ such that $\EqtMACRoH {\mathrm{sm}}{s}$. Let $\mathrm{sa}$ be an additive submonoid of $R$ such that $\EqtMACRoH {\mathrm{sa}}{s}$. Then $\operatorname{mk'}$ applied to $s$, $\mathrm{sm}$, $\mathrm{hm}$, $\mathrm{sa}$ and $\mathrm{ha}$ is a subsemiring of $R$.

the subsemiring of s (from the name)

Let $s$ be an element of $S$. Then the subsemiring of $s$ is a subsemiring of $R$.

the subtype of s (from the name)

Let $s$ be a subsemiring of $R$. Then the subtype of $s$ is a ring homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $R$.

the additive submonoid of self (from the name)

Let $\mathrm{self}$ be a subsemiring of $R$. Then the additive submonoid of $\mathrm{self}$ is an additive submonoid of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the carrier of $\operatorname{toSubsemigroup}$ applied to $\operatorname{toSubmonoid}$ applied to $\mathrm{self}$ and $\mathrm{Subsemiring\_\_add\_mem'}$ applied to $\mathrm{self}$ and $\mathrm{Subsemiring\_\_zero\_mem'}$ applied to $\mathrm{self}$.

the non unital subsemiring of S (from the name)

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

R is a subsemiring class (from the name)

Let $S$ be a set. Let $R$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $R$ is a subsemiring class.

the subtype of s (from the name)

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

the additive equivalence opposite of S (from the name)

Let $S$ be a subsemiring of $R$. Then the additive equivalence opposite of $S$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{2}})}$.

Let $S$ be a subsemiring of $R$. Then $\operatorname{mopRingEquivOp}$ applied to $S$ is a ring isomorphism of the set of multiplicative opposites of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{2}})}$.

the opposite of S (from the name)

Let $S$ be a subsemiring of $R$. Then the opposite of $S$ is a subsemiring of the set of multiplicative opposites of $R$.

the opposite equivalence (from the name)

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

Let $S$ be a subsemiring of $R$. Then $\operatorname{ringEquivOpMop}$ applied to $S$ is a ring isomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and the set of multiplicative opposites of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (S)}{x_{2}})}$.

the opposite of S (from the name)

Let $S$ be a subsemiring of the set of multiplicative opposites of $R$. Then the opposite of $S$ is a subsemiring of $R$.

Let $R$ be a set. Then $\operatorname{nonneg}$ applied to $R$ is a subsemiring of $R$.

the sum square of T (from the name)

Let $T$ be a set. Then the sum square of $T$ is an additive submonoid of $T$.

x3 is a sum square (from the name)

Let $x_{3}$ be an element of $R$. Then we can say that $x_{3}$ is a sum square.

Assume that $x_{3}$ is a sum square. Then we can say that $\operatorname{below}$ holds for $t$.

the sum square of T (from the name)

Let $T$ be a set. Then the sum square of $T$ is a non unital subsemiring of $T$ defined as the additive closure of the square of $T$.

the sum square of T (from the name)

Let $T$ be a set. Then the sum square of $T$ is a subsemiring of $T$.

the ring isomorphism of e (from the name)

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

the lift of f (from the name)

Let $f$ be a ring homomorphism of $R$ and $S$. Then the lift of $f$ is a ring homomorphism of $\mathrm{ULift}$ applied to $R$ and $\mathrm{ULift}$ applied to $S$ defined as the composition of the ring homomorphism of the inverse of the ring isomorphism and the composition of $f$ and the ring homomorphism of the ring isomorphism.

the ring isomorphism (from the name)

The ring isomorphism is a ring isomorphism of $\mathrm{ULift}$ applied to $R$ and $R$.