Definitions: Mathlib.Algebra, part 5 of 17

R is a Euclidean domain (from the name)

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

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be elements of $R$. Then the greatest common divisor of $a$ and $b$ is an element of $R$ defined as $\mathrm{EuclideanDomain\_\_gcd\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $a$ and $b$.

the greatest common divisor of x2 and y (from the name)

Let $x_{2}$ and $y$ be elements of $R$. Then the greatest common divisor of $x_{2}$ and $y$ is an element of $R$ defined as $\ProdfstMACRoZ {\operatorname{xgcd} (x_{2} , y)}$.

the greatest common divisor of x2 and y (from the name)

Let $x_{2}$ and $y$ be elements of $R$. Then the greatest common divisor of $x_{2}$ and $y$ is an element of $R$ defined as $\ProdsndMACRoAA {\operatorname{xgcd} (x_{2} , y)}$.

the least common multiple of x2 and y (from the name)

Let $x_{2}$ and $y$ be elements of $R$. Then the least common multiple of $x_{2}$ and $y$ is an element of $R$ defined as the quotient of $x_{2} \times y$ and the greatest common divisor of $x_{2}$ and $y$.

the quotient of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of $R$. Then the quotient of $x$ and $x_{1}$ is an element of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Let $x$ and $x_{1}$ be elements of $R$. Then $\operatorname{r}$ holds for $x$ and $x_{1}$, if $\operatorname{proj6}$ holds for $\mathrm{self}$, $x$ and $x_{1}$.

the remainder of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of $R$. Then the remainder of $x$ and $x_{1}$ is an element of $R$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Let $x_{2}$ and $y$ be elements of $R$. Then $\operatorname{xgcd}$ applied to $x_{2}$ and $y$ is an element of $\mathrm{Prod}$ applied to $R$ and $R$ defined as $\ProdsndMACRoAA {\operatorname{xgcdAux} (x_{2} , 1 , 0 , y , 0 , 1)}$.

Let $f$ be a function from elements of $M$ to elements of $N$. Let $g$ be a function from elements of $N$ to elements of $P$. Then $\operatorname{Exact}$ holds for $f$ and $g$, if for all elements $y$ of $N$, $\EqtMACRoH {g (y)}{0}$, if and only if $y$ is an element of the range of $f$.

the linear equivalence of h and hg (from the docstring)

Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Then the linear equivalence of $h$ and $\mathrm{hg}$ is a linear equivalence of the set of quotients of $N$ and the range of $f$ and $P$.

the split injective equivalence of h and hg (from the name)

Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Then the split injective equivalence of $h$ and $\mathrm{hg}$ is an element of $\EquivMACRoAE {(\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , f)}{\operatorname{id}})})}{(\SubtypeSet {e}{\mathrm{and} (\EqtMACRoH {f}{\operatorname{comp} (\operatorname{toLinearMap} (\operatorname{symm} (e)), \operatorname{inl} (M , P))}, \EqtMACRoH {g}{\operatorname{comp} (\operatorname{snd} (M , P), \operatorname{toLinearMap} (e))})})}$.

the split surjective equivalence of h and hf (from the name)

Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the split surjective equivalence of $h$ and $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (g , l)}{\operatorname{id}})})}{(\SubtypeSet {e}{\mathrm{and} (\EqtMACRoH {f}{\operatorname{comp} (\operatorname{toLinearMap} (\operatorname{symm} (e)), \operatorname{inl} (M , P))}, \EqtMACRoH {g}{\operatorname{comp} (\operatorname{snd} (M , P), \operatorname{toLinearMap} (e))})})}$.

Let $f$ be a function from elements of $M$ to elements of $N$. Let $g$ be a function from elements of $N$ to elements of $P$. Then $\operatorname{MulExact}$ holds for $f$ and $g$, if for all elements $y$ of $N$, $\EqtMACRoH {g (y)}{1}$, if and only if $y$ is an element of the range of $f$.

K is a division ring (from the name)

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

Let $x$ be a nonnegative rational number. Let $x_{1}$ be an element of $K$. Then $\operatorname{nnqsmul}$ applied to $x$ and $x_{1}$ is an element of $K$ defined as $\operatorname{proj14}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Let $x$ be a rational number. Let $x_{1}$ be an element of $K$. Then $\operatorname{qsmul}$ applied to $x$ and $x_{1}$ is an element of $K$ defined as $\operatorname{proj17}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

K is a division semiring (from the name)

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

Let $x$ be a nonnegative rational number. Let $x_{1}$ be an element of $K$. Then $\operatorname{nnqsmul}$ applied to $x$ and $x_{1}$ is an element of $K$ defined as $\operatorname{proj13}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

K is a field (from the name)

Let $K$ be a set. Then we can say that $K$ is a field.

Let $x$ be a nonnegative rational number. Let $x_{1}$ be an element of $K$. Then $\operatorname{nnqsmul}$ applied to $x$ and $x_{1}$ is an element of $K$ defined as $\operatorname{proj14}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Let $x$ be a rational number. Let $x_{1}$ be an element of $K$. Then $\operatorname{qsmul}$ applied to $x$ and $x_{1}$ is an element of $K$ defined as $\operatorname{proj17}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Let $q$ be a nonnegative rational number. Then $\operatorname{castRec}$ applied to $q$ is an element of $K$ defined as the quotient of the numerator of $q$ and the denominator of $q$.

Let $q$ be a rational number. Then $\operatorname{castRec}$ applied to $q$ is an element of $K$ defined as $\frac{ \operatorname{num} (q)}{\operatorname{den} (q)}$.

K is a semifield (from the name)

Let $K$ be a set. Then we can say that $K$ is a semifield.

Let $x$ be a nonnegative rational number. Let $x_{1}$ be an element of $K$. Then $\operatorname{nnqsmul}$ applied to $x$ and $x_{1}$ is an element of $K$ defined as $\operatorname{proj13}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

R is a field (from the name)

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

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

the subfield congruence of h (from the name)

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

Let $f$ and $g$ be ring homomorphisms of $K$ and $L$. Then $\operatorname{eqLocusField}$ applied to $f$ and $g$ is a subfield of $K$.

the range of f (from the docstring)

Let $f$ be a ring homomorphism of $K$ and $L$. Then the range of $f$ is a subfield of $L$.

Let $f$ be a ring homomorphism of $K$ and $L$. Then $\operatorname{rangeRestrictField}$ applied to $f$ is a ring homomorphism of $K$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{fieldRange} (f)}{x_{2}})}$ defined as $\operatorname{rangeSRestrict}$ applied to $f$.

Let $f$ be a ring homomorphism of $K$ and $L$. Then $\operatorname{rangeRestrictFieldEquiv}$ applied to $f$ is a ring isomorphism of $K$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{fieldRange} (f)}{x_{2}})}$ defined as the ring isomorphism of $\operatorname{rangeRestrictField}$ applied to $f$ and $\mathrm{RingHom\_\_rangeRestrictField\_bijective}$ applied to $f$.

the closure of s (from the name)

Let $s$ be an element of $\wp K$. Then the closure of $s$ is a subfield of $K$ 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 $K$ and $L$. Let $s$ be a subfield of $L$. Then the preimage of $f$ and $s$ is a subfield of $K$.

Let $K$ be a set. Then $\operatorname{gi}$ applied to $K$ 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 $K$ and $L$. Let $s$ be a subfield of $K$. Then the map of $f$ and $s$ is a subfield of $L$.

the top equivalence (from the name)

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

subfield of K (from the name)

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

the copy of S and s (from the name)

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

the subtype of s (from the name)

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

the additive subgroup of s (from the name)

Let $s$ be a subfield of $K$. Then the additive subgroup of $s$ is an additive subgroup of $K$ defined as the additive subgroup of $\operatorname{toSubring}$ applied to $s$.

Let $S$ and $K$ be sets. Then we can say that $\mathrm{SubfieldClass}$ holds for $S$ and $K$.

the subfield of s and hinv (from the name)

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

f has finite multiplicative supports (from the name)

Let $f$ be a function from elements of $x$ to elements of $M$. Then $f$ has finite multiplicative supports, if the multiplicative support of $f$ is finite.

f has finite supports (from the name)

Let $f$ be a function from elements of $x$ to elements of $M$. Then $f$ has finite supports, if the support of $f$ is finite.

Let $x$ be a set. Let $x_{2}$ and $x_{3}$ be elements of $x$. Then we can say that $\operatorname{AssocRel}$ holds for $x$, $x_{2}$ and $x_{3}$.

free additive semigroup of x (from the name)

Let $x$ be a set. Then a free additive semigroup of $x$ is an element of the function that maps $x$ to $\mathrm{Quot}$ applied to $\operatorname{AssocRel}$ applied to $x$.

the lift (from the name)

The lift is an equivalence from the set of additive homomorphisms of $x$ and $x_{2}$ to the set of additive homomorphisms of the set of free additive semigroups of $x$ and $x_{2}$.

the map of f (from the name)

Let $f$ be an additive homomorphism of $x$ and $x_{2}$. Then the map of $f$ is an additive homomorphism of the set of free additive semigroups of $x$ and the set of free additive semigroups of $x_{2}$ defined as $\operatorname{lift}$ applied to the composition of $\operatorname{of}$ and $f$.

$\operatorname{of}$ is an additive homomorphism of $x$ and the set of free additive semigroups of $x$.

free additive magma of x (from the name)

Let $x$ be a set. Then the free additive magmas of $x$ are a basic type.

the sum of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be free additive magmas of $x$. Then the sum of $x_{1}$ and $x_{2}$ is a free additive magma of $x$.

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 $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from free additive magmas $x_{2}$ of $x$ and free additive magmas $x_{3}$ of $x$ to elements of $\mathrm{motive}$ applied to the sum of $x_{2}$ and $x_{3}$.

the length of x1 (from the name)

Let $x_{1}$ be a free additive magma of $x$. Then the length of $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FreeAddMagma\_\_length\_\_\_f}$.

the lift (from the name)

The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of additive homomorphisms of the set of free additive magmas of $x$ and $x_{1}$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is an additive homomorphism of the set of free additive magmas of $x$ and the set of free additive magmas of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free additive magma of $x$.

Let $x_{1}$ be a free additive magma of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{of}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from free additive magmas $x_{2}$ of $x$ and free additive magmas $y$ of $x$ and elements of $C$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $x_{2} + y$. Then $\operatorname{recOnAdd}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOn}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$.

Let $x_{1}$ be a free additive magma of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{pure}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from free additive magmas $x_{2}$ of $x$ and free additive magmas $y$ of $x$ and elements of $C$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $x_{2} + y$. Then $\operatorname{recOnPure}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOnAdd}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$.

the representation of x2 (from the name)

Let $x_{2}$ be a free additive magma of $x$. Then the representation of $x_{2}$ is an element of $\operatorname{Format}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FreeAddMagma\_\_repr\_\_\_f}$.

the free additive semigroup (from the name)

The free additive semigroup is an additive homomorphism of the set of free additive magmas of $x$ and the set of free additive semigroups of $x$ defined as $\operatorname{lift}$ applied to $\operatorname{of}$.

the traverse of F and x3 (from the name)

Let $F$ be a function from elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $x_{3}$ be a free additive magma of $x_{1}$. Then the traverse of $F$ and $x_{3}$ is an element of $m$ applied to the set of free additive magmas of $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{FreeAddMagma\_\_traverse\_\_\_f}$ applied to $F$.

the free additive magma associator quotient equivalence of x (from the name)

Let $x$ be a set. Then the free additive magma associator quotient equivalence of $x$ is an additive equivalence of the set of free additive semigroups of the set of free additive magmas of $x$ and the set of free additive semigroups of $x$.

free additive semigroup of x (from the name)

Let $x$ be a set. Then the free additive semigroups of $x$ are a basic type.

the head of the element of self (from the docstring)

Let $\mathrm{self}$ be a free additive semigroup of $x$. Then the head of the element of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the length of x1 (from the name)

Let $x_{1}$ be a free additive semigroup of $x$. Then the length of $x_{1}$ is a natural number defined as the sum of $\operatorname{length}$ applied to the tail of the element of $x_{1}$ and $1$.

the lift (from the name)

The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of additive homomorphisms of the set of free additive semigroups of $x$ and $x_{1}$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is an additive homomorphism of the set of free additive semigroups of $x$ and the set of free additive semigroups of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free additive semigroup of $x$ defined as $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{nil}$.

Let $x_{1}$ be a free additive semigroup of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{of}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from elements $x_{2}$ of $x$ and free additive semigroups $y$ of $x$ and elements of $C$ applied to $\operatorname{of}$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $\operatorname{of} (x_{2})+ y$. Then $\operatorname{recOnAdd}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOn}$ applied to $x_{1}$, the function that maps $f$ and $s$ to $\operatorname{recOn}$ applied to $s$, $x_{5}$, the function that maps $\mathrm{hd}$, $\mathrm{tl}$, $\mathrm{ih}$ and $f_{1}$ to $\mathrm{ih1}$ applied to $f_{1}$, $\operatorname{mk}$ applied to $\mathrm{hd}$ and $\mathrm{tl}$, $x_{5}$ applied to $f_{1}$ and $\mathrm{ih}$ applied to $\mathrm{hd}$ and $f$, $x_{2}$, $y$ and $\mathrm{ih2}$.

Let $x_{1}$ be a free additive semigroup of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{pure}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from elements $x_{2}$ of $x$ and free additive semigroups $y$ of $x$ and elements of $C$ applied to $\operatorname{pure}$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $\operatorname{pure} (x_{2})+ y$. Then $\operatorname{recOnPure}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOnAdd}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$.

the tail of the element of self (from the docstring)

Let $\mathrm{self}$ be a free additive semigroup of $x$. Then the tail of the element of $\mathrm{self}$ is a list of elements of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the traverse of F and x3 (from the name)

Let $F$ be a function from elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $x_{3}$ be a free additive semigroup of $x_{1}$. Then the traverse of $F$ and $x_{3}$ is an element of $m$ applied to the set of free additive semigroups of $x_{2}$ defined as $\operatorname{recOnPure}$ applied to $x_{3}$, the function that maps $x_{4}$ to $\operatorname{map}$ applied to $\operatorname{pure}$ and $F$ applied to $x_{4}$ and the function that maps $\mathrm{\_x}$, $\mathrm{\_y}$, $\mathrm{ihx}$ and $\mathrm{ihy}$ to $\operatorname{seq}$ applied to $\operatorname{map}$ applied to the function that maps $x_{5}$ and $x_{6}$ to $x_{5} + x_{6}$ and $\mathrm{ihx}$ and the function that maps $x_{7}$ to $\mathrm{ihy}$.

free magma of x (from the name)

Let $x$ be a set. Then the free magmas of $x$ 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 $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from free magmas $x_{2}$ of $x$ and free magmas $x_{3}$ of $x$ to elements of $\mathrm{motive}$ applied to the product of $x_{2}$ and $x_{3}$.

the length of x1 (from the name)

Let $x_{1}$ be a free magma of $x$. Then the length of $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FreeMagma\_\_length\_\_\_f}$.

the lift (from the name)

The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of multiplicative homomorphisms of the set of free magmas of $x$ and $x_{1}$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a multiplicative homomorphism of the set of free magmas of $x$ and the set of free magmas of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.

the product of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be free magmas of $x$. Then the product of $x_{1}$ and $x_{2}$ is a free magma of $x$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free magma of $x$.

Let $x_{1}$ be a free magma of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{of}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from free magmas $x_{2}$ of $x$ and free magmas $y$ of $x$ and elements of $C$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $x_{2} \times y$. Then $\operatorname{recOnMul}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOn}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$.

Let $x_{1}$ be a free magma of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{pure}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from free magmas $x_{2}$ of $x$ and free magmas $y$ of $x$ and elements of $C$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $x_{2} \times y$. Then $\operatorname{recOnPure}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOnMul}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$.

the representation of x2 (from the name)

Let $x_{2}$ be a free magma of $x$. Then the representation of $x_{2}$ is an element of $\operatorname{Format}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FreeMagma\_\_repr\_\_\_f}$.

the free semigroup (from the name)

The free semigroup is a multiplicative homomorphism of the set of free magmas of $x$ and the set of free semigroups of $x$ defined as $\operatorname{lift}$ applied to $\operatorname{of}$.

the traverse of F and x3 (from the name)

Let $F$ be a function from elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $x_{3}$ be a free magma of $x_{1}$. Then the traverse of $F$ and $x_{3}$ is an element of $m$ applied to the set of free magmas of $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{FreeMagma\_\_traverse\_\_\_f}$ applied to $F$.

the free magma associator quotient equivalence of x (from the name)

Let $x$ be a set. Then the free magma associator quotient equivalence of $x$ is a multiplicative equivalence of the set of associator quotients of the set of free magmas of $x$ and the set of free semigroups of $x$.

free semigroup of x (from the name)

Let $x$ be a set. Then the free semigroups of $x$ are a basic type.

the head of the element of self (from the docstring)

Let $\mathrm{self}$ be a free semigroup of $x$. Then the head of the element of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the length of x1 (from the name)

Let $x_{1}$ be a free semigroup of $x$. Then the length of $x_{1}$ is a natural number defined as the sum of $\operatorname{length}$ applied to the tail of the element of $x_{1}$ and $1$.

the lift (from the name)

The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of multiplicative homomorphisms of the set of free semigroups of $x$ and $x_{1}$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a multiplicative homomorphism of the set of free semigroups of $x$ and the set of free semigroups of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free semigroup of $x$ defined as $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{nil}$.

Let $x_{1}$ be a free semigroup of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{of}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from elements $x_{2}$ of $x$ and free semigroups $y$ of $x$ and elements of $C$ applied to $\operatorname{of}$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $\operatorname{of} (x_{2})\times y$. Then $\operatorname{recOnMul}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOn}$ applied to $x_{1}$, the function that maps $f$ and $s$ to $\operatorname{recOn}$ applied to $s$, $x_{5}$, the function that maps $\mathrm{hd}$, $\mathrm{tl}$, $\mathrm{ih}$ and $f_{1}$ to $\mathrm{ih1}$ applied to $f_{1}$, $\operatorname{mk}$ applied to $\mathrm{hd}$ and $\mathrm{tl}$, $x_{5}$ applied to $f_{1}$ and $\mathrm{ih}$ applied to $\mathrm{hd}$ and $f$, $x_{2}$, $y$ and $\mathrm{ih2}$.

Let $x_{1}$ be a free semigroup of $x$. Let $\mathrm{ih1}$ be a function from elements $x_{5}$ of $x$ to elements of $C$ applied to $\operatorname{pure}$ applied to $x_{5}$. Let $\mathrm{ih2}$ be a function from elements $x_{2}$ of $x$ and free semigroups $y$ of $x$ and elements of $C$ applied to $\operatorname{pure}$ applied to $x_{2}$ and elements of $C$ applied to $y$ to elements of $C$ applied to $\operatorname{pure} (x_{2})\times y$. Then $\operatorname{recOnPure}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $x_{2}$, $y$ and $\mathrm{ih2}$ to $\operatorname{recOnMul}$ applied to $x_{1}$, $x_{5}$, $\mathrm{ih1}$, $x_{2}$, $y$ and $\mathrm{ih2}$.

the tail of the element of self (from the docstring)

Let $\mathrm{self}$ be a free semigroup of $x$. Then the tail of the element of $\mathrm{self}$ is a list of elements of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the traverse of F and x3 (from the name)

Let $F$ be a function from elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $x_{3}$ be a free semigroup of $x_{1}$. Then the traverse of $F$ and $x_{3}$ is an element of $m$ applied to the set of free semigroups of $x_{2}$ defined as $\operatorname{recOnPure}$ applied to $x_{3}$, the function that maps $x_{4}$ to $\operatorname{map}$ applied to $\operatorname{pure}$ and $F$ applied to $x_{4}$ and the function that maps $\mathrm{\_x}$, $\mathrm{\_y}$, $\mathrm{ihx}$ and $\mathrm{ihy}$ to $\operatorname{seq}$ applied to $\operatorname{map}$ applied to the function that maps $x_{5}$ and $x_{6}$ to $x_{5} \times x_{6}$ and $\mathrm{ihx}$ and the function that maps $x_{7}$ to $\mathrm{ihy}$.

associator quotient of x (from the name)

Let $x$ be a set. Then an associator quotient of $x$ is an element of the function that maps $x$ to $\mathrm{Quot}$ applied to $\operatorname{AssocRel}$ applied to $x$.

the lift (from the name)

The lift is an equivalence from the set of multiplicative homomorphisms of $x$ and $x_{2}$ to the set of multiplicative homomorphisms of the set of associator quotients of $x$ and $x_{2}$.

the map of f (from the name)

Let $f$ be a multiplicative homomorphism of $x$ and $x_{2}$. Then the map of $f$ is a multiplicative homomorphism of the set of associator quotients of $x$ and the set of associator quotients of $x_{2}$ defined as $\operatorname{lift}$ applied to the composition of $\operatorname{of}$ and $f$.

$\operatorname{of}$ is a multiplicative homomorphism of $x$ and the set of associator quotients of $x$.

Let $x$ be a set. Let $x_{2}$ and $x_{3}$ be elements of $x$. Then we can say that $\operatorname{AssocRel}$ holds for $x$, $x_{2}$ and $x_{3}$.

the group homomorphism (from the docstring)

The group homomorphism is an additive monoid homomorphism of $\FinsuppMACRoQ {X}{\Integer}$ and the set of free Abelian groups of $X$ defined as $\operatorname{liftAddHom}$ applied to the function that maps $x_{1}$ to $\operatorname{flip}$ applied to the scalar multiple additive homomorphism of $\Integer$ and the set of free Abelian groups of $X$ and $\operatorname{of}$ applied to $x_{1}$.

the coefficient of x (from the name)

Let $x$ be an element of $X$. Then the coefficient of $x$ is an additive monoid homomorphism of the set of free Abelian groups of $X$ and $\Integer$ defined as the composition of $\operatorname{applyAddHom}$ applied to $x$ and the finitely supported function.

the equivalence finitely supported function of X (from the name)

Let $X$ be a set. Then the equivalence finitely supported function of $X$ is an additive equivalence of the set of free Abelian groups of $X$ and $\FinsuppMACRoQ {X}{\Integer}$.

the support of a (from the name)

Let $a$ be a free Abelian group of $X$. Then the support of $a$ is a finite set of $X$ defined as $\FinsuppsupportMACRoR {\operatorname{toFinsupp} (a)}$.

the finitely supported function (from the name)

The finitely supported function is an additive monoid homomorphism of the set of free Abelian groups of $X$ and $\FinsuppMACRoQ {X}{\Integer}$ defined as $\operatorname{lift}$ applied to the function that maps $x_{1}$ to $\FinsuppsingleMACRoS {x_{1}}{1}$.

free algebra of R and X (from the name)

Let $R$ and $X$ be sets. Then a free algebra of $R$ and $X$ is an element of the function that maps $R$ and $X$ to $\mathrm{Quot}$ applied to $\operatorname{Rel}$ applied to $R$ and $X$.

Let $R$ and $X$ be sets. Then the elements of $\operatorname{Pre}$ applied to $R$ and $X$ are a basic type.

the sum of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of $\operatorname{Pre}$ applied to $R$ and $X$. Then the sum of $x$ and $x_{1}$ is an element of $\operatorname{Pre}$ applied to $R$ and $X$.

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 the set of functions from elements $x$ of $X$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $R$ to elements of $\mathrm{motive}$ applied to $\operatorname{ofScalar}$ applied to $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $\operatorname{Pre}$ applied to $R$ and $X$ and elements $x_{3}$ of $\operatorname{Pre}$ applied to $R$ and $X$ to elements of $\mathrm{motive}$ applied to the sum of $x_{2}$ and $x_{3}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{4}$ of $\operatorname{Pre}$ applied to $R$ and $X$ and elements $x_{5}$ of $\operatorname{Pre}$ applied to $R$ and $X$ to elements of $\mathrm{motive}$ applied to the product of $x_{4}$ and $x_{5}$.

the product of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of $\operatorname{Pre}$ applied to $R$ and $X$. Then the product of $x$ and $x_{1}$ is an element of $\operatorname{Pre}$ applied to $R$ and $X$.

Let $x$ be an element of $X$. Then $\operatorname{of}$ applied to $x$ is an element of $\operatorname{Pre}$ applied to $R$ and $X$.

Let $x$ be an element of $R$. Then $\operatorname{ofScalar}$ applied to $x$ is an element of $\operatorname{Pre}$ applied to $R$ and $X$.

Let $R$ and $X$ be sets. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Pre}$ applied to $R$ and $X$. Then we can say that $\operatorname{Rel}$ holds for $R$, $X$, $x_{1}$ and $x_{2}$.

Assume that $\operatorname{Rel}$ holds for $R$, $X$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

the algebra map inverse (from the name)

The algebra map inverse is an algebra homomorphism of the set of free algebras of $R$ and $X$ and $R$ defined as $\operatorname{lift}$ applied to $R$ and $0$.

the equivalence monoid algebra free monoid (from the name)

The equivalence monoid algebra free monoid is an algebra isomorphism of the set of free algebras of $R$ and $X$ and the set of monoid algebras of $R$ and the set of free monoids of $X$.

the lift of R (from the name)

Let $R$ be a set. Then the lift of $R$ is an equivalence from the set of functions from elements of $X$ to elements of $A$ to the set of algebra homomorphisms of the set of free algebras of $R$ and $X$ and $A$.

the lift function of f and x3 (from the name)

Let $R$ and $X$ be sets. Let $f$ be a function from elements of $X$ to elements of $A$. Let $x_{3}$ be an element of $\operatorname{Pre}$ applied to $R$ and $X$. Then the lift function of $f$ and $x_{3}$ is an element of $A$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{FreeAlgebra\_\_liftFun\_\_\_f}$ applied to $R$, $X$ and $f$.

the inclusion of R and x1 (from the name)

Let $R$ be a set. Let $x_{1}$ be an element of $X$. Then the inclusion of $R$ and $x_{1}$ is a free algebra of $R$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{FreeAlgebra\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_FreeAlgebra\_\_2097919375\_\_\_hygCtx\_\_\_hyg\_\_2}$, $R$ and $x_{1}$.

free additive monoid of x (from the name)

Let $x$ be a set. Then a free additive monoid of $x$ is an element of the function that maps $x$ to the set of lists of elements of $x$.

Let $\mathrm{xs}$ be a free additive monoid of $x$. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{of\_add}$ be a function from elements $x_{1}$ of $x$ and free additive monoids $\mathrm{xs1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{of} (x_{1})+ \mathrm{xs1}$. Then $\operatorname{casesOn}$ applied to $\mathrm{xs}$, $\mathrm{zero}$, $x_{1}$, $\mathrm{xs1}$ and $\mathrm{of\_add}$ is an element of $\mathrm{motive}$ applied to $\mathrm{xs}$.

the free additive monoid congruence of e (from the name)

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the free additive monoid congruence of $e$ is an additive equivalence of the set of free additive monoids of $x$ and the set of free additive monoids of $x_{1}$.

the length of a (from the docstring)

Let $a$ be a free additive monoid of $x$. Then the length of $a$ is a natural number defined as $\operatorname{length}$ applied to $\operatorname{toList}$ applied to $a$.

the lift (from the name)

The lift is an equivalence from the set of functions from elements of $x$ to elements of $M$ to the set of additive monoid homomorphisms of the set of free additive monoids of $x$ and $M$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is an additive monoid homomorphism of the set of free additive monoids of $x$ and the set of free additive monoids of $x_{1}$.

Let $a$ be a free additive monoid of $x$. Let $m$ be an element of $x$. Then $\operatorname{mem}$ holds for $a$ and $m$, if $\MembershipmemMACRoT {\operatorname{toList} (a)}{m}$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free additive monoid of $x$ defined as $\operatorname{ofList}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $\operatorname{nil}$.

the free additive monoid (from the name)

The free additive monoid is an equivalence from the set of lists of elements of $x$ to the set of free additive monoids of $x$ defined as the identity of the set of lists of elements of $x$.

Let $\mathrm{xs}$ be a free additive monoid of $x$. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{of\_add}$ be a function from elements $x_{1}$ of $x$ and free additive monoids $\mathrm{xs1}$ of $x$ and elements of $\mathrm{motive}$ applied to $\mathrm{xs1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{of} (x_{1})+ \mathrm{xs1}$. Then $\operatorname{recOn}$ applied to $\mathrm{xs}$, $\mathrm{zero}$, $x_{1}$, $\mathrm{xs1}$ and $\mathrm{of\_add}$ is an element of $\mathrm{motive}$ applied to $\mathrm{xs}$.

the reverse of x1 (from the name)

Let $x_{1}$ be a free additive monoid of $x$. Then the reverse of $x_{1}$ is a free additive monoid of $x$ defined as $\operatorname{reverse}$ applied to $x_{1}$.

the list (from the name)

The list is an equivalence from the set of free additive monoids of $x$ to the set of lists of elements of $x$ defined as the identity of the set of free additive monoids of $x$.

free monoid of x (from the name)

Let $x$ be a set. Then a free monoid of $x$ is an element of the function that maps $x$ to the set of lists of elements of $x$.

Let $\mathrm{xs}$ be a free monoid of $x$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{of\_mul}$ be a function from elements $x_{1}$ of $x$ and free monoids $\mathrm{xs1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{of} (x_{1})\times \mathrm{xs1}$. Then $\operatorname{casesOn}$ applied to $\mathrm{xs}$, $\mathrm{one}$, $x_{1}$, $\mathrm{xs1}$ and $\mathrm{of\_mul}$ is an element of $\mathrm{motive}$ applied to $\mathrm{xs}$.

the free monoid congruence of e (from the name)

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the free monoid congruence of $e$ is a multiplicative equivalence of the set of free monoids of $x$ and the set of free monoids of $x_{1}$.

the length of a (from the docstring)

Let $a$ be a free monoid of $x$. Then the length of $a$ is a natural number defined as $\operatorname{length}$ applied to $\operatorname{toList}$ applied to $a$.

the lift (from the name)

The lift is an equivalence from the set of functions from elements of $x$ to elements of $M$ to the set of monoid homomorphisms of the set of free monoids of $x$ and $M$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a monoid homomorphism of the set of free monoids of $x$ and the set of free monoids of $x_{1}$.

Let $a$ be a free monoid of $x$. Let $m$ be an element of $x$. Then $\operatorname{mem}$ holds for $a$ and $m$, if $\MembershipmemMACRoT {\operatorname{toList} (a)}{m}$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free monoid of $x$ defined as $\operatorname{ofList}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $\operatorname{nil}$.

the free monoid (from the name)

The free monoid is an equivalence from the set of lists of elements of $x$ to the set of free monoids of $x$ defined as the identity of the set of lists of elements of $x$.

Let $\mathrm{xs}$ be a free monoid of $x$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{of\_mul}$ be a function from elements $x_{1}$ of $x$ and free monoids $\mathrm{xs1}$ of $x$ and elements of $\mathrm{motive}$ applied to $\mathrm{xs1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{of} (x_{1})\times \mathrm{xs1}$. Then $\operatorname{recOn}$ applied to $\mathrm{xs}$, $\mathrm{one}$, $x_{1}$, $\mathrm{xs1}$ and $\mathrm{of\_mul}$ is an element of $\mathrm{motive}$ applied to $\mathrm{xs}$.

the reverse of x1 (from the name)

Let $x_{1}$ be a free monoid of $x$. Then the reverse of $x_{1}$ is a free monoid of $x$ defined as $\operatorname{reverse}$ applied to $x_{1}$.

the list (from the name)

The list is an equivalence from the set of free monoids of $x$ to the set of lists of elements of $x$ defined as the identity of the set of free monoids of $x$.

the count of x2 (from the name)

Let $x_{2}$ be an element of $x$. Then the count of $x_{2}$ is an additive monoid homomorphism of the set of free additive monoids of $x$ and $\Natural$ defined as the count of the function that maps $x_{3}$ to $\EqtMACRoH {x_{3}}{x_{2}}$.

the count of p (from the name)

Let $p$ be a function from elements of $x$ to propositions. Then the count of $p$ is an additive monoid homomorphism of the set of free additive monoids of $x$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{countP'}$ applied to $p$ and $\mathrm{FreeAddMonoid\_\_countP'\_zero}$ applied to $p$ and $\mathrm{FreeAddMonoid\_\_countP'\_add}$ applied to $p$.

the count of p and l (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a free additive monoid of $x$. Then the count of $p$ and $l$ is a natural number defined as $\operatorname{countP}$ applied to the function that maps $b$ to $\operatorname{decide}$ applied to $p$ applied to $b$ and $\operatorname{toList}$ applied to $l$.

the count of x2 (from the name)

Let $x_{2}$ be an element of $x$. Then the count of $x_{2}$ is a monoid homomorphism of the set of free monoids of $x$ and the set of multiplicatives of $\Natural$ defined as the count of the function that maps $x_{3}$ to $\EqtMACRoH {x_{3}}{x_{2}}$.

the count of p (from the name)

Let $p$ be a function from elements of $x$ to propositions. Then the count of $p$ is a monoid homomorphism of the set of free monoids of $x$ and the set of multiplicatives of $\Natural$.

the count of p and l (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a free monoid of $x$. Then the count of $p$ and $l$ is a natural number defined as $\operatorname{countP}$ applied to the function that maps $b$ to $\operatorname{decide}$ applied to $p$ applied to $b$ and $\operatorname{toList}$ applied to $l$.

the equivalence with zero free additive semigroup (from the name)

The equivalence with zero free additive semigroup is an additive equivalence of the set of free additive monoids of $x$ and $\mathrm{WithZero}$ applied to the set of free additive semigroups of $x$.

the free additive monoid (from the name)

The free additive monoid is an additive homomorphism of the set of free additive semigroups of $x$ and the set of free additive monoids of $x$ defined as $\operatorname{lift}$ applied to $\operatorname{of}$.

the equivalence with one free semigroup (from the name)

The equivalence with one free semigroup is a multiplicative equivalence of the set of free monoids of $x$ and $\mathrm{WithOne}$ applied to the set of free semigroups of $x$.

the natural embedding of the free semigroup into the free monoid (from the docstring)

The natural embedding of the free semigroup into the free monoid is a multiplicative homomorphism of the set of free semigroups of $x$ and the set of free monoids of $x$ defined as $\operatorname{lift}$ applied to $\operatorname{of}$.

the symbol of a (from the name)

Let $a$ be a free additive monoid of $x$. Then the symbol of $a$ is a finite set of $x$ defined as the finite set of $a$.

the symbol of a (from the name)

Let $a$ be a free monoid of $x$. Then the symbol of $a$ is a finite set of $x$ defined as the finite set of $a$.

Let $R$ and $X$ be sets. Then an element of $\mathrm{FreeNonUnitalNonAssocAlgebra}$ applied to $R$ and $X$ is an element of the function that maps $R$ and $X$ to the set of monoid algebras of $R$ and the set of free magmas of $X$.

the lift of R (from the name)

Let $R$ be a set. Then the lift of $R$ is an equivalence from the set of functions from elements of $X$ to elements of $A$ to the set of non unital algebra homomorphisms of $\mathrm{FreeNonUnitalNonAssocAlgebra}$ applied to $R$ and $X$ and $A$ defined as the composition of the lift and the lift magma of $R$.

Let $R$ be a set. Let $x_{1}$ be an element of $X$. Then $\operatorname{of}$ applied to $R$ and $x_{1}$ is an element of $\mathrm{FreeNonUnitalNonAssocAlgebra}$ applied to $R$ and $X$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the embedding of $R$ and the set of free magmas of $X$, $\operatorname{of}$ and $x_{1}$.

Let $x_{3}$ be an associate of $x$. Then $\operatorname{out}$ applied to $x_{3}$ is an element of $x$.

x is a greatest common divisor monoid (from the name)

Let $x$ be a set. Then we can say that $x$ is a greatest common divisor monoid.

the greatest common divisor of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then the greatest common divisor of $x_{2}$ and $x_{3}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

the least common multiple of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then the least common multiple of $x_{2}$ and $x_{3}$ is an element of $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

x is a greatest common divisor monoid (from the name)

Let $x$ be a set. Then we can say that $x$ is a greatest common divisor monoid.

x is a normalization monoid (from the name)

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

the norm unit of x2 (from the name)

Let $x_{2}$ be an element of $x$. Then the norm unit of $x_{2}$ is a unit of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

x is a normalized greatest common divisor monoid (from the name)

Let $x$ be a set. Then we can say that $x$ is a normalized greatest common divisor monoid.

x is a strong normalization monoid (from the name)

Let $x$ be a set. Then we can say that $x$ is a strong normalization monoid.

x is a strong normalized greatest common divisor monoid (from the name)

Let $x$ be a set. Then we can say that $x$ is a strong normalized greatest common divisor monoid.

the associate equivalence (from the name)

The associate equivalence is a multiplicative equivalence of the set of associates of $x$ and $x$.

Let $x_{3}$ be an element of $x$. Then $\mathrm{normalize}$ applied to $x_{3}$ is an element of $x$ defined as the product of $x_{3}$ and the underlying value in the base of the norm unit of $x_{3}$.

$\mathrm{normalizeHom}$ is a monoid with zero homomorphism of $x$ and $x$.

the greatest common divisor of s and f (from the name)

Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the greatest common divisor of $s$ and $f$ is an element of $x$ defined as the fold of $f$ and $s$.

the least common multiple of s and f (from the name)

Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the least common multiple of $s$ and $f$ is an element of $x$ defined as the fold of $f$ and $s$.

the greatest common divisor of s (from the name)

Let $s$ be a multiset of $x$. Then the greatest common divisor of $s$ is an element of $x$ defined as the fold of $0$ and $s$.

the least common multiple of s (from the name)

Let $s$ be a multiset of $x$. Then the least common multiple of $s$ is an element of $x$ defined as the fold of $1$ and $s$.

the associate integer equivalence natural number (from the name)

The associate integer equivalence natural number is an equivalence from the set of associates of $\Integer$ to $\Natural$.

the equivalence of e and i (from the name)

Let $e$ be an element of $E$. Let $i$ be an element of $x_{2}$. Then the equivalence of $e$ and $i$ is an equivalence from $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{5} (i)}{x_{8}})}$ to $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{6} (i)}{x_{9}})}$.

the subtype map of i and x8 (from the name)

Let $f$ be an element of $F$. Let $i$ be an element of $x_{2}$. Let $x_{8}$ be an element of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {x_{5} (i)}{x_{10}})}$. Then the subtype map of $i$ and $x_{8}$ is an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{6} (i)}{x_{9}})}$ defined as $f$ applied to $x_{8}$.

Let $E$ be a set. Let $x_{5}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x_{2}$ to elements of $x$. Let $x_{6}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x_{2}$ to elements of $x_{1}$. Then we can say that $\mathrm{GradedEquivLike}$ holds for $E$, $x_{5}$ and $x_{6}$.

Let $F$ be a set. Let $x_{5}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x_{2}$ to elements of $x$. Let $x_{6}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x_{2}$ to elements of $x_{1}$. Then we can say that $\mathrm{GradedFunLike}$ holds for $F$, $x_{5}$ and $x_{6}$.

graded monoid of A (from the name)

Let $A$ be a function from elements of $x$ to sets. Then a graded monoid of $A$ is an element of the function that maps $A$ to $\Sigma$ applied to $A$.

A is a commutative monoid (from the name)

Let $A$ be a function from elements of $x$ to sets. Then we can say that $A$ is a commutative monoid.

A is a monoid (from the name)

Let $A$ be a function from elements of $x$ to sets. Then we can say that $A$ is a monoid.

Let $n$ be a natural number. Let $x_{2}$ be an element of $A$ applied to $i$. Then $\operatorname{gnpow}$ applied to $n$ and $x_{2}$ is an element of $A$ applied to $\HSMulhSMulMACRoAL {n}{i}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$, $n$ and $x_{2}$.

Let $n$ be a natural number. Let $x_{4}$ be an element of $A$ applied to $i$. Then $\operatorname{gnpowRec}$ applied to $n$ and $x_{4}$ is an element of $A$ applied to $\HSMulhSMulMACRoAL {n}{i}$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{GradedMonoid\_\_GMonoid\_\_gnpowRec\_\_\_f}$, $i$ and $x_{4}$.

A is a product (from the name)

Let $A$ be a function from elements of $x$ to sets. Then we can say that $A$ is a product.

the product of x2 and x3 (from the name)

Let $x_{2}$ be an element of $A$ applied to $i$. Let $x_{3}$ be an element of $A$ applied to $j$. Then the product of $x_{2}$ and $x_{3}$ is an element of $A$ applied to $i + j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

A is a one (from the name)

Let $A$ be a function from elements of $x$ to sets. Then we can say that $A$ is an one.

the one (from the name)

The one is an element of $A$ applied to $0$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $i$ be an element of $x$. Let $x_{1}$ be an element of $A$ applied to $i$. Then $\operatorname{mk}$ applied to $i$ and $x_{1}$ is a graded monoid of $A$ defined as $\operatorname{mk}$ applied to $i$ and $x_{1}$.

the zero monoid homomorphism of A (from the name)

Let $A$ be a function from elements of $x$ to sets. Then the zero monoid homomorphism of $A$ is a monoid homomorphism of $A$ applied to $0$ and the set of graded monoids of $A$.

the product of x4 and fA (from the name)

Let $l$ be a list of elements of $x_{1}$. Let $x_{4}$ be a function from elements of $x_{1}$ to elements of $x$. Let $\mathrm{fA}$ be a function from elements $a$ of $x_{1}$ to elements of $A$ applied to $x_{4}$ applied to $a$. Then the product of $x_{4}$ and $a$ is an element of $A$ applied to the product index of $l$ and $x_{4}$ defined as the function that maps $\mathrm{fA}$ to $\operatorname{foldrRecOn}$ applied to $l$, the function that maps $i$ and $b$ to $x_{4} (i)+ b$, the one, the function that maps $x_{5}$, $x_{6}$, $a$ and $h$ to the product of $a$ applied to $a$ and $x_{6}$ and $\mathrm{fA}$.

the product index of l and x3 (from the name)

Let $l$ be a list of elements of $x_{1}$. Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $x$. Then the product index of $l$ and $x_{3}$ is an element of $x$ defined as $\operatorname{foldr}$ applied to the function that maps $i$ and $b$ to $x_{3} (i)+ b$, $0$ and $l$.

the submonoid of A (from the docstring)

Let $A$ be a function from elements of $x$ to elements of $S$. Then the submonoid of $A$ is a submonoid of $R$.

A is a graded monoid (from the name)

Let $A$ be a function from elements of $x$ to elements of $S$. Then we can say that $A$ is a graded monoid.

A is a graded product (from the name)

Let $A$ be a function from elements of $x$ to elements of $S$. Then we can say that $A$ is a graded product.

A is a graded one (from the name)

Let $A$ be a function from elements of $x$ to elements of $S$. Then we can say that $A$ is a graded one.

Let $A$ be a function from elements of $x$ to elements of $S$. Let $a$ be an element of $R$. Then $\operatorname{IsHomogeneousElem}$ holds for $A$ and $a$, if there exists an element $i$ of $x$, such that $\MembershipmemMACRoT {A (i)}{a}$.

the homogeneous submonoid of A (from the name)

Let $A$ be a function from elements of $x$ to elements of $S$. Then the homogeneous submonoid of $A$ is a submonoid of $R$.

Let $A$ be a function from elements of $x$ to sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then we can say that $\operatorname{GMulAction}$ holds for $A$ and $M$.

Let $A$ be a function from elements of $x$ to sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then we can say that $\operatorname{GSMul}$ holds for $A$ and $M$.

the homogeneous multiplication map of x3 and x4 (from the docstring)

Let $x_{3}$ be an element of $A$ applied to $i$. Let $x_{4}$ be an element of $M$ applied to $j$. Then the homogeneous multiplication map of $x_{3}$ and $x_{4}$ is an element of $M$ applied to the sum of $i$ and $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.

Let $A$ be a function from elements of $x$ to elements of $S$. Let $B$ be a function from elements of $x_{1}$ to elements of $N$. Then we can say that $\operatorname{GradedSMul}$ holds for $A$ and $B$.

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

Let $M$ and $x$ be sets. Then the additive action of $M$ and $x$ is an embedding of $x$ and the set of functions from elements of $M$ to elements of $x$.

the permutation of a (from the name)

Let $a$ be an element of $x$. Then the permutation of $a$ is a permutation of $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $x_{4}$ to the sum of $a$ and $x_{4}$, the function that maps $x_{5}$ to the sum of $\operatorname{neg}$ applied to $a$ and $x_{5}$, $\mathrm{neg\_vadd\_vadd}$ applied to $a$ and $\mathrm{vadd\_neg\_vadd}$ applied to $a$.

the multiplicative action of M and x (from the name)

Let $M$ and $x$ be sets. Then the multiplicative action of $M$ and $x$ is an embedding of $x$ and the set of functions from elements of $M$ to elements of $x$.

the permutation of a (from the name)

Let $a$ be an element of $x$. Then the permutation of $a$ is a permutation of $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $x_{4}$ to $\HSMulhSMulMACRoAL {a}{x_{4}}$, the function that maps $x_{5}$ to $\HSMulhSMulMACRoAL {\operatorname{inv} (a)}{x_{5}}$, $\mathrm{inv\_smul\_smul}$ applied to $a$ and $\mathrm{smul\_inv\_smul}$ applied to $a$.

the monoid end of M and A (from the name)

Let $M$ and $A$ be sets. Then the monoid end of $M$ and $A$ is a monoid homomorphism of $M$ and the set of ends of $A$.

the monoid homomorphism of A and r (from the name)

Let $A$ be a set. Let $r$ be an element of $M$. Then the monoid homomorphism of $A$ and $r$ is a monoid homomorphism of $A$ and $A$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $\HSMulhSMulMACRoAL {r}{x_{3}}$ and $\mathrm{MulDistribMulAction\_\_smul\_one}$ applied to $r$ and $\mathrm{smul\_mul'}$ applied to $r$.

Let $G$ and $P$ be sets. Then we can say that $\mathrm{AddAction}$ holds for $G$ and $P$.

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

Let $G$ and $P$ be sets. Then we can say that $\mathrm{AddSemigroupAction}$ holds for $G$ and $P$.

G is cancellative (from the docstring)

Let $G$ and $P$ be sets. Then we can say that $G$ is cancellative.

G is cancellative (from the docstring)

Let $G$ and $P$ be sets. Then we can say that $G$ is cancellative.

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

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

Let $G$ and $P$ be sets. Then we can say that $\mathrm{IsLeftCancelSMul}$ holds for $G$ and $P$.

Let $G$ and $P$ be sets. Then we can say that $\mathrm{IsLeftCancelVAdd}$ holds for $G$ and $P$.

Let $M$, $N$ and $x$ be sets. Then we can say that $\mathrm{IsScalarTower}$ holds for $M$, $N$ and $x$.

the bundled map over different ring (from the name)

The bundled map over different ring is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{MulAction}$ holds for $x$ and $x_{1}$.

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

Let $M$, $N$ and $x$ be sets. Then we can say that $\mathrm{SMulCommClass}$ holds for $M$, $N$ and $x$.

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

Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{SemigroupAction}$ holds for $x$ and $x_{1}$.

Let $M$, $N$ and $x$ be sets. Then we can say that $\mathrm{VAddAssocClass}$ holds for $M$, $N$ and $x$.

Let $M$, $N$ and $x$ be sets. Then we can say that $\mathrm{VAddCommClass}$ holds for $M$, $N$ and $x$.

the end homomorphism (from the name)

The end homomorphism is an additive monoid homomorphism of $M$ and $\mathrm{Additive}$ applied to the set of ends of $x$ defined as $\operatorname{toAdditiveRight}$ applied to the end homomorphism.

the permutation homomorphism of G and x (from the name)

Let $G$ and $x$ be sets. Then the permutation homomorphism of $G$ and $x$ is an additive monoid homomorphism of $G$ and $\mathrm{Additive}$ applied to the set of permutations of $x$ defined as $\operatorname{toAdditiveRight}$ applied to the permutation homomorphism of the set of multiplicatives of $G$ and $x$.

the end homomorphism (from the name)

The end homomorphism is a monoid homomorphism of $M$ and the set of ends of $x$.

the permutation homomorphism of G and x (from the name)

Let $G$ and $x$ be sets. Then the permutation homomorphism of $G$ and $x$ is a monoid homomorphism of $G$ and the set of permutations of $x$.

the multiplicative automorphism of G and M (from the name)

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

the multiplicative equivalence of M and x3 (from the name)

Let $M$ be a set. Let $x_{3}$ be an element of $G$. Then the multiplicative equivalence of $M$ and $x_{3}$ is a multiplicative equivalence of $M$ and $M$.

the multiplicative automorphism arrow (from the name)

The multiplicative automorphism arrow is a monoid homomorphism of $G$ and the set of multiplicative automorphisms of the set of functions from elements of $A$ to elements of $M$ defined as the multiplicative automorphism of $G$ and the set of functions from elements of $A$ to elements of $M$.

Let $X$ and $G$ be sets. Then the elements of $\mathrm{Equidecomp}$ applied to $X$ and $G$ are a basic type.

Let $f$ be a function from elements of $X$ to elements of $X$. Let $A$ be an element of $\wp X$. Let $S$ be a finite set of $G$. Then $\operatorname{IsDecompOn}$ holds for $f$, $A$ and $S$, if for all elements $a$ of $X$, if $a$ is an element of $A$, then there exists an element $g$ of $G$, such that $g$ is an element of $S$ and $\EqtMACRoH {f (a)}{\HSMulhSMulMACRoAL {g}{a}}$.

the identity function of X and G (from the docstring)

Let $X$ and $G$ be sets. Then the identity function of $X$ and $G$ is an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$.

the restriction of f and A (from the docstring)

Let $f$ be an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$. Let $A$ be an element of $\wp X$. Then the restriction of $f$ and $A$ is an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$.

the inverse function of f (from the docstring)

Let $f$ be an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$. Then the inverse function of $f$ is an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$.

the composition of f and g (from the name)

Let $f$ and $g$ be elements of $\mathrm{Equidecomp}$ applied to $X$ and $G$. Then the composition of $f$ and $g$ is an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$.

the set of witness of f (from the name)

Let $f$ be an element of $\mathrm{Equidecomp}$ applied to $X$ and $G$. Then the set of witness of $f$ is a finite set of $G$ defined as $\operatorname{choose}$ applied to $\operatorname{isDecompOn'}$ applied to $f$.

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

Let $G$ and $P$ be sets. Then we can say that $\mathrm{FaithfulVAdd}$ holds for $G$ and $P$.

the vector sum zero homomorphism (from the name)

The vector sum zero homomorphism is an additive monoid homomorphism of $M$ and $N$.

the scalar multiple one homomorphism (from the name)

The scalar multiple one homomorphism is a monoid homomorphism of $M$ and $N$.

the additive monoid homomorphism equivalence additive action additive associator class of M and N (from the name)

Let $M$ and $N$ be sets. Then the additive monoid homomorphism equivalence additive action additive associator class of $M$ and $N$ is an equivalence from the set of additive monoid homomorphisms of $M$ and $N$ to $\SubtypeSet {\mathrm{\_inst}}{\mathrm{VAddAssocClass} (M , N , N)}$.

Let $M$ and $N$ be sets. Then $\mathrm{monoidHomEquivMulActionIsScalarTower}$ applied to $M$ and $N$ is an equivalence from the set of monoid homomorphisms of $M$ and $N$ to $\SubtypeSet {\mathrm{\_inst}}{\mathrm{IsScalarTower} (M , N , N)}$.

Let $M$ and $x$ be sets. Then we can say that $\operatorname{IsPretransitive}$ holds for $M$ and $x$.

Let $M$ and $x$ be sets. Then we can say that $\operatorname{IsPretransitive}$ holds for $M$ and $x$.

the product equivalence of N and x (from the name)

Let $M$, $N$ and $x$ be sets. Then the product equivalence of $N$ and $x$ is an element of $\EquivMACRoAE {\mathrm{AddAction} (\mathrm{Prod} (M , N), x)}{\mathrm{PSigma} (\lambda x_{3} . \mathrm{PSigma} (\lambda x_{4} . \mathrm{VAddCommClass} (M , N , x)))}$.

the product equivalence of N and x (from the name)

Let $M$, $N$ and $x$ be sets. Then the product equivalence of $N$ and $x$ is an element of $\EquivMACRoAE {\mathrm{MulAction} (\mathrm{Prod} (M , N), x)}{\mathrm{PSigma} (\lambda x_{3} . \mathrm{PSigma} (\lambda x_{4} . \mathrm{SMulCommClass} (M , N , x)))}$.

the scalar multiple monoid homomorphism (from the name)

The scalar multiple monoid homomorphism is a monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

the scalar multiple multiplicative homomorphism (from the name)

The scalar multiple multiplicative homomorphism is a multiplicative homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

additive characteristic of A and M (from the name)

Let $A$ and $M$ be sets. Then the additive characteristics of $A$ and $M$ are a basic type.

the composition additive monoid homomorphism of x3 and f (from the name)

Let $x_{3}$ be an additive characteristic of $B$ and $M$. Let $f$ be an additive monoid homomorphism of $A$ and $B$. Then the composition additive monoid homomorphism of $x_{3}$ and $f$ is an additive characteristic of $A$ and $M$ defined as $\operatorname{symm}$ applied to the additive monoid homomorphism equivalence and the composition of the additive monoid homomorphism of $x_{3}$ and $f$.

the double dual embedding (from the docstring)

The double dual embedding is an additive monoid homomorphism of $A$ and the set of additive characteristics of the set of additive characteristics of $A$ and $M$ and $M$.

the multiplicative shift of x2 and r (from the name)

Let $x_{2}$ be an additive characteristic of $R$ and $M$. Let $r$ be an element of $R$. Then the multiplicative shift of $x_{2}$ and $r$ is an additive characteristic of $R$ and $M$ defined as the composition additive monoid homomorphism of $x_{2}$ and the left multiplicative of $r$.

the additive monoid additive equivalence (from the name)

The additive monoid additive equivalence is an additive equivalence of $\mathrm{Additive}$ applied to the set of additive characteristics of $A$ and $M$ and the set of additive monoid homomorphisms of $A$ and $\mathrm{Additive}$ applied to $M$.

the additive monoid homomorphism of x2 (from the name)

Let $x_{2}$ be an additive characteristic of $A$ and $M$. Then the additive monoid homomorphism of $x_{2}$ is an additive monoid homomorphism of $A$ and $\mathrm{Additive}$ applied to $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $x_{2}$ and $\mathrm{AddChar\_\_map\_zero\_eq\_one'}$ applied to $x_{2}$ and $\mathrm{AddChar\_\_map\_add\_eq\_mul'}$ applied to $x_{2}$.

the additive monoid homomorphism equivalence (from the name)

The additive monoid homomorphism equivalence is an equivalence from the set of additive characteristics of $A$ and $M$ to the set of additive monoid homomorphisms of $A$ and $\mathrm{Additive}$ applied to $M$.

the additive characteristic of self and x2 (from the name)

Let $\mathrm{self}$ be an additive characteristic of $A$ and $M$. Let $x_{2}$ be an element of $A$. Then the additive characteristic of $\mathrm{self}$ and $x_{2}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

the monoid homomorphism of x2 (from the name)

Let $x_{2}$ be an additive characteristic of $A$ and $M$. Then the monoid homomorphism of $x_{2}$ is a monoid homomorphism of the set of multiplicatives of $A$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $x_{2}$ and $\mathrm{AddChar\_\_map\_zero\_eq\_one'}$ applied to $x_{2}$ and $\mathrm{AddChar\_\_map\_add\_eq\_mul'}$ applied to $x_{2}$.

the monoid homomorphism equivalence (from the name)

The monoid homomorphism equivalence is an equivalence from the set of additive characteristics of $A$ and $M$ to the set of monoid homomorphisms of the set of multiplicatives of $A$ and $M$.

the monoid homomorphism multiplicative equivalence (from the name)

The monoid homomorphism multiplicative equivalence is a multiplicative equivalence of the set of additive characteristics of $A$ and $M$ and the set of monoid homomorphisms of the set of multiplicatives of $A$ and $M$.

the composition additive characteristic of f and x3 (from the name)

Let $f$ be a monoid homomorphism of $M$ and $N$. Let $x_{3}$ be an additive characteristic of $A$ and $M$. Then the composition additive characteristic of $f$ and $x_{3}$ is an additive characteristic of $A$ and $N$ defined as $\operatorname{symm}$ applied to the monoid homomorphism equivalence and the composition of $f$ and the monoid homomorphism of $x_{3}$.

Let $z$ be an element of $M$. Then we can say that $\mathrm{IsAddCentral}$ holds for $z$.

Let $z$ be an element of $M$. Then we can say that $\mathrm{IsMulCentral}$ holds for $z$.

the center of M (from the docstring)

Let $M$ be a set. Then the center of $M$ is an element of $\wp M$ defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to $\mathrm{IsAddCentral}$ applied to $z$.

the centralizer of S (from the docstring)

Let $S$ be an element of $\wp M$. Then the centralizer of $S$ is an element of $\wp M$ defined as $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that for all elements $m$ of $M$, if $m$ is an element of $S$, then $\EqtMACRoH {m + c}{c + m}$.

the center of M (from the docstring)

Let $M$ be a set. Then the center of $M$ is an element of $\wp M$ defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to $\mathrm{IsMulCentral}$ applied to $z$.

the centralizer of S (from the docstring)

Let $S$ be an element of $\wp M$. Then the centralizer of $S$ is an element of $\wp M$ defined as $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that for all elements $m$ of $M$, if $m$ is an element of $S$, then $\EqtMACRoH {m \times c}{c \times m}$.

the left of a and b (from the name)

Let $u$ be an additive unit of $M$. Let $a$ and $b$ be elements of $M$ such that $a + b$ is equal to the underlying value in the base of $u$ and $\mathrm{AddCommute}$ holds for $a$ and $b$. Then the left of $a$ and $b$ is an additive unit of $M$.

the additive unit of u and x1 (from the name)

Let $u$ be an additive unit of $M$. Let $x_{1}$ be an element of $M$. Assume that $n \neq 0$. Assume that $\HSMulhSMulMACRoAL {n}{x_{1}}$ is equal to the underlying value in the base of $u$. Then the additive unit of $u$ and $x_{1}$ is an additive unit of $M$.

the additive unit of a and n (from the name)

Let $a$ be an element of $M$. Let $n$ be a natural number such that $\EqtMACRoH {\HSMulhSMulMACRoAL {n}{a}}{0}$ and $n \neq 0$. Then the additive unit of $a$ and $n$ is an additive unit of $M$ defined as the additive unit of $0$ and $a$.

the right of a and b (from the name)

Let $u$ be an additive unit of $M$. Let $a$ and $b$ be elements of $M$ such that $a + b$ is equal to the underlying value in the base of $u$ and $\mathrm{AddCommute}$ holds for $a$ and $b$. Then the right of $a$ and $b$ is an additive unit of $M$.

the left of a and b (from the name)

Let $u$ be a unit of $M$. Let $a$ and $b$ be elements of $M$ such that $a \times b$ is equal to the underlying value in the base of $u$ and $\mathrm{Commute}$ holds for $a$ and $b$. Then the left of $a$ and $b$ is a unit of $M$.

the unit of u and x1 (from the name)

Let $u$ be a unit of $M$. Let $x_{1}$ be an element of $M$. Assume that $n \neq 0$. Assume that $x_{1} ^ {n}$ is equal to the underlying value in the base of $u$. Then the unit of $u$ and $x_{1}$ is a unit of $M$.

the unit of a and n (from the name)

Let $a$ be an element of $M$. Let $n$ be a natural number such that $\EqtMACRoH {a ^ {n}}{1}$ and $n \neq 0$. Then the unit of $a$ and $n$ is a unit of $M$ defined as the unit of $1$ and $a$.

the right of a and b (from the name)

Let $u$ be a unit of $M$. Let $a$ and $b$ be elements of $M$ such that $a \times b$ is equal to the underlying value in the base of $u$ and $\mathrm{Commute}$ holds for $a$ and $b$. Then the right of $a$ and $b$ is a unit of $M$.

additive conjugate class of x (from the name)

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

the carrier of x2 (from the name)

Let $x_{2}$ be an additive conjugate class of $x$. Then the carrier of $x_{2}$ is an element of $\wp x$ defined as $\operatorname{lift}$ applied to $\mathrm{addConjugatesOf}$, the function that maps $x_{2}$, $x_{3}$ and $\mathrm{ab}$ to $\mathrm{IsAddConj\_\_addConjugatesOf\_eq}$ applied to $\mathrm{ab}$ and $x_{2}$.

the map of f and x4 (from the name)

Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an additive conjugate class of $x$. Then the map of $f$ and $x_{4}$ is an additive conjugate class of $x_{1}$.

Let $a$ be an element of $x$. Then $\operatorname{mk}$ applied to $a$ is an additive conjugate class of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $x$ and $a$.

the equivalence (from the name)

The equivalence is an equivalence from $x$ to the set of additive conjugate classes of $x$.

conjugate class of x (from the name)

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

the carrier of x2 (from the name)

Let $x_{2}$ be a conjugate class of $x$. Then the carrier of $x_{2}$ is an element of $\wp x$ defined as $\operatorname{lift}$ applied to $\mathrm{conjugatesOf}$, the function that maps $x_{2}$, $x_{3}$ and $\mathrm{ab}$ to $\mathrm{IsConj\_\_conjugatesOf\_eq}$ applied to $\mathrm{ab}$ and $x_{2}$.

the map of f and x4 (from the name)

Let $f$ be a monoid homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be a conjugate class of $x$. Then the map of $f$ and $x_{4}$ is a conjugate class of $x_{1}$.

Let $a$ be an element of $x$. Then $\operatorname{mk}$ applied to $a$ is a conjugate class of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $x$ and $a$.

the equivalence (from the name)

The equivalence is an equivalence from $x$ to the set of conjugate classes of $x$.

a is a additive conjugate with respect to b (from the name)

Let $a$ and $b$ be elements of $x$. Then $a$ is an additive conjugate with respect to $b$, if there exists an additive unit $c$ of $x$, such that $\mathrm{AddSemiconjBy}$ holds for the underlying value in the base of $c$, $a$ and $b$.

a is conjugate to b (from the name)

Let $a$ and $b$ be elements of $x$. Then $a$ is conjugate to $b$, if there exists a unit $c$ of $x$, such that $\mathrm{SemiconjBy}$ holds for the underlying value in the base of $c$, $a$ and $b$.

the additive conjugate of a (from the name)

Let $a$ be an element of $x$. Then the additive conjugate of $a$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that $a$ is an additive conjugate with respect to $b$.

the conjugate of a (from the name)

Let $a$ be an element of $x$. Then the conjugate of $a$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that $a$ is conjugate to $b$.

G is a additive commutative group (from the name)

Let $G$ be a set. Then we can say that $G$ is an additive commutative group.

A is a additive group (from the name)

Let $A$ be a set. Then we can say that $A$ is an additive group.

G is a commutative group (from the name)

Let $G$ be a set. Then we can say that $G$ is a commutative group.

G is a group (from the name)

Let $G$ be a set. Then we can say that $G$ is a group.

G is a quotient inverse monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a quotient inverse monoid.

the quotient of a and b (from the name)

Let $a$ and $b$ be elements of $G$. Then the quotient of $a$ and $b$ is an element of $G$ defined as $a \times \operatorname{inv} (b)$.

G is a quotient inverse one monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a quotient inverse one monoid.

G is a division commutative monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a division commutative monoid.

G is a division monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a division monoid.

G is a inverse one class (from the name)

Let $G$ be a set. Then we can say that $G$ is an inverse one class.

G is cyclic (from the docstring)

Let $G$ be a set. Then we can say that $G$ is cyclic.

G is cyclic (from the docstring)

Let $G$ be a set. Then we can say that $G$ is cyclic.

G is a negation zero class (from the name)

Let $G$ be a set. Then we can say that $G$ is a negation zero class.

G is a difference negation monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a difference negation monoid.

the difference of a and b (from the name)

Let $a$ and $b$ be elements of $G$. Then the difference of $a$ and $b$ is an element of $G$ defined as $a + \operatorname{neg} (b)$.

G is a difference negation zero monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a difference negation zero monoid.

G is a subtraction commutative monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a subtraction commutative monoid.

G is a subtraction monoid (from the name)

Let $G$ be a set. Then we can say that $G$ is a subtraction monoid.

G is a power (from the name)

Let $G$ be a set. Then we can say that $G$ is a power.

the integer power of x and x1 (from the name)

Let $x$ be an integer. Let $x_{1}$ be an element of $G$. Then the integer power of $x$ and $x_{1}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

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

the integer multiple of x and x1 (from the name)

Let $x$ be an integer. Let $x_{1}$ be an element of $G$. Then the integer multiple of $x$ and $x_{1}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Let $\mathrm{npow}$ be an element of $\mathrm{optParam}$ applied to the set of functions from natural numbers and elements of $G$ to elements of $G$ and $\mathrm{npowRec}$. Let $x_{3}$ be an integer. Let $x_{4}$ be an element of $G$. Then $\mathrm{zpowRec}$ applied to $\mathrm{npow}$, $x_{3}$ and $x_{4}$ is an element of $G$.

Let $\mathrm{nsmul}$ be an element of $\mathrm{optParam}$ applied to the set of functions from natural numbers and elements of $G$ to elements of $G$ and $\mathrm{nsmulRec}$. Let $x_{3}$ be an integer. Let $x_{4}$ be an element of $G$. Then $\mathrm{zsmulRec}$ applied to $\mathrm{nsmul}$, $x_{3}$ and $x_{4}$ is an element of $G$.

the additive left embedding of g (from the name)

Let $g$ be an element of $G$. Then the additive left embedding of $g$ is an embedding of $G$ and $G$ defined as $\operatorname{mk}$ applied to the function that maps $h_{1}$ to $g + h_{1}$ and $\mathrm{add\_right\_injective}$ applied to $g$.

the additive right embedding of g (from the name)

Let $g$ be an element of $G$. Then the additive right embedding of $g$ is an embedding of $G$ and $G$ defined as $\operatorname{mk}$ applied to the function that maps $h_{1}$ to $h_{1} + g$ and $\mathrm{add\_left\_injective}$ applied to $g$.

the multiplicative left embedding of g (from the name)

Let $g$ be an element of $G$. Then the multiplicative left embedding of $g$ is an embedding of $G$ and $G$ defined as $\operatorname{mk}$ applied to the function that maps $h_{1}$ to $g \times h_{1}$ and $\mathrm{mul\_right\_injective}$ applied to $g$.

the multiplicative right embedding of g (from the name)

Let $g$ be an element of $G$. Then the multiplicative right embedding of $g$ is an embedding of $G$ and $G$ defined as $\operatorname{mk}$ applied to the function that maps $h_{1}$ to $h_{1} \times g$ and $\mathrm{mul\_left\_injective}$ applied to $g$.

additive automorphism of M (from the name)

Let $M$ be a set. Then an additive automorphism of $M$ is an element of the function that maps $M$ to the set of additive equivalences of $M$ and $M$.

the additive conjugate (from the name)

The additive conjugate is an additive monoid homomorphism of $G$ and the set of additive automorphisms of $G$.

the congruence of x2 (from the name)

Let $x_{2}$ be an additive equivalence of $G$ and $H$. Then the congruence of $x_{2}$ is an additive equivalence of the set of additive automorphisms of $G$ and the set of additive automorphisms of $H$.

the permutation of A (from the name)

Let $A$ be a set. Then the permutation of $A$ is an additive monoid homomorphism of the set of additive automorphisms of $A$ and $\mathrm{Additive}$ applied to the set of permutations of $A$.

Let $G$ be a set. Then $\mathrm{AddAutAdditive}$ applied to $G$ is an additive equivalence of the set of additive automorphisms of $\mathrm{Additive}$ applied to $G$ and $\mathrm{Additive}$ applied to the set of multiplicative automorphisms of $G$.

the equivalence unit end (from the name)

The equivalence unit end is a multiplicative equivalence of the set of permutations of $x$ and the set of units of the set of ends of $x$.

Let $f$ be an equivalence from $x$ to $\SubtypeSet {x_{3}}{p (x_{3})}$. Then $\operatorname{extendDomainHom}$ applied to $f$ is a monoid homomorphism of the set of permutations of $x$ and the set of permutations of $x_{1}$.

the permutation (from the name)

The permutation is a monoid homomorphism of the set of permutations of $\SubtypeSet {x_{2}}{p (x_{2})}$ and the set of permutations of $x$.

the sigma congruence right homomorphism of x1 (from the name)

Let $x_{1}$ be a function from elements of $x$ to sets. Then the sigma congruence right homomorphism of $x_{1}$ is a monoid homomorphism of the set of functions from elements $a$ of $x$ to permutations of $x_{1}$ applied to $a$ and the set of permutations of $\Sigma$ applied to the function that maps $a_{1}$ to $x_{1}$ applied to $a_{1}$.

the subtype congruence homomorphism of p (from the name)

Let $p$ be a function from elements of $x$ to propositions. Then the subtype congruence homomorphism of $p$ is a monoid homomorphism of $\mathrm{Prod}$ applied to the set of permutations of $\SubtypeSet {a}{p (a)}$ and the set of permutations of $\SubtypeSet {a_{1}}{\mathrm{not} (p (a_{1}))}$ and the set of permutations of $x$.

the subtype equivalence subtype permutation of p (from the name)

Let $p$ be a function from elements of $x$ to propositions. Then the subtype equivalence subtype permutation of $p$ is an equivalence from the set of permutations of $\SubtypeSet {x_{2}}{p (x_{2})}$ to $\SubtypeSet {f}{\mathrm{forall} (x , \lambda a . \mathrm{if} (\mathrm{not} (p (a)), \EqtMACRoH {f (a)}{a}))}$.

the subtype permutation of f and h (from the name)

Let $f$ be a permutation of $x$ such that for all elements $x_{2}$ of $x$, $p$ holds for $f$ applied to $x_{2}$, if and only if $p$ holds for $x_{2}$. Then the subtype permutation of $f$ and $h$ is a permutation of $\SubtypeSet {x_{1}}{p (x_{1})}$.

the sum congruence homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the sum congruence homomorphism of $x$ and $x_{1}$ is a monoid homomorphism of $\mathrm{Prod}$ applied to the set of permutations of $x$ and the set of permutations of $x_{1}$ and the set of permutations of $\mathrm{Sum}$ applied to $x$ and $x_{1}$.

the permutation congruence homomorphism of e (from the name)

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the permutation congruence homomorphism of $e$ is a multiplicative equivalence of the set of permutations of $x$ and the set of permutations of $x_{1}$ defined as $\operatorname{mk}$ applied to the permutation congruence of $e$ and the function that maps $p$ and $q$ to $\mathrm{Equiv\_\_permCongr\_mul}$ applied to $e$, $p$ and $q$.

end of x (from the name)

Let $x$ be a set. Then an end of $x$ is an element of the function that maps $x$ to the set of functions from elements of $x$ to elements of $x$.

the homomorphism permutation of f (from the name)

Let $f$ be a monoid homomorphism of $G$ and the set of ends of $x$. Then the homomorphism permutation of $f$ is a monoid homomorphism of $G$ and the set of permutations of $x$ defined as the composition of the monoid homomorphism of the inverse of the equivalence unit end and the homomorphism unit of $f$.

multiplicative automorphism of M (from the name)

Let $M$ be a set. Then a multiplicative automorphism of $M$ is an element of the function that maps $M$ to the set of multiplicative equivalences of $M$ and $M$.

the congruence of x2 (from the name)

Let $x_{2}$ be a multiplicative equivalence of $G$ and $H$. Then the congruence of $x_{2}$ is a multiplicative equivalence of the set of multiplicative automorphisms of $G$ and the set of multiplicative automorphisms of $H$.

the conjugate (from the name)

The conjugate is a monoid homomorphism of $G$ and the set of multiplicative automorphisms of $G$.

the permutation of M (from the name)

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

the multiplicative automorphism multiplicative of G (from the name)

Let $G$ be a set. Then the multiplicative automorphism multiplicative of $G$ is a multiplicative equivalence of the set of multiplicative automorphisms of the set of multiplicatives of $G$ and the set of multiplicatives of the set of additive automorphisms of $G$.

the left additive monoid homomorphism congruence of e (from the name)

Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then the left additive monoid homomorphism congruence of $e$ is an additive equivalence of the set of additive monoid homomorphisms of $x$ and $N$ and the set of additive monoid homomorphisms of $x_{1}$ and $N$.

the equivalence of e (from the docstring)

Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then the equivalence of $e$ is an equivalence from the set of additive monoid homomorphisms of $x$ and $N$ to the set of additive monoid homomorphisms of $x_{1}$ and $N$.

the right additive monoid homomorphism congruence of e (from the name)

Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then the right additive monoid homomorphism congruence of $e$ is an additive equivalence of the set of additive monoid homomorphisms of $M$ and $x$ and the set of additive monoid homomorphisms of $M$ and $x_{1}$.

the equivalence of e (from the docstring)

Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then the equivalence of $e$ is an equivalence from the set of additive monoid homomorphisms of $M$ and $x$ to the set of additive monoid homomorphisms of $M$ and $x_{1}$.

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

Let $f$ be an equivalence from $M$ to $N$. Let $g$ be an additive equivalence of $P$ and $Q$. Then the arrow congruence of $f$ and $g$ is an additive equivalence of the set of functions from elements of $M$ to elements of $P$ and the set of functions from elements of $N$ to elements of $Q$.

Let $x$ and $M$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $M$ is an additive equivalence of the set of functions from elements of $x$ to elements of $M$ and $M$.

the additive equivalence (from the name)

The additive equivalence is an additive equivalence of $M$ and $N$.

the right product congruence of es (from the name)

Let $\mathrm{es}$ be a function from elements $j_{2}$ of $x$ to additive equivalences of $\mathrm{Ms}$ applied to $j_{2}$ and $\mathrm{Ns}$ applied to $j_{2}$. Then the right product congruence of $j_{2}$ is an additive equivalence of the set of functions from elements $j$ of $x$ to elements of $\mathrm{Ms}$ applied to $j$ and the set of functions from elements $j_{1}$ of $x$ to elements of $\mathrm{Ns}$ applied to $j_{1}$.

Let $M$ be a function from elements of $x$ to sets. Then $\operatorname{piUnique}$ applied to $M$ is an additive equivalence of the set of functions from elements $j$ of $x$ to elements of $M$ applied to $j$ and $M$ applied to $\operatorname{default}$.

the inverse of G (from the name)

Let $G$ be a set. Then the inverse of $G$ is a permutation of $G$ defined as the permutation of $\operatorname{inv}$ and $\mathrm{inv\_involutive}$.

the negation of G (from the name)

Let $G$ be a set. Then the negation of $G$ is a permutation of $G$ defined as the permutation of $\operatorname{neg}$ and $\mathrm{neg\_involutive}$.

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

Let $f$ be an equivalence from $M$ to $N$. Let $g$ be a multiplicative equivalence of $P$ and $Q$. Then the arrow congruence of $f$ and $g$ is a multiplicative equivalence of the set of functions from elements of $M$ to elements of $P$ and the set of functions from elements of $N$ to elements of $Q$.

Let $x$ and $M$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $M$ is a multiplicative equivalence of the set of functions from elements of $x$ to elements of $M$ and $M$.

the left monoid homomorphism congruence of e (from the name)

Let $e$ be a multiplicative equivalence of $x$ and $x_{1}$. Then the left monoid homomorphism congruence of $e$ is a multiplicative equivalence of the set of monoid homomorphisms of $x$ and $N$ and the set of monoid homomorphisms of $x_{1}$ and $N$.

the equivalence of e (from the docstring)

Let $e$ be a multiplicative equivalence of $x$ and $x_{1}$. Then the equivalence of $e$ is an equivalence from the set of monoid homomorphisms of $x$ and $N$ to the set of monoid homomorphisms of $x_{1}$ and $N$.

the right monoid homomorphism congruence of e (from the name)

Let $e$ be a multiplicative equivalence of $x$ and $x_{1}$. Then the right monoid homomorphism congruence of $e$ is a multiplicative equivalence of the set of monoid homomorphisms of $M$ and $x$ and the set of monoid homomorphisms of $M$ and $x_{1}$.

the equivalence of e (from the docstring)

Let $e$ be a multiplicative equivalence of $x$ and $x_{1}$. Then the equivalence of $e$ is an equivalence from the set of monoid homomorphisms of $M$ and $x$ to the set of monoid homomorphisms of $M$ and $x_{1}$.

the multiplicative equivalence (from the name)

The multiplicative equivalence is a multiplicative equivalence of $M$ and $N$.

the right product congruence of es (from the name)

Let $\mathrm{es}$ be a function from elements $j_{2}$ of $x$ to multiplicative equivalences of $\mathrm{Ms}$ applied to $j_{2}$ and $\mathrm{Ns}$ applied to $j_{2}$. Then the right product congruence of $j_{2}$ is a multiplicative equivalence of the set of functions from elements $j$ of $x$ to elements of $\mathrm{Ms}$ applied to $j$ and the set of functions from elements $j_{1}$ of $x$ to elements of $\mathrm{Ns}$ applied to $j_{1}$.

Let $M$ be a function from elements of $x$ to sets. Then $\operatorname{piUnique}$ applied to $M$ is a multiplicative equivalence of the set of functions from elements $j$ of $x$ to elements of $M$ applied to $j$ and $M$ applied to $\operatorname{default}$.

additive equivalence of A and B (from the name)

Let $A$ and $B$ be sets. Then the additive equivalences of $A$ and $B$ are a basic type.

the cast of h (from the name)

Assume that $\EqtMACRoH {i}{j}$. Then the cast of $h$ is an additive equivalence of $M$ applied to $i$ and $M$ applied to $j$.

Let $f$ be an equivalence from $M$ to $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\EqtMACRoH {f (x_{2} + y)}{f (x_{2})+ f (y)}$. Then $\operatorname{mk'}$ applied to $f$ and $h$ is an additive equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$ and $h$.

the additive equivalence 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 additive equivalence of $f$ and $\mathrm{hf}$ is an additive equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to the equivalence of $\operatorname{coe}$ applied to $f$ and $\mathrm{hf}$ and $\mathrm{map\_add}$ applied to $f$.

the identity map of M (from the docstring)

Let $M$ be a set. Then the identity map of $M$ is an additive equivalence of $M$ and $M$.

the inverse of h (from the docstring)

Let $h$ be an additive equivalence of $M$ and $N$. Then the inverse of $h$ is an additive equivalence of $N$ and $M$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toEquiv}$ applied to $h$ and $\mathrm{AddEquiv\_\_symm\_map\_add}$ applied to $h$.

the inverse equivalence of P and Q (from the name)

Let $P$ and $Q$ be sets. Then the inverse equivalence of $P$ and $Q$ is an equivalence from the set of additive equivalences of $P$ and $Q$ to the set of additive equivalences of $Q$ and $P$.

the additive homomorphism of self (from the name)

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

the additive monoid homomorphism of h (from the name)

Let $h$ be an additive equivalence of $M$ and $N$. Then the additive monoid homomorphism of $h$ is an additive monoid homomorphism of $M$ and $N$.

the composition of h1 and h2 (from the name)

Let $h_{1}$ be an additive equivalence of $M$ and $N$. Let $h_{2}$ be an additive equivalence of $N$ and $P$. Then the composition of $h_{1}$ and $h_{2}$ is an additive equivalence of $M$ and $P$.

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

the additive equivalence of f (from the name)

Let $f$ be an element of $F$. Then the additive equivalence of $f$ is an additive equivalence of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the equivalence of $f$ and $\mathrm{AddHom\_\_map\_add'}$ applied to the additive homomorphism of $f$.

the additive equivalence of f and g (from the name)

Let $f$ be an additive homomorphism of $M$ and $N$. Let $g$ be an additive homomorphism of $N$ and $M$ such that the composition of $g$ and $f$ is equal to the identity map of $M$ and the composition of $f$ and $g$ is equal to the identity map of $N$. Then the additive equivalence of $f$ and $g$ is an additive equivalence of $M$ and $N$.

the equivalence of M (from the name)

Let $M$ be a set. Then the equivalence of $M$ is an equivalence from the set of ends of $M$ to the set of additive monoid homomorphisms of $M$ and $M$.

the additive equivalence of f and g (from the name)

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $g$ be an additive monoid homomorphism of $N$ and $M$ such that the composition of $g$ and $f$ is equal to the identity map of $M$ and the composition of $f$ and $g$ is equal to the identity map of $N$. Then the additive equivalence of $f$ and $g$ is an additive equivalence of $M$ and $N$.

the equivalence of M (from the name)

Let $M$ be a set. Then the equivalence of $M$ is an equivalence from the set of ends of $M$ to the set of monoid homomorphisms of $M$ and $M$.

the multiplicative equivalence of f and g (from the name)

Let $f$ be a monoid homomorphism of $M$ and $N$. Let $g$ be a monoid homomorphism of $N$ and $M$ such that the composition of $g$ and $f$ is equal to the identity map of $M$ and the composition of $f$ and $g$ is equal to the identity map of $N$. Then the multiplicative equivalence of $f$ and $g$ is a multiplicative equivalence of $M$ and $N$.

multiplicative equivalence of M and N (from the name)

Let $M$ and $N$ be sets. Then the multiplicative equivalences of $M$ and $N$ are a basic type.

the cast of h (from the name)

Assume that $\EqtMACRoH {i}{j}$. Then the cast of $h$ is a multiplicative equivalence of $M$ applied to $i$ and $M$ applied to $j$.

Let $f$ be an equivalence from $M$ to $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\EqtMACRoH {f (x_{2} \times y)}{f (x_{2})\times f (y)}$. Then $\operatorname{mk'}$ applied to $f$ and $h$ is a multiplicative equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$ and $h$.

the multiplicative equivalence 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 multiplicative equivalence of $f$ and $\mathrm{hf}$ is a multiplicative equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to the equivalence of $\operatorname{coe}$ applied to $f$ and $\mathrm{hf}$ and $\mathrm{map\_mul}$ applied to $f$.

the identity map of M (from the docstring)

Let $M$ be a set. Then the identity map of $M$ is a multiplicative equivalence of $M$ and $M$.

the inverse of h (from the docstring)

Let $h$ be a multiplicative equivalence of $M$ and $N$. Then the inverse of $h$ is a multiplicative equivalence of $N$ and $M$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toEquiv}$ applied to $h$ and $\mathrm{MulEquiv\_\_symm\_map\_mul}$ applied to $h$.

the inverse equivalence of P and Q (from the name)

Let $P$ and $Q$ be sets. Then the inverse equivalence of $P$ and $Q$ is an equivalence from the set of multiplicative equivalences of $P$ and $Q$ to the set of multiplicative equivalences of $Q$ and $P$.

the monoid homomorphism of h (from the name)

Let $h$ be a multiplicative equivalence of $M$ and $N$. Then the monoid homomorphism of $h$ is a monoid homomorphism of $M$ and $N$.

the multiplicative homomorphism of self (from the name)

Let $\mathrm{self}$ be a multiplicative equivalence of $M$ and $N$. Then the multiplicative homomorphism of $\mathrm{self}$ is a multiplicative homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{MulEquiv\_\_map\_mul'}$ applied to $\mathrm{self}$.

the composition of h1 and h2 (from the name)

Let $h_{1}$ be a multiplicative equivalence of $M$ and $N$. Let $h_{2}$ be a multiplicative equivalence of $N$ and $P$. Then the composition of $h_{1}$ and $h_{2}$ is a multiplicative equivalence of $M$ and $P$.

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

the multiplicative equivalence of f (from the name)

Let $f$ be an element of $F$. Then the multiplicative equivalence of $f$ is a multiplicative equivalence of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the equivalence of $f$ and $\mathrm{MulHom\_\_map\_mul'}$ applied to the multiplicative homomorphism of $f$.

the multiplicative equivalence of f and g (from the name)

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Let $g$ be a multiplicative homomorphism of $N$ and $M$ such that the composition of $g$ and $f$ is equal to the identity map of $M$ and the composition of $f$ and $g$ is equal to the identity map of $N$. Then the multiplicative equivalence of $f$ and $g$ is a multiplicative equivalence of $M$ and $N$.