Definitions: Mathlib.Algebra, part 4 of 17

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of additive commutative monoid categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive commutative monoid categories and the set of additive monoid categories.

the chosen cone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of additive commutative monoid categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of additive commutative monoid categories and the set of additive monoid categories.

the limit cone of F (from the name)

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

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

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

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

the section additive submonoid of F (from the name)

Let $F$ be a functor of $J$ and the set of additive monoid categories. Then the section additive submonoid of $F$ is an additive submonoid of the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of commutative monoid categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative monoid categories and the set of monoid categories.

the chosen cone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of commutative monoid categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative monoid categories and the set of monoid categories.

the limit cone of F (from the name)

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

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

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

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

the section submonoid of F (from the name)

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

the shrink functor of F (from the name)

Let $F$ be a functor of $C$ and the set of monoid categories. Then the shrink functor of $F$ is a functor of $C$ and the set of monoid categories.

the shrink functor map of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the shrink functor map of $x_{1}$ is a homomorphism of the shrink functor of $F$ and the shrink functor of $G$.

the Coyoneda (from the name)

The Coyoneda is a functor of the set of opposites of the set of additive commutative monoid categories and the set of functors of the set of additive commutative monoid categories and the set of additive commutative monoid categories.

$\operatorname{coyonedaForget}$ is an isomorphism of the composition of the Coyoneda and the action of the right whiskering of the set of additive commutative monoid categories and the set of sets and the forgetful functor of the set of additive commutative monoid categories and the Coyoneda.

the Coyoneda type (from the name)

The Coyoneda type is a functor of the set of opposites of the set of sets and the set of functors of the set of additive commutative monoid categories and the set of additive commutative monoid categories.

the Coyoneda (from the name)

The Coyoneda is a functor of the set of opposites of the set of commutative monoid categories and the set of functors of the set of commutative monoid categories and the set of commutative monoid categories.

$\operatorname{coyonedaForget}$ is an isomorphism of the composition of the Coyoneda and the action of the right whiskering of the set of commutative monoid categories and the set of sets and the forgetful functor of the set of commutative monoid categories and the Coyoneda.

the Coyoneda type (from the name)

The Coyoneda type is a functor of the set of opposites of the set of sets and the set of functors of the set of commutative monoid categories and the set of commutative monoid categories.

the adjoint (from the name)

The adjoint is an adjunction of the free functor and the forgetful functor of the set of categories of commutative rings.

the Coyoneda (from the name)

The Coyoneda is a functor of the set of opposites of the set of sets and the set of functors of the set of categories of commutative rings and the set of categories of commutative rings.

the Coyoneda adjoint of R (from the name)

Let $R$ be a category of commutative rings. Then the Coyoneda adjoint of $R$ is an adjunction of the right opposite of the action of the flip of the Coyoneda and $R$ and the action of the Yoneda and $R$.

$\operatorname{coyonedaUnique}$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $n$ and the identity of the set of categories of commutative rings.

Let $\mathrm{hR}$ be an element of $\operatorname{IsInitial}$ applied to $R$. Then $\mathrm{CommRingCat\_\_forget\_u2082\_Adj}$ applied to $\mathrm{hR}$ is an adjunction of the composition of the monoid algebra functor of $R$ and $\operatorname{forget}$ applied to $R$ and the forgetful functor of the set of categories of commutative rings and the set of commutative monoid categories defined as the composition of the monoid algebra adjoint of $R$ and the adjunction of the equivalence of $\mathrm{hR}$.

the free functor (from the docstring)

The free functor is a functor of the set of sets and the set of categories of commutative rings.

the monoid algebra functor of R (from the docstring)

Let $R$ be a category of commutative rings. Then the monoid algebra functor of $R$ is a functor of the set of commutative monoid categories and $\operatorname{Under}$ applied to $R$.

the monoid algebra adjoint of R (from the name)

Let $R$ be a category of commutative rings. Then the monoid algebra adjoint of $R$ is an adjunction of the monoid algebra functor of $R$ and the composition of $\operatorname{forget}$ applied to $R$ and the forgetful functor of the set of categories of commutative rings and the set of commutative monoid categories.

the commutative ring category isomorphism to ring isomorphism of e (from the name)

Let $e$ be an isomorphism of $R$ and $S$. Then the commutative ring category isomorphism to ring isomorphism of $e$ is a ring isomorphism of the set of carriers of $R$ and the set of carriers of $S$.

the commutative semi ring category isomorphism to ring isomorphism of e (from the name)

Let $e$ be an isomorphism of $R$ and $S$. Then the commutative semi ring category isomorphism to ring isomorphism of $e$ is a ring isomorphism of the set of carriers of $R$ and the set of carriers of $S$.

the ring category isomorphism to ring isomorphism of e (from the name)

Let $e$ be an isomorphism of $R$ and $S$. Then the ring category isomorphism to ring isomorphism of $e$ is a ring isomorphism of the set of carriers of $R$ and the set of carriers of $S$.

the semi ring category isomorphism to ring isomorphism of e (from the name)

Let $e$ be an isomorphism of $R$ and $S$. Then the semi ring category isomorphism to ring isomorphism of $e$ is a ring isomorphism of the set of carriers of $R$ and the set of carriers of $S$.

category of commutative rings (from the docstring)

The categories of commutative rings are a basic type.

homomorphism of R and S (from the name)

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

the underlying ring hom of f (from the docstring)

Let $f$ be a homomorphism of $R$ and $S$. Then the underlying ring hom of $f$ is a ring homomorphism of the set of carriers of $R$ and the set of carriers of $S$ defined as the homomorphism of $f$.

the underlying ring hom of self (from the docstring)

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

carrier of self (from the name)

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

Let $R$ and $\mathrm{R'}$ be categories of commutative rings. Then $\mathrm{CommRingCat\_\_forget\_obj\_eq\_coe}$ holds for $R$ and $\mathrm{R'}$, if if $\EqtMACRoH {R}{\mathrm{R'}}$, then the action of the forgetful functor of the set of categories of commutative rings and $R$ is equal to the set of carriers of $\mathrm{R'}$.

$\mathrm{CommRingCat\_\_fullyFaithfulForget\_u2082\_ToRingCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the commutative ring category of f (from the name)

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

commutative semi ring category (from the name)

The commutative semi ring categories are a basic type.

homomorphism of R and S (from the name)

Let $R$ and $S$ be commutative semi ring categories. Then the homomorphisms of $R$ and $S$ are a basic type.

the homomorphism of f (from the name)

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

the underlying ring hom of self (from the docstring)

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

carrier of self (from the name)

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

Let $R$ and $\mathrm{R'}$ be commutative semi ring categories. Then $\mathrm{CommSemiRingCat\_\_forget\_obj\_eq\_coe}$ holds for $R$ and $\mathrm{R'}$, if if $\EqtMACRoH {R}{\mathrm{R'}}$, then the action of the forgetful functor of the set of commutative semi ring categories and $R$ is equal to the set of carriers of $\mathrm{R'}$.

$\mathrm{CommSemiRingCat\_\_fullyFaithfulForget\_u2082\_ToSemiRingCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of commutative semi ring categories and the set of semi ring categories.

the commutative semi ring category of f (from the name)

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

category of rings (from the docstring)

The categories of rings are a basic type.

homomorphism of R and S (from the name)

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

the homomorphism of f (from the name)

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

the underlying ring hom of self (from the docstring)

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

carrier of self (from the name)

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

Let $R$ and $\mathrm{R'}$ be categories of rings. Then $\mathrm{RingCat\_\_forget\_obj\_eq\_coe}$ holds for $R$ and $\mathrm{R'}$, if if $\EqtMACRoH {R}{\mathrm{R'}}$, then the action of the forgetful functor of the set of categories of rings and $R$ is equal to the set of carriers of $\mathrm{R'}$.

$\mathrm{RingCat\_\_fullyFaithfulForget\_u2082\_ToSemiRingCat}$ is an element of $\operatorname{FullyFaithful}$ applied to the forgetful functor of the set of categories of rings and the set of semi ring categories.

the ring category of f (from the name)

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

the commutative ring category isomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the commutative ring category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $\operatorname{of}$ applied to $S$.

the commutative semi ring category isomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the commutative semi ring category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $\operatorname{of}$ applied to $S$.

the ring category isomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the ring category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $\operatorname{of}$ applied to $S$.

the semi ring category isomorphism of e (from the name)

Let $e$ be a ring isomorphism of $R$ and $S$. Then the semi ring category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $R$ and $\operatorname{of}$ applied to $S$.

semi ring category (from the name)

The semi ring categories are a basic type.

homomorphism of R and S (from the name)

Let $R$ and $S$ be semi ring categories. Then the homomorphisms of $R$ and $S$ are a basic type.

the homomorphism of f (from the name)

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

the underlying ring hom of self (from the docstring)

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

carrier of self (from the name)

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

Let $R$ and $\mathrm{R'}$ be semi ring categories. Then $\mathrm{SemiRingCat\_\_forget\_obj\_eq\_coe}$ holds for $R$ and $\mathrm{R'}$, if if $\EqtMACRoH {R}{\mathrm{R'}}$, then the action of the forgetful functor of the set of semi ring categories and $R$ is equal to the set of carriers of $\mathrm{R'}$.

the semi ring category of f (from the name)

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

underlying type of the colimit in F (from the docstring)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then an underlying type of the colimit in $F$ is an element of the function that maps $F$ to $\mathrm{Quotient}$ applied to $\operatorname{colimitSetoid}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the elements of $\operatorname{Prequotient}$ applied to $F$ are a basic type.

the sum of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then the sum of $x_{1}$ and $x_{2}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

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 $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $j$ of $J$ and carriers $x_{1}$ of the action of $F$ and $j$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $j$ and $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the negation of $x_{2}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{3}$ of $\operatorname{Prequotient}$ applied to $F$ and elements $x_{4}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the sum of $x_{3}$ and $x_{4}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{5}$ of $\operatorname{Prequotient}$ applied to $F$ and elements $x_{6}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the product of $x_{5}$ and $x_{6}$.

the product of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then the product of $x_{1}$ and $x_{2}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

the negation of x1 (from the name)

Let $x_{1}$ be an element of $\operatorname{Prequotient}$ applied to $F$. Then the negation of $x_{1}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

Let $j$ be an element of $J$. Let $x_{1}$ be a carrier of the action of $F$ and $j$. Then $\operatorname{of}$ applied to $j$ and $x_{1}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

the one (from the name)

The one is an element of $\operatorname{Prequotient}$ applied to $F$.

the zero (from the name)

The zero is an element of $\operatorname{Prequotient}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then we can say that $\operatorname{Relation}$ holds for $F$, $x_{1}$ and $x_{2}$.

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

the cocone function of j and x1 (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Let $j$ be an element of $J$. Let $x_{1}$ be a carrier of the action of $F$ and $j$. Then the cocone function of $j$ and $x_{1}$ is an underlying type of the colimit in $F$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $\operatorname{of}$ applied to $j$ and $x_{1}$.

the cocone morphism of F and j (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Let $j$ be an element of $J$. Then the cocone morphism of $F$ and $j$ is a homomorphism of the action of $F$ and $j$ and the colimit of $F$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the colimit of $F$ is a category of commutative rings defined as $\operatorname{of}$ applied to the set of underlying types of the colimit in $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then $\operatorname{colimitIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Let $s$ be a cocone of $F$. Let $x_{1}$ be an underlying type of the colimit in $F$. Then $\operatorname{descFun}$ applied to $F$, $s$ and $x_{1}$ is a carrier of $\operatorname{pt}$ applied to $s$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Let $s$ be a cocone of $F$. Let $x_{1}$ be an element of $\operatorname{Prequotient}$ applied to $F$. Then $\operatorname{descFunLift}$ applied to $F$, $s$ and $x_{1}$ is a carrier of $\operatorname{pt}$ applied to $s$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CommRingCat\_\_Colimits\_\_descFunLift\_\_\_f}$ applied to $F$ and $s$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Let $s$ be a cocone of $F$. Then $\operatorname{descMorphism}$ applied to $F$ and $s$ is a homomorphism of the colimit of $F$ and $\operatorname{pt}$ applied to $s$.

underlying type of the colimit in F (from the docstring)

Let $F$ be a functor of $J$ and the set of categories of rings. Then an underlying type of the colimit in $F$ is an element of the function that maps $F$ to $\mathrm{Quotient}$ applied to $\operatorname{colimitSetoid}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of categories of rings. Then the elements of $\operatorname{Prequotient}$ applied to $F$ are a basic type.

the sum of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then the sum of $x_{1}$ and $x_{2}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

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 $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $j$ of $J$ and carriers $x_{1}$ of the action of $F$ and $j$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $j$ and $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the negation of $x_{2}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{3}$ of $\operatorname{Prequotient}$ applied to $F$ and elements $x_{4}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the sum of $x_{3}$ and $x_{4}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{5}$ of $\operatorname{Prequotient}$ applied to $F$ and elements $x_{6}$ of $\operatorname{Prequotient}$ applied to $F$ to elements of $\mathrm{motive}$ applied to the product of $x_{5}$ and $x_{6}$.

the product of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then the product of $x_{1}$ and $x_{2}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

the negation of x1 (from the name)

Let $x_{1}$ be an element of $\operatorname{Prequotient}$ applied to $F$. Then the negation of $x_{1}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

Let $j$ be an element of $J$. Let $x_{1}$ be a carrier of the action of $F$ and $j$. Then $\operatorname{of}$ applied to $j$ and $x_{1}$ is an element of $\operatorname{Prequotient}$ applied to $F$.

the one (from the name)

The one is an element of $\operatorname{Prequotient}$ applied to $F$.

the zero (from the name)

The zero is an element of $\operatorname{Prequotient}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of categories of rings. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Prequotient}$ applied to $F$. Then we can say that $\operatorname{Relation}$ holds for $F$, $x_{1}$ and $x_{2}$.

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

the cocone function of j and x1 (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Let $j$ be an element of $J$. Let $x_{1}$ be a carrier of the action of $F$ and $j$. Then the cocone function of $j$ and $x_{1}$ is an underlying type of the colimit in $F$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $\operatorname{of}$ applied to $j$ and $x_{1}$.

the cocone morphism of F and j (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Let $j$ be an element of $J$. Then the cocone morphism of $F$ and $j$ is a homomorphism of the action of $F$ and $j$ and the colimit of $F$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Then the colimit of $F$ is a category of rings defined as $\operatorname{of}$ applied to the set of underlying types of the colimit in $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of categories of rings. Then $\operatorname{colimitIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of categories of rings. Let $s$ be a cocone of $F$. Let $x_{1}$ be an underlying type of the colimit in $F$. Then $\operatorname{descFun}$ applied to $F$, $s$ and $x_{1}$ is a carrier of $\operatorname{pt}$ applied to $s$.

Let $F$ be a functor of $J$ and the set of categories of rings. Let $s$ be a cocone of $F$. Let $x_{1}$ be an element of $\operatorname{Prequotient}$ applied to $F$. Then $\operatorname{descFunLift}$ applied to $F$, $s$ and $x_{1}$ is a carrier of $\operatorname{pt}$ applied to $s$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{RingCat\_\_Colimits\_\_descFunLift\_\_\_f}$ applied to $F$ and $s$.

Let $F$ be a functor of $J$ and the set of categories of rings. Let $s$ be a cocone of $F$. Then $\operatorname{descMorphism}$ applied to $F$ and $s$ is a homomorphism of the colimit of $F$ and $\operatorname{pt}$ applied to $s$.

the coproduct cocone of A and B (from the name)

Let $A$ and $B$ be categories of commutative rings. Then the coproduct cocone of $A$ and $B$ is a binary cofan of $A$ and $B$ defined as $\operatorname{mk}$ applied to the commutative ring category of $\operatorname{toRingHom}$ applied to $\operatorname{includeLeft}$ and the commutative ring category of $\operatorname{toRingHom}$ applied to $\operatorname{includeRight}$.

Let $A$ and $B$ be categories of commutative rings. Then $\operatorname{coproductCoconeIsColimit}$ applied to $A$ and $B$ is an element of $\operatorname{IsColimit}$ applied to the coproduct cocone of $A$ and $B$.

the coproduct colimit cocone of A and B (from the name)

Let $A$ and $B$ be categories of commutative rings. Then the coproduct colimit cocone of $A$ and $B$ is a colimit cocone of the pair of $A$ and $B$ defined as $\operatorname{mk}$ applied to the coproduct cocone of $A$ and $B$ and $\operatorname{coproductCoconeIsColimit}$ applied to $A$ and $B$.

the equalizer fork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the equalizer fork of $f$ and $g$ is a fork of $f$ and $g$.

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then $\operatorname{equalizerForkIsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the equalizer fork of $f$ and $g$.

$\operatorname{isInitial}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $\Integer$.

the categorical product of rings of R (from the docstring)

Let $R$ be a function from elements of $x$ to categories of commutative rings. Then the categorical product of rings of $R$ is an element of $\operatorname{Fan}$ applied to $R$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to the set of functions from elements $i$ of $x$ to carriers of $R$ applied to $i$ and the function that maps $i_{1}$ to the commutative ring category of the evaluation ring homomorphism of the function that maps $i_{2}$ to the set of carriers of $R$ applied to $i_{2}$ and $i_{1}$.

the categorical product of rings of R (from the docstring)

Let $R$ be a function from elements of $x$ to categories of commutative rings. Then the categorical product of rings of $R$ is an element of $\operatorname{IsLimit}$ applied to the categorical product of rings of $R$.

the product isomorphism product of R (from the name)

Let $R$ be a function from elements of $x$ to categories of commutative rings. Then the product isomorphism product of $R$ is an isomorphism of the product object of $R$ and $\operatorname{of}$ applied to the set of functions from elements $i$ of $x$ to carriers of $R$ applied to $i$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the categorical product of rings of $R$ and the categorical product of rings of $R$.

Let $A$ and $B$ be categories of commutative rings. Then $\operatorname{prodFan}$ applied to $A$ and $B$ is an element of $\operatorname{BinaryFan}$ applied to $A$ and $B$ defined as $\operatorname{mk}$ applied to the commutative ring category of the first component of the set of carriers of $A$ and the set of carriers of $B$ and the commutative ring category of the second component of the set of carriers of $A$ and the set of carriers of $B$.

Let $A$ and $B$ be categories of commutative rings. Then $\operatorname{prodFanIsLimit}$ applied to $A$ and $B$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{prodFan}$ applied to $A$ and $B$.

the pullback cone of f and g (from the name)

Let $f$ be a homomorphism of $A$ and $C$. Let $g$ be a homomorphism of $B$ and $C$. Then the pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.

Let $f$ be a homomorphism of $A$ and $C$. Let $g$ be a homomorphism of $B$ and $C$. Then $\operatorname{pullbackConeIsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $f$ and $g$.

$\operatorname{punitIsTerminal}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$.

the pushout cocone of A and B (from the name)

Let $R$, $A$ and $B$ be sets. Then the pushout cocone of $A$ and $B$ is a pushout cocone of the commutative ring category of the algebra map of $R$ and $A$ and the commutative ring category of the algebra map of $R$ and $B$.

Let $R$, $A$ and $B$ be sets. Then $\operatorname{pushoutCoconeIsColimit}$ applied to $R$, $A$ and $B$ is an element of $\operatorname{IsColimit}$ applied to the pushout cocone of $A$ and $B$.

$\operatorname{zIsInitial}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{of}$ applied to $\Integer$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{of}$ applied to $\Integer$.

the product equivalence product of R (from the name)

Let $R$ be a function from elements of $x$ to sets. Then the product equivalence product of $R$ is a ring isomorphism of the set of carriers of the product object of the function that maps $i$ to $\operatorname{of}$ applied to $R$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $R$ applied to $i_{1}$ defined as the commutative ring category isomorphism to ring isomorphism of the product isomorphism product of the function that maps $x_{2}$ to $\operatorname{of}$ applied to $R$ applied to $x_{2}$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then $\operatorname{R}$ applied to $F$ is a category of rings defined as the colimit of the composition of $F$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the colimit of $F$ is a category of commutative rings defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{R}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of categories of commutative rings and the set of categories of rings and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

Let $F$ be a functor of $J$ and the set of commutative semi ring categories. Then $\operatorname{R}$ applied to $F$ is a semi ring category defined as the colimit of the composition of $F$ and the forgetful functor of the set of commutative semi ring categories and the set of semi ring categories.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of commutative semi ring categories. Then the colimit of $F$ is a commutative semi ring category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{R}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of commutative semi ring categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of commutative semi ring categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of commutative semi ring categories and the set of semi ring categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative semi ring categories and the set of semi ring categories.

Let $F$ be a functor of $J$ and the set of categories of rings. Then $\operatorname{R}$ applied to $F$ is a semi ring category defined as the colimit of the composition of $F$ and the forgetful functor of the set of categories of rings and the set of semi ring categories.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Then the colimit of $F$ is a category of rings defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{R}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of categories of rings. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\operatorname{isColimitOfReflects}$ applied to the forgetful functor of the set of categories of rings and the set of semi ring categories and $\operatorname{colimitCoconeIsColimit}$ applied to the composition of $F$ and the forgetful functor of the set of categories of rings and the set of semi ring categories.

Let $F$ be a functor of $J$ and the set of semi ring categories. Then $\operatorname{R}$ applied to $F$ is a monoid category defined as the colimit of the composition of $F$ and the forgetful functor of the set of semi ring categories and the set of monoid categories.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of semi ring categories. Then the colimit of $F$ is a semi ring category defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{R}$ applied to $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of semi ring categories. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of semi ring categories. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the chosen cone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of categories of commutative rings. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of commutative semi ring categories. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative semi ring categories and the set of semi ring categories.

the chosen cone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of commutative semi ring categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of commutative semi ring categories and the set of semi ring categories.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of categories of rings. Then the limit cone of $F$ is a cone of $F$ defined as the lift limit of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of categories of rings and the set of semi ring categories.

the chosen cone of F (from the docstring)

Let $F$ be a functor of $J$ and the set of categories of rings. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as the lifted cone of $\operatorname{isLimit}$ applied to the composition of $F$ and the forgetful functor of the set of categories of rings and the set of semi ring categories.

the section subring of F (from the name)

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

the limit cone of F (from the name)

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

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

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

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

the section subsemiring of F (from the name)

Let $F$ be a functor of $J$ and the set of semi ring categories. Then the section subsemiring of $F$ is a subsemiring of the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.

the multivariate polynomial homeomorphism of R and A (from the name)

Let $x$ be a set. Let $R$ and $A$ be categories of commutative rings. Then the multivariate polynomial homeomorphism of $R$ and $A$ is a homeomorphism of the set of homomorphisms of $\operatorname{of}$ applied to the set of multivariate polynomials of $x$ and the set of carriers of $A$ and $R$ and $\mathrm{Prod}$ applied to the set of homomorphisms of $A$ and $R$ and the set of functions from elements of $x$ to carriers of $R$.

the precomposition homeomorphism of f (from the name)

Let $f$ be an isomorphism of $A$ and $B$. Then the precomposition homeomorphism of $f$ is a homeomorphism of the set of homomorphisms of $B$ and $R$ and the set of homomorphisms of $A$ and $R$.

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

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

Let $R$ be a category of commutative rings. Let $A$ be a set. Then $\operatorname{mkUnder}$ applied to $R$ and $A$ is an element of $\operatorname{Under}$ applied to $R$ defined as $\operatorname{mk}$ applied to the commutative ring category of the algebra map of the set of carriers of $R$ and $A$.

the tensor product of R and S (from the name)

Let $R$ and $S$ be categories of commutative rings. Then the tensor product of $R$ and $S$ is a functor of $\operatorname{Under}$ applied to $R$ and $\operatorname{Under}$ applied to $S$.

the tensor product isomorphism pushout of R and S (from the name)

Let $R$ and $S$ be categories of commutative rings. Then the tensor product isomorphism pushout of $R$ and $S$ is an isomorphism of the tensor product of $R$ and $S$ and the pushout of the commutative ring category of the algebra map of the set of carriers of $R$ and the set of carriers of $S$.

the natural isomorphism of S and A (from the docstring)

Let $S$ be a category of commutative rings. Let $A$ be an element of $\operatorname{Under}$ applied to $R$. Then the natural isomorphism of $S$ and $A$ is an isomorphism of $\operatorname{mkUnder}$ applied to $S$ and the set of tensor products of the set of carriers of $S$ and the set of carriers of the right of $A$ and the action of the pushout of the commutative ring category of the algebra map of the set of carriers of $R$ and the set of carriers of $S$ and $A$.

the algebra homomorphism of f (from the name)

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

the equalizer fork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the equalizer fork of $f$ and $g$ is a fork of $f$ and $g$.

the equalizer fork of f and g (from the name)

Let $f$ and $g$ be algebra homomorphisms of $A$ and $B$. Then the equalizer fork of $f$ and $g$ is a fork of $\operatorname{toUnder}$ applied to $f$ and $\operatorname{toUnder}$ applied to $g$.

Let $f$ and $g$ be algebra homomorphisms of $A$ and $B$. Then $\operatorname{equalizerFork'IsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the equalizer fork of $f$ and $g$ defined as $\operatorname{equalizerForkIsLimit}$ applied to $\operatorname{toUnder}$ applied to $f$ and $\operatorname{toUnder}$ applied to $g$.

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then $\operatorname{equalizerForkIsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the equalizer fork of $f$ and $g$ defined as $\operatorname{isLimitOfReflects}$ applied to $\operatorname{forget}$ applied to $R$ and the inverse function of the map of $\operatorname{forget}$ applied to $R$ and $\mathrm{CommRingCat\_\_Under\_\_equalizer\_comp}$ applied to $f$ and $g$ and $\operatorname{equalizerForkIsLimit}$ applied to the right of $f$ and the right of $g$.

the equalizer fork tensor product isomorphism of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the equalizer fork tensor product isomorphism of $f$ and $g$ is an isomorphism of the tensor product equalizer of $f$ and $g$ and the equalizer fork of the map of the identity of the set of carriers of $S$ and the set of carriers of $S$ and the algebra homomorphism of $f$ and the map of the identity of the set of carriers of $S$ and the set of carriers of $S$ and the algebra homomorphism of $g$.

Let $P$ be a function from elements of $x$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{piFan}$ applied to $P$ is an element of $\operatorname{Fan}$ applied to $P$.

Let $P$ be a function from elements of $x$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{piFanIsLimit}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{piFan}$ applied to $P$.

Let $P$ be a function from elements of $x_{1}$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{piFanTensorProductIsLimit}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the tensor product of $R$ and $S$ and $\operatorname{piFan}$ applied to $P$.

the tensor product equalizer of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the tensor product equalizer of $f$ and $g$ is a fork of the map of the tensor product of $R$ and $S$ and $f$ and the map of the tensor product of $R$ and $S$ and $g$.

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then $\operatorname{tensorProdMapEqualizerForkIsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the tensor product of $R$ and $S$ and the equalizer fork of $f$ and $g$.

Let $S$ be a category of commutative rings. Let $P$ be a function from elements of $x_{1}$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{tensorProductFan}$ applied to $S$ and $P$ is an element of $\operatorname{Fan}$ applied to the function that maps $i$ to $\operatorname{mkUnder}$ applied to $S$ and the set of tensor products of the set of carriers of $S$ and the set of carriers of the right of $P$ applied to $i$ defined as $\operatorname{mk}$ applied to $\operatorname{mkUnder}$ applied to $S$ and the set of tensor products of the set of carriers of $S$ and the set of functions from elements $i$ of $x_{1}$ to carriers of the right of $P$ applied to $i$ and the function that maps $i_{1}$ to $\operatorname{toUnder}$ applied to the map of the identity of the set of carriers of $S$ and the set of carriers of $S$ and the evaluation algebra homomorphism of the function that maps $j$ to the set of carriers of the right of $P$ applied to $j$ and $i_{1}$.

Let $S$ be a category of commutative rings. Let $P$ be a function from elements of $x_{1}$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{tensorProductFan'}$ applied to $S$ and $P$ is an element of $\operatorname{Fan}$ applied to the function that maps $i$ to $\operatorname{mkUnder}$ applied to $S$ and the set of tensor products of the set of carriers of $S$ and the set of carriers of the right of $P$ applied to $i$ defined as $\operatorname{mk}$ applied to $\operatorname{mkUnder}$ applied to $S$ and the set of functions from elements $i$ of $x_{1}$ to tensor products of the set of carriers of $S$ and the set of carriers of the right of $P$ applied to $i$ and the function that maps $i_{1}$ to $\operatorname{toUnder}$ applied to the evaluation algebra homomorphism of the function that maps $i_{2}$ to the set of tensor products of the set of carriers of $S$ and the set of carriers of the right of $P$ applied to $i_{2}$ and $i_{1}$.

Let $P$ be a function from elements of $x_{1}$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{tensorProductFanIsLimit}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{tensorProductFan}$ applied to $S$ and $P$ defined as $\operatorname{symm}$ applied to the equivalence isomorphism limit of $\operatorname{tensorProductFanIso}$ applied to $P$ and $\operatorname{piFanIsLimit}$ applied to the function that maps $i_{1}$ to $\operatorname{mkUnder}$ applied to $S$ and the set of tensor products of the set of carriers of $S$ and the set of carriers of the right of $P$ applied to $i_{1}$.

Let $P$ be a function from elements of $x_{1}$ to elements of $\operatorname{Under}$ applied to $R$. Then $\operatorname{tensorProductFanIso}$ applied to $P$ is an isomorphism of $\operatorname{tensorProductFan}$ applied to $S$ and $P$ and $\operatorname{tensorProductFan'}$ applied to $S$ and $P$.

the additive magma category isomorphism of e (from the name)

Let $e$ be an additive equivalence of $X$ and $Y$. Then the additive magma category isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

Let $e$ be an additive equivalence of $X$ and $Y$. Then $\operatorname{toAddSemigrpIso}$ applied to $e$ is an isomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

additive magma category (from the name)

The additive magma categories are a basic type.

homomorphism of A and B (from the name)

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

the homomorphism of f (from the name)

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

the homomorphism of self (from the name)

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

carrier of self (from the name)

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

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an additive magma category defined as $\operatorname{mk}$ applied to $M$.

the additive magma category of f (from the name)

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

The elements of $\mathrm{AddSemigrp}$ are a basic type.

homomorphism of A and B (from the name)

Let $A$ and $B$ be elements of $\mathrm{AddSemigrp}$. Then the homomorphisms of $A$ and $B$ are a basic type.

the homomorphism of f (from the name)

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

the homomorphism of self (from the name)

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

carrier of self (from the name)

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

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an element of $\mathrm{AddSemigrp}$ defined as $\operatorname{mk}$ applied to $M$.

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

the additive magma category isomorphism to additive equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the additive magma category isomorphism to additive equivalence of $i$ is an additive equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

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

the magma category isomorphism to multiplicative equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the magma category isomorphism to multiplicative equivalence of $i$ is a multiplicative equivalence of the set of carriers of $X$ and the set of carriers of $Y$.

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

magma category (from the name)

The magma categories are a basic type.

homomorphism of A and B (from the name)

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

the homomorphism of f (from the name)

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

the homomorphism of self (from the name)

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

carrier of self (from the name)

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

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is a magma category defined as $\operatorname{mk}$ applied to $M$.

the magma category of f (from the name)

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

the magma category isomorphism of e (from the name)

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

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

The elements of $\mathrm{Semigrp}$ are a basic type.

homomorphism of A and B (from the name)

Let $A$ and $B$ be elements of $\mathrm{Semigrp}$. Then the homomorphisms of $A$ and $B$ are a basic type.

the homomorphism of f (from the name)

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

the homomorphism of self (from the name)

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

carrier of self (from the name)

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

Let $M$ be a set. Then $\operatorname{of}$ applied to $M$ is an element of $\mathrm{Semigrp}$ defined as $\operatorname{mk}$ applied to $M$.

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

the additive equivalence isomorphism additive magma isomorphism (from the name)

The additive equivalence isomorphism additive magma isomorphism is an isomorphism of the set of additive equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

$\mathrm{addEquivIsoAddSemigrpIso}$ is an isomorphism of the set of additive equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

the multiplicative equivalence isomorphism magma isomorphism (from the name)

The multiplicative equivalence isomorphism magma isomorphism is an isomorphism of the set of multiplicative equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

$\mathrm{mulEquivIsoSemigrpIso}$ is an isomorphism of the set of multiplicative equivalences of $X$ and $Y$ and the set of isomorphisms of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$.

Let $K$ and $D$ be sets. Then we can say that $\operatorname{IsCentral}$ holds for $K$ and $D$.

p is characteristic (from the name)

Let $R$ be a set. Let $p$ be an element of $\mathrm{outParam}$ applied to $\Natural$. Then we can say that $p$ is characteristic.

x1 is a exponential characteristic (from the name)

Let $R$ be a set. Let $x_{1}$ be a natural number. Then we can say that $x_{1}$ is an exponential characteristic.

the ring characteristic of R (from the name)

Let $R$ be a set. Then the ring characteristic of $R$ is a natural number defined as $\operatorname{choose}$ applied to $\operatorname{existsUnique}$ applied to $R$.

the ring exponential characteristic of R (from the name)

Let $R$ be a set. Then the ring exponential characteristic of $R$ is a natural number defined as the maximum of the ring characteristic of $R$ and $1$.

Let $R$ and $S$ be sets. Let $p$ be a natural number. Then $\operatorname{frobenius}$ applied to $R$, $S$ and $p$ is a linear map of $S$ and $S$.

Let $R$ and $S$ be sets. Let $p$ and $n$ be natural numbers. Then $\operatorname{iterateFrobenius}$ applied to $R$, $S$, $p$ and $n$ is a linear map of $S$ and $S$.

the Frobenius map of R and p (from the docstring)

Let $R$ be a set. Let $p$ be a natural number. Then the Frobenius map of $R$ and $p$ is a ring homomorphism of $R$ and $R$.

Let $R$ be a set. Let $p$ and $n$ be natural numbers. Then $\mathrm{iterateFrobenius}$ applied to $R$, $p$ and $n$ is a ring homomorphism of $R$ and $R$.

p is a mixed characteristic zero (from the name)

Let $R$ be a set. Let $p$ be a natural number. Then we can say that $p$ is a mixed characteristic zero.

R is a characteristic zero (from the name)

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

the lift of f and x10 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{9}$ of $x$ and elements $x_{10}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{9} , x_{10})$ to elements of $T$ applied to $x_{9}$, $x_{10}$ and $h_{4}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to algebra homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{8}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{8}))}{g (i , x_{8})}$. Then the lift of $x_{9}$ and $h_{4}$ is an algebra homomorphism of the set of direct limits of $G$ and $f$ and $P$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{6}$ of $x$ and elements $x_{7}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{6} , x_{7})$ to elements of $T$ applied to $x_{6}$, $x_{7}$ and $h_{4}$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $x_{6}$, $x_{7}$, $h_{4}$, $f$ and $i$ is an algebra homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the lift of f and x9 (from the name)

Let $R$ and $x$ be sets. Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{9}$ of $x$ and elements $x_{10}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{9} , x_{10})$ to elements of $T$ applied to $x_{9}$, $x_{10}$ and $h_{4}$. Let $g$ be a function from elements $i_{1}$ of $x$ to linear maps of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{8}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{8}))}{g (i , x_{8})}$. Then the lift of $x_{9}$ and $x_{10}$ is a linear map of the set of direct limits of $G$ and $f$ and $P$.

Let $R$ and $x$ be sets. Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{6}$ of $x$ and elements $x_{7}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{6} , x_{7})$ to elements of $T$ applied to $x_{6}$, $x_{7}$ and $h_{4}$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $R$, $x$, $G$, $x_{6}$, $x_{7}$, $h_{4}$, $f$ and $i$ is a linear map of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the lift of f and x10 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{9}$ of $x$ and elements $x_{10}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{9} , x_{10})$ to elements of $T$ applied to $x_{9}$, $x_{10}$ and $h_{4}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to non unital algebra homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{8}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{8}))}{g (i , x_{8})}$. Then the lift of $x_{9}$ and $h_{4}$ is a non unital algebra homomorphism of the set of direct limits of $G$ and $f$ and $P$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{6}$ of $x$ and elements $x_{7}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{6} , x_{7})$ to elements of $T$ applied to $x_{6}$, $x_{7}$ and $h_{4}$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $x_{6}$, $x_{7}$, $h_{4}$, $f$ and $i$ is a non unital algebra homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the lift of f and x7 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{6}$ of $x$ and elements $x_{7}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{6} , x_{7})$ to elements of $T$ applied to $x_{6}$, $x_{7}$ and $h_{4}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to non unital ring homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{5}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{5}))}{g (i , x_{5})}$. Then the lift of $x_{6}$ and $h_{4}$ is a non unital ring homomorphism of the set of direct limits of $G$ and $f$ and $P$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{4}$ of $x$ and elements $x_{5}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{4} , x_{5})$ to elements of $T$ applied to $x_{4}$, $x_{5}$ and $h_{4}$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $x_{4}$, $x_{5}$, $h_{4}$, $f$ and $i$ is a non unital ring homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the lift of f and x9 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{8}$ of $x$ and elements $x_{9}$ of $x$ and elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{8} , x_{9})$ to elements of $T$ applied to $x_{8}$, $x_{9}$ and $h_{5}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to non unital star ring homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{7}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{7}))}{g (i , x_{7})}$. Then the lift of $x_{8}$ and $h_{5}$ is a non unital star ring homomorphism of the set of direct limits of $G$ and $f$ and $P$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{5}$ of $x$ and elements $x_{6}$ of $x$ and elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{5} , x_{6})$ to elements of $T$ applied to $x_{5}$, $x_{6}$ and $h_{5}$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $x_{5}$, $x_{6}$, $h_{5}$, $f$ and $i$ is a non unital star ring homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the lift of f and x7 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{6}$ of $x$ and elements $x_{7}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{6} , x_{7})$ to elements of $T$ applied to $x_{6}$, $x_{7}$ and $h_{4}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to ring homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{5}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{5}))}{g (i , x_{5})}$. Then the lift of $x_{6}$ and $h_{4}$ is a ring homomorphism of the set of direct limits of $G$ and $f$ and $P$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $x_{4}$ of $x$ and elements $x_{5}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{4} , x_{5})$ to elements of $T$ applied to $x_{4}$, $x_{5}$ and $h_{4}$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $x_{4}$, $x_{5}$, $h_{4}$, $f$ and $i$ is a ring homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the map additive monoid homomorphism of f (from the name)

Let $f$ be a function from elements $x_{4}$ of $x$ and elements $x_{5}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{4} , x_{5})$ to elements of $T$ applied to $x_{4}$, $x_{5}$ and $h_{4}$. Then the map additive monoid homomorphism of $x_{4}$ is an additive monoid homomorphism of the set of functions from elements $i$ of $x$ to elements of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the map monoid homomorphism of f (from the name)

Let $f$ be a function from elements $x_{4}$ of $x$ and elements $x_{5}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{4} , x_{5})$ to elements of $T$ applied to $x_{4}$, $x_{5}$ and $h_{4}$. Then the map monoid homomorphism of $x_{4}$ is a monoid homomorphism of the set of functions from elements $i$ of $x$ to elements of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the map ring homomorphism of f (from the name)

Let $f$ be a function from elements $x_{4}$ of $x$ and elements $x_{5}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (x_{4} , x_{5})$ to elements of $T$ applied to $x_{4}$, $x_{5}$ and $h_{4}$. Then the map ring homomorphism of $x_{4}$ is a ring homomorphism of the set of functions from elements $i$ of $x$ to elements of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

Let $R$ and $M$ be sets. Let $x_{3}$ be an element of $\SubtypeSet {N_{1}}{\operatorname{FG} (N_{1})}$. Let $x_{4}$ be an element of $\SubtypeSet {N}{\operatorname{FG} (N)}$ such that $x_{3} \leq x_{4}$. Then $\operatorname{fgSystem}$ applied to $R$, $M$, $x_{3}$, $x_{4}$ and $\mathrm{le}$ is a linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {x_{3}}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {x_{4}}{x_{6}})}$ defined as the inclusion of $\mathrm{le}$.

the equivalence of R and M (from the name)

Let $R$ and $M$ be sets. Then the equivalence of $R$ and $M$ is a linear equivalence of the set of direct limits of the function that maps $i$ to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {i}{x_{4}})}$ and $\operatorname{fgSystem}$ applied to $R$ and $M$ and $M$.

direct limit of G and f (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to additive monoid homomorphisms of $G$ applied to $i$ and $G$ applied to $j$. Then a direct limit of $G$ and $i$ is an element of the function that maps $G$, $f$, $j$ and $f$ to the set of direct limits of $G$ and the function that maps $i$, $j$ and $\mathrm{hij}$ to the natural linear map of $i$ applied to $i$, $j$ and $\mathrm{hij}$.

the congruence of e and i1 (from the name)

Let $e$ be a function from elements $i_{1}$ of $x$ to additive equivalences of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, the composition of the additive monoid homomorphism of $e$ applied to $j$ and $f$ applied to $i$, $j$ and $h$ is equal to the composition of $\mathrm{f'}$ applied to $i$, $j$ and $h$ and the additive monoid homomorphism of $e$ applied to $i$. Then the congruence of $i_{1}$ and $e$ is an additive equivalence of the set of direct limits of $G$ and $f$ and the set of direct limits of $\mathrm{G'}$ and $\mathrm{f'}$.

the lift of f and j1 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to additive monoid homomorphisms of $G$ applied to $i_{2}$ and $G$ applied to $j_{1}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to additive monoid homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{5}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{5}))}{g (i , x_{5})}$. Then the lift of $i_{2}$ and $f$ is an additive monoid homomorphism of the set of direct limits of $G$ and $f$ and $P$ defined as the function that maps $i_{1}$, $g$ and $\mathrm{Hg}$ to the additive monoid homomorphism of the lift of the function that maps $i$, $j$ and $\mathrm{hij}$ to the natural linear map of $i_{2}$ applied to $i$, $j$ and $\mathrm{hij}$ and the function that maps $i_{1}$ to the natural linear map of $f$ applied to $i_{1}$.

the map of g and i1 (from the name)

Let $g$ be a function from elements $i_{1}$ of $x$ to additive monoid homomorphisms of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, the composition of $g$ applied to $j$ and $f$ applied to $i$, $j$ and $h$ is equal to the composition of $\mathrm{f'}$ applied to $i$, $j$ and $h$ and $g$ applied to $i$. Then the map of $i_{1}$ and $g$ is an additive monoid homomorphism of the set of direct limits of $G$ and $f$ and the set of direct limits of $\mathrm{G'}$ and $\mathrm{f'}$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ to additive monoid homomorphisms of $G$ applied to $i_{1}$ and $G$ applied to $j$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $i_{1}$, $j$, $f$ and $i$ is an additive monoid homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$ defined as the function that maps $f$ and $i$ to the additive monoid homomorphism of $\operatorname{of}$ applied to $\Natural$, $x$, $G$, the function that maps $i_{1}$, $j$ and $\mathrm{hij}$ to the natural linear map of $i_{1}$ applied to $i_{1}$, $j$ and $\mathrm{hij}$ and $j$.

direct limit of G and f (from the name)

Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Then a direct limit of $G$ and $i$ is an element of the function that maps $G$, $f$, $j$ and $f$ to the set of quotients of the set of direct sums of $x_{1}$ and $G$ and the module congruence relation of $i$.

Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Let $x_{6}$ and $x_{7}$ be direct sums of $x_{1}$ and $G$. Then we can say that $\operatorname{Eqv}$ holds for $i$, $j$, $f$, $x_{6}$ and $x_{7}$.

the congruence of e and i1 (from the name)

Let $e$ be a function from elements $i_{1}$ of $x_{1}$ to linear equivalences of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x_{1}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, the composition of $\operatorname{toLinearMap}$ applied to $e$ applied to $j$ and $f$ applied to $i$, $j$ and $h$ is equal to the composition of $\mathrm{f'}$ applied to $i$, $j$ and $h$ and $\operatorname{toLinearMap}$ applied to $e$ applied to $i$. Then the congruence of $i_{1}$ and $e$ is a linear equivalence of the set of direct limits of $G$ and $f$ and the set of direct limits of $\mathrm{G'}$ and $\mathrm{f'}$.

the lift of f and i2 (from the name)

Let $R$ and $x_{1}$ be sets. Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i_{2}$ of $x_{1}$ and elements $j_{1}$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to linear maps of $G$ applied to $i_{2}$ and $G$ applied to $j_{1}$. Let $g$ be a function from elements $i_{1}$ of $x_{1}$ to linear maps of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x_{1}$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{8}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{8}))}{g (i , x_{8})}$. Then the lift of $i_{2}$ and $j_{1}$ is a linear map of the set of direct limits of $G$ and $f$ and $P$.

the linear equivalence of G and f (from the name)

Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Then the linear equivalence of $G$ and $i$ is a linear equivalence of the set of direct limits of $G$ and $f$ and the set of direct limits of $G$ and $f$.

the map of g and i1 (from the name)

Let $g$ be a function from elements $i_{1}$ of $x_{1}$ to linear maps of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x_{1}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, the composition of $g$ applied to $j$ and $f$ applied to $i$, $j$ and $h$ is equal to the composition of $\mathrm{f'}$ applied to $i$, $j$ and $h$ and $g$ applied to $i$. Then the map of $i_{1}$ and $g$ is a linear map of the set of direct limits of $G$ and $f$ and the set of direct limits of $\mathrm{G'}$ and $\mathrm{f'}$.

the module congruence relation of f (from the name)

Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Then the module congruence relation of $i$ is a module congruence relation of $R$ and the set of direct sums of $x_{1}$ and $G$.

Let $R$ and $x_{1}$ be sets. Let $G$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements $i_{1}$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ to linear maps of $G$ applied to $i_{1}$ and $G$ applied to $j$. Let $i$ be an element of $x_{1}$. Then $\operatorname{of}$ applied to $R$, $x_{1}$, $G$, $i_{1}$, $j$, $f$ and $i$ is a linear map of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

the inverse of f and i (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ and elements of $G$ applied to $i$ to elements of $G$ applied to $j$. Let $p$ be a direct limit of $G$ and $f$. Then the inverse of $i$ and $j$ is a direct limit of $G$ and $f$ defined as the function that maps $f$ and $p$ to $\mathrm{dite}$ applied to $\EqtMACRoH {j}{0}$, the function that maps $H$ to $0$, the function that maps $H_{1}$ to $\operatorname{choose}$ applied to $\mathrm{Field\_\_DirectLimit\_\_exists\_inv}$ applied to $G$, $i$ and $H_{1}$, $f$ and $p$.

direct limit of G and f (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ and elements of $G$ applied to $i$ to elements of $G$ applied to $j$. Then a direct limit of $G$ and $i$ is an element of the function that maps $G$, $f$, $j$ and $f$ to the set of quotients of the set of free commutative rings of $\Sigma$ applied to the function that maps $i$ to $G$ applied to $i$ and the span of $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that there exists an element $i_{1}$ of $x$ such that there exists an element $j$ of $x$ such that there exists an element $H$ of $\mathrm{Leq} (i_{1} , j)$ such that there exists an element $x_{3}$ of $G$ applied to $i_{1}$ such that $\EqtMACRoH {\operatorname{of} (\operatorname{mk} (j , i (i_{1} , j , H , x_{3})))- \operatorname{of} (\operatorname{mk} (i_{1} , x_{3}))}{a}$, there exists an element $i_{3}$ of $x$ such that $\EqtMACRoH {\operatorname{of} (\operatorname{mk} (i_{3} , 1))- 1}{a}$, there exists an element $i_{5}$ of $x$ such that there exists an element $x_{4}$ of $G$ applied to $i_{5}$ such that there exists an element $y$ of $G$ applied to $i_{5}$ such that $\EqtMACRoH {\operatorname{of} (\operatorname{mk} (i_{5} , x_{4} + y))- (\operatorname{of} (\operatorname{mk} (i_{5} , x_{4}))+ \operatorname{of} (\operatorname{mk} (i_{5} , y)))}{a}$ or there exists an element $i_{7}$ of $x$ such that there exists an element $x_{5}$ of $G$ applied to $i_{7}$ such that there exists an element $y_{1}$ of $G$ applied to $i_{7}$ such that $\EqtMACRoH {\operatorname{of} (\operatorname{mk} (i_{7} , x_{5} \times y_{1}))- \operatorname{of} (\operatorname{mk} (i_{7} , x_{5}))\times \operatorname{of} (\operatorname{mk} (i_{7} , y_{1}))}{a}$.

the congruence of e and i1 (from the name)

Let $e$ be a function from elements $i_{1}$ of $x$ to ring isomorphisms of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $h_{2}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, the composition of the ring homomorphism of $e$ applied to $j$ and $f$ applied to $i$, $j$ and $h_{2}$ is equal to the composition of $\mathrm{f'}$ applied to $i$, $j$ and $h_{2}$ and the ring homomorphism of $e$ applied to $i$. Then the congruence of $i_{1}$ and $e$ is a ring isomorphism of the set of direct limits of $G$ and the function that maps $x_{4}$, $x_{5}$ and $h$ to $\operatorname{coe}$ applied to $f$ applied to $x_{4}$, $x_{5}$ and $h$ and the set of direct limits of $\mathrm{G'}$ and the function that maps $x_{6}$, $x_{7}$ and $h_{1}$ to $\operatorname{coe}$ applied to $\mathrm{f'}$ applied to $x_{6}$, $x_{7}$ and $h_{1}$.

the lift of f and j1 (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ and elements of $G$ applied to $i_{2}$ to elements of $G$ applied to $j_{1}$. Let $P$ be a set. Let $g$ be a function from elements $i_{1}$ of $x$ to ring homomorphisms of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{4}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{4}))}{g (i , x_{4})}$. Then the lift of $i_{2}$ and $f$ is a ring homomorphism of the set of direct limits of $G$ and $f$ and $P$.

the map of g and i1 (from the name)

Let $g$ be a function from elements $i_{1}$ of $x$ to ring homomorphisms of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $h_{2}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, the composition of $g$ applied to $j$ and $f$ applied to $i$, $j$ and $h_{2}$ is equal to the composition of $\mathrm{f'}$ applied to $i$, $j$ and $h_{2}$ and $g$ applied to $i$. Then the map of $i_{1}$ and $g$ is a ring homomorphism of the set of direct limits of $G$ and the function that maps $x_{4}$, $x_{5}$ and $h$ to $\operatorname{coe}$ applied to $f$ applied to $x_{4}$, $x_{5}$ and $h$ and the set of direct limits of $\mathrm{G'}$ and the function that maps $x_{6}$, $x_{7}$ and $h_{1}$ to $\operatorname{coe}$ applied to $\mathrm{f'}$ applied to $x_{6}$, $x_{7}$ and $h_{1}$.

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ and elements of $G$ applied to $i_{1}$ to elements of $G$ applied to $j$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $G$, $i_{1}$, $j$, $f$ and $i$ is a ring homomorphism of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

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

Let $G$ be a function from elements of $x$ to sets. Let $\mathrm{f'}$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to ring homomorphisms of $G$ applied to $i$ and $G$ applied to $j$. Then the ring isomorphism of $G$ and $i$ is a ring isomorphism of the set of direct limits of $G$ and the function that maps $x_{3}$, $x_{4}$ and $h_{3}$ to $\operatorname{coe}$ applied to $\mathrm{f'}$ applied to $x_{3}$, $x_{4}$ and $h_{3}$ and the set of direct limits of $G$ and $\mathrm{f'}$.

Let $x$ be a set. Then an element of $\mathrm{ContFract}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {s}{\operatorname{IsContFract} (s)}$.

Let $a$ be an element of $x$. Then $\operatorname{ofInteger}$ applied to $a$ is an element of $\mathrm{ContFract}$ applied to $x$ defined as $\operatorname{ofInteger}$ applied to $a$.

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

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then $\operatorname{IsSimpContFract}$ holds for $g$, if for all natural numbers $n$, for all elements $x_{2}$ of $x$, if $\EqtMACRoH {\mathrm{Stream'\_\_Seq\_\_get?} (\operatorname{partNums} (g), n)}{\operatorname{some} (x_{2})}$, then $\EqtMACRoH {x_{2}}{1}$.

pair of x (from the name)

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

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

Let $\mathrm{self}$ be a pair of $x$. Then $\operatorname{b}$ applied to $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the coercion function of x3 (from the name)

Let $x_{3}$ be a pair of $x$. Then the coercion function of $x_{3}$ is a pair of $x_{1}$ defined as the map of $\operatorname{coe}$ and $x_{3}$.

the map of f and gp (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{gp}$ be a pair of $x$. Then the map of $f$ and $\mathrm{gp}$ is a pair of $x_{1}$ defined as $\operatorname{mk}$ applied to $f$ applied to $\operatorname{a}$ applied to $\mathrm{gp}$ and $f$ applied to $\operatorname{b}$ applied to $\mathrm{gp}$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $x$. Let $n$ be a natural number. Then $\operatorname{TerminatedAt}$ holds for $g$ and $n$, if $\operatorname{TerminatedAt}$ holds for $\operatorname{s}$ applied to $g$ and $n$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then $\operatorname{Terminates}$ holds for $g$, if $\operatorname{Terminates}$ holds for $\operatorname{s}$ applied to $g$.

the coercion function of x3 (from the name)

Let $x_{3}$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then the coercion function of $x_{3}$ is an element of $\mathrm{GenContFract}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $\operatorname{h}$ applied to $x_{3}$ and the map of $\operatorname{coeFn}$ and $\operatorname{s}$ applied to $x_{3}$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Then $\mathrm{Stream'}$ holds for the set of pairs of $K$. Proof. Let $g$ be arbitrary. By g. By GenContFract__contsAux. By Stream'__tail.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Then $\mathrm{Stream'}$ holds for $K$. Proof. Let $g$ be arbitrary. Let $n$ be arbitrary. By g. By n. By GenContFract__nums. By g. By n. By GenContFract__dens. By div.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Let $n$ be a natural number. Then $\operatorname{convs'}$ applied to $g$ and $n$ is an element of $K$ defined as $\operatorname{h} (g)+ \operatorname{convs'Aux} (\operatorname{s} (g), n)$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Then $\mathrm{Stream'}$ holds for $K$. Proof. Let $g$ be arbitrary. By GenContFract__Pair__b. By g. By GenContFract__conts. By Stream'__map.

Let $\mathrm{self}$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then $\operatorname{h}$ applied to $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the default (from the name)

The default is a pair of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{default}$ and $\operatorname{default}$.

Let $a$ and $b$ be elements of $K$. Let $\mathrm{ppred}$ and $\mathrm{pred}$ be pairs of $K$. Then $\operatorname{nextConts}$ applied to $a$, $b$, $\mathrm{ppred}$ and $\mathrm{pred}$ is a pair of $K$ defined as $\operatorname{mk}$ applied to the next numerator of $\operatorname{a}$ applied to $\mathrm{ppred}$ and $\operatorname{a}$ applied to $\mathrm{pred}$ and the next denominator of $\operatorname{b}$ applied to $\mathrm{ppred}$ and $\operatorname{b}$ applied to $\mathrm{pred}$.

the next denominator of ppredB and predB (from the name)

Let $x_{1}$, $x_{2}$, $\mathrm{ppredB}$ and $\mathrm{predB}$ be elements of $K$. Then the next denominator of $\mathrm{ppredB}$ and $\mathrm{predB}$ is an element of $K$ defined as $x_{2} \times \mathrm{predB} + x_{1} \times \mathrm{ppredB}$.

the next numerator of ppredA and predA (from the name)

Let $a$, $b$, $\mathrm{ppredA}$ and $\mathrm{predA}$ be elements of $K$. Then the next numerator of $\mathrm{ppredA}$ and $\mathrm{predA}$ is an element of $K$ defined as $b \times \mathrm{predA} + a \times \mathrm{ppredA}$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Then $\mathrm{Stream'}$ holds for $K$. Proof. Let $g$ be arbitrary. By GenContFract__Pair__a. By g. By GenContFract__conts. By Stream'__map.

Let $a$ be an element of $x$. Then $\operatorname{ofInteger}$ applied to $a$ is an element of $\mathrm{GenContFract}$ applied to $x$ defined as $\operatorname{mk}$ applied to $a$ and $\operatorname{nil}$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then $\operatorname{partDens}$ applied to $g$ is a sequence of $x$ defined as the map of $\operatorname{b}$ and $\operatorname{s}$ applied to $g$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then $\operatorname{partNums}$ applied to $g$ is a sequence of $x$ defined as the map of $\operatorname{a}$ and $\operatorname{s}$ applied to $g$.

Let $\mathrm{self}$ be an element of $\mathrm{GenContFract}$ applied to $x$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a sequence of the set of pairs of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $x$ be a set. Then an element of $\mathrm{SimpContFract}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {g}{\operatorname{IsSimpContFract} (g)}$.

Let $s$ be an element of $\mathrm{SimpContFract}$ applied to $x$. Then $\operatorname{IsContFract}$ holds for $s$, if for all natural numbers $n$, for all elements $x_{4}$ of $x$, if $\EqtMACRoH {\mathrm{Stream'\_\_Seq\_\_get?} (\operatorname{partDens} (s), n)}{\operatorname{some} (x_{4})}$, then $0 < x_{4}$.

Let $a$ be an element of $x$. Then $\operatorname{ofInteger}$ applied to $a$ is an element of $\mathrm{SimpContFract}$ applied to $x$ defined as $\operatorname{ofInteger}$ applied to $a$.

Let $v$ be an element of $K$. Then $\operatorname{of}$ applied to $v$ is an element of $\mathrm{ContFract}$ applied to $K$ defined as $\operatorname{of}$ applied to $v$.

Let $v$ be an element of $K$. Then $\operatorname{of}$ applied to $v$ is an element of $\mathrm{SimpContFract}$ applied to $K$ defined as $\operatorname{of}$ applied to $v$.

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

Let $\mathrm{self}$ be an element of $\operatorname{IntFractPair}$ applied to $K$. Then $\operatorname{b}$ applied to $\mathrm{self}$ is an integer defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the coercion function of x2 (from the name)

Let $x_{2}$ be an element of $\operatorname{IntFractPair}$ applied to $K$. Then the coercion function of $x_{2}$ is an element of $\operatorname{IntFractPair}$ applied to $x$ defined as $\operatorname{mapFr}$ applied to $\operatorname{coe}$ and $x_{2}$.

Let $\mathrm{self}$ be an element of $\operatorname{IntFractPair}$ applied to $K$. Then $\operatorname{fr}$ applied to $\mathrm{self}$ is an element of $K$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $f$ be a function from elements of $K$ to elements of $x$. Let $\mathrm{gp}$ be an element of $\operatorname{IntFractPair}$ applied to $K$. Then $\operatorname{mapFr}$ applied to $f$ and $\mathrm{gp}$ is an element of $\operatorname{IntFractPair}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{b}$ applied to $\mathrm{gp}$ and $f$ applied to $\operatorname{fr}$ applied to $\mathrm{gp}$.

Let $v$ be an element of $K$. Then $\operatorname{of}$ applied to $v$ is an element of $\operatorname{IntFractPair}$ applied to $K$ defined as $\operatorname{mk}$ applied to the floor of $v$ and $\operatorname{fract}$ applied to $v$.

the sequence of v (from the name)

Let $v$ be an element of $K$. Then the sequence of $v$ is a sequence of $\operatorname{IntFractPair}$ applied to $K$ defined as $\ProdmkMACRoU {\operatorname{of} (v)}{\operatorname{tail} (\operatorname{stream} (v))}$.

Let $v$ be an element of $K$. Then $\mathrm{Stream'}$ holds for $\mathrm{Option}$ applied to $\operatorname{IntFractPair}$ applied to $K$. Proof. Let $v$ be arbitrary. Let $x_{3}$ be arbitrary. By x3. By v. By GenContFract__IntFractPair__stream___f. By Nat__brecOn.

Let $v$ be an element of $K$. Then $\operatorname{of}$ applied to $v$ is an element of $\mathrm{GenContFract}$ applied to $K$.

the composition exact value of conts and fr (from the name)

Let $\mathrm{pconts}$ and $\mathrm{conts}$ be pairs of $K$. Let $\mathrm{fr}$ be an element of $K$. Then the composition exact value of $\mathrm{conts}$ and $\mathrm{fr}$ is an element of $K$ defined as $\iteMACRoG {(\EqtMACRoH {\mathrm{fr}}{0})}{(\frac{ \operatorname{a} (\mathrm{conts})}{\operatorname{b} (\mathrm{conts})})}{(\frac{ \operatorname{a} (\operatorname{nextConts} (1 , \operatorname{inv} (\mathrm{fr}), \mathrm{pconts} , \mathrm{conts}))}{\operatorname{b} (\operatorname{nextConts} (1 , \operatorname{inv} (\mathrm{fr}), \mathrm{pconts} , \mathrm{conts}))})}$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Let $x_{1}$ be a natural number. Then $\operatorname{squashGCF}$ applied to $g$ and $x_{1}$ is an element of $\mathrm{GenContFract}$ applied to $K$.

Let $s$ be a sequence of the set of pairs of $K$. Let $n$ be a natural number. Then $\operatorname{squashSeq}$ applied to $s$ and $n$ is a sequence of the set of pairs of $K$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Then $\operatorname{IsEuler}$ holds for $g$, if for all natural numbers $n$, for all elements $x_{1}$ and $x_{2}$ of $K$, if $\EqtMACRoH {\mathrm{Stream'\_\_Seq\_\_get?} (\operatorname{s} (g), n)}{\operatorname{some} (\operatorname{mk} (x_{1} , x_{2}))}$, then $\iteMACRoG {\mathrm{Eq} (n , 0)}{\EqtMACRoH {x_{2}}{1}}{\EqtMACRoH {(x_{1} + x_{2})}{1}}$.

Let $h$ be an element of $K$. Let $x_{1}$ be a sequence of $K$. Then $\operatorname{euler}$ applied to $h$ and $x_{1}$ is an element of $\mathrm{GenContFract}$ applied to $K$.

Let $g$ be an element of $\mathrm{GenContFract}$ applied to $K$. Then $\operatorname{toEuler}$ applied to $g$ is an element of $\mathrm{GenContFract}$ applied to $K$.

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

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

Let $\mathrm{self}$ be an element of $\mathrm{Cubic}$ applied to $R$. Then $\operatorname{b}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\mathrm{Cubic}$ applied to $R$. Then $\operatorname{c}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\mathrm{Cubic}$ applied to $R$. Then $\operatorname{d}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the discriminant of P (from the docstring)

Let $P$ be an element of $\mathrm{Cubic}$ applied to $R$. Then the discriminant of $P$ is an element of $R$ defined as $\operatorname{b} (P)^ {2}\times \operatorname{c} (P)^ {2}- 4 \times \operatorname{a} (P)\times \operatorname{c} (P)^ {3}- 4 \times \operatorname{b} (P)^ {3}\times \operatorname{d} (P)- 27 \times \operatorname{a} (P)^ {2}\times \operatorname{d} (P)^ {2}+ 18 \times \operatorname{a} (P)\times \operatorname{b} (P)\times \operatorname{c} (P)\times \operatorname{d} (P)$.

the equivalence (from the name)

The equivalence is an element of $\EquivMACRoAE {\mathrm{Cubic} (R)}{(\SubtypeSet {p}{\mathrm{Leq} (\operatorname{degree} (p), 3)})}$.

the map of x2 and P (from the name)

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $P$ be an element of $\mathrm{Cubic}$ applied to $R$. Then the map of $x_{2}$ and $P$ is an element of $\mathrm{Cubic}$ applied to $S$ defined as $\operatorname{mk}$ applied to $x_{2}$ applied to $\operatorname{a}$ applied to $P$, $x_{2}$ applied to $\operatorname{b}$ applied to $P$, $x_{2}$ applied to $\operatorname{c}$ applied to $P$ and $x_{2}$ applied to $\operatorname{d}$ applied to $P$.

the root of P (from the name)

Let $P$ be an element of $\mathrm{Cubic}$ applied to $R$. Then the root of $P$ is a multiset of $R$ defined as the root of the polynomial of $P$.

the polynomial of P (from the name)

Let $P$ be an element of $\mathrm{Cubic}$ applied to $R$. Then the polynomial of $P$ is a polynomial of $R$ defined as $\operatorname{C} (\operatorname{a} (P))\times \operatorname{X} ^ {3}+ \operatorname{C} (\operatorname{b} (P))\times \operatorname{X} ^ {2}+ \operatorname{C} (\operatorname{c} (P))\times \operatorname{X} + \operatorname{C} (\operatorname{d} (P))$.

the direct sum of x4 (from the name)

Let $x_{4}$ be a function from elements $i_{1}$ of $x$ to additive characteristics of $G$ applied to $i_{1}$ and $R$. Then the direct sum of $i_{1}$ is an additive characteristic of the set of direct sums of $x$ and the function that maps $i$ to $G$ applied to $i$ and $R$ defined as the function that maps $x_{4}$ to $\operatorname{symm}$ applied to the additive monoid homomorphism equivalence, the additive monoid of the function that maps $i_{4}$ to $\operatorname{toAddMonoidHomEquiv}$ applied to $i_{1}$ applied to $i_{4}$ and $x_{4}$.

A is a algebra (from the name)

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

the algebra (from the name)

The algebra is an additive monoid homomorphism of $R$ and $A$ applied to $0$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

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

Let $R$ be a set. Let $A$ be a function from elements of $x$ to sets. Then the multiplicative homomorphism of $R$ and $A$ is a linear map of $A$ applied to $i$ and the set of linear maps of $A$ applied to $j$ and $A$ applied to $i + j$.

the algebra of A and f (from the name)

Let $R$ be a set. Let $A$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{2}$ of $x$ to linear maps of $A$ applied to $i_{2}$ and $B$ such that $f$ applied to $0$ and the one is equal to $1$ and for all elements $i_{1}$ of $x$, for all elements $j$ of $x$, for all elements $\mathrm{ai}$ of $A$ applied to $i_{1}$, for all elements $\mathrm{aj}$ of $A$ applied to $j$, $f$ applied to $i_{1} + j$ and the product of $\mathrm{ai}$ and $\mathrm{aj}$ is equal to $f (i_{1} , \mathrm{ai})\times f (j , \mathrm{aj})$. Then the algebra of $A$ and $i_{2}$ is an algebra homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $A$ applied to $i$ and $B$.

direct sum of x and x1 (from the name)

Let $x$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Then a direct sum of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$.

A is internal (from the name)

Let $A$ be a function from elements of $x$ to elements of $S$. Then $A$ is internal, if $\operatorname{coe}$ applied to the coercion additive monoid homomorphism of $A$ is bijective.

the additive equivalence product of G (from the name)

Let $G$ be a function from elements of $x$ to sets. Then the additive equivalence product of $G$ is an additive equivalence of the set of direct sums of $x$ and $G$ and the set of functions from elements $i$ of $x$ to elements of $G$ applied to $i$.

the additive equivalence product direct sum (from the name)

The additive equivalence product direct sum is an additive equivalence of the set of direct sums of $\mathrm{Option}$ applied to $x$ and the function that maps $i$ to $x_{1}$ applied to $i$ and $\mathrm{Prod}$ applied to $x_{1}$ applied to $\operatorname{none}$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $x_{1}$ applied to $\operatorname{some}$ applied to $i_{1}$.

the coercion additive monoid homomorphism of A (from the name)

Let $A$ be a function from elements of $x$ to elements of $S$. Then the coercion additive monoid homomorphism of $A$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A (i)}{x_{4}})}$ and $M$ defined as the additive monoid of the function that maps $i$ to the subtype of $A$ applied to $i$.

the coercion function additive monoid homomorphism of x1 (from the name)

Let $x_{1}$ be a function from elements of $x$ to sets. Then the coercion function additive monoid homomorphism of $x_{1}$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$.

the left equivalence congruence of h (from the name)

Let $h$ be an equivalence from $x$ to $x_{3}$. Then the left equivalence congruence of $h$ is an additive equivalence of the set of direct sums of $x$ and the function that maps $i$ to $x_{1}$ applied to $i$ and the set of direct sums of $x_{3}$ and the function that maps $k$ to $x_{1}$ applied to $\operatorname{symm}$ applied to $h$ and $k$.

$\operatorname{fromAddMonoid}$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to the set of additive monoid homomorphisms of $x_{4}$ and $x_{1}$ applied to $i$ and the set of additive monoid homomorphisms of $x_{4}$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ defined as the additive monoid of the function that maps $i$ to $\operatorname{compHom}$ applied to $\operatorname{of}$ applied to $x_{1}$ and $i$.

the identity of M and x (from the name)

Let $M$ be a set. Let $x$ be an element of $\mathrm{optParam}$ applied to the set of sets and $\mathrm{PUnit}$. Then the identity of $M$ and $x$ is an additive equivalence of the set of direct sums of $x$ and the function that maps $x_{3}$ to $M$ and $M$.

the map of f (from the name)

Let $f$ be a function from elements $i_{2}$ of $x$ to additive monoid homomorphisms of $x_{1}$ applied to $i_{2}$ and $x_{2}$ applied to $i_{2}$. Then the map of $i_{2}$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $x_{1}$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$ defined as the function that maps $f$ to the additive monoid homomorphism of $i_{2}$.

Let $x_{1}$ be a function from elements of $x$ to sets. Let $s$ be a finite set of $x$. Then $\operatorname{mk}$ applied to $x_{1}$ and $s$ is an additive monoid homomorphism of the set of functions from elements $i$ of $s$ to elements of $x_{1}$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$.

Let $x_{1}$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ and $i$ is an additive monoid homomorphism of $x_{1}$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ defined as the single additive homomorphism of $x_{1}$ and $i$.

the set to set of S and T (from the name)

Let $x_{1}$ be a function from elements of $x$ to sets. Let $S$ and $T$ be elements of $\wp x$ such that $S \leq T$. Then the set to set of $S$ and $T$ is an additive monoid homomorphism of the set of direct sums of the set of elements of $S$ and the function that maps $i$ to $x_{1}$ applied to $i$ and the set of direct sums of the set of elements of $T$ and the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ defined as the additive monoid of the function that maps $i$ to $\operatorname{of}$ applied to the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ and $i$.

the sigma curry (from the name)

The sigma curry is an additive monoid homomorphism of the set of direct sums of $\Sigma$ applied to the function that maps $\mathrm{\_i}$ to $x_{2}$ applied to $\mathrm{\_i}$ and the function that maps $i$ to $x_{3}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to the set of direct sums of $x_{2}$ applied to $i_{1}$ and the function that maps $j$ to $x_{3}$ applied to $i_{1}$ and $j$.

the sigma curry equivalence (from the name)

The sigma curry equivalence is an additive equivalence of the set of direct sums of $\Sigma$ applied to the function that maps $\mathrm{\_i}$ to $x_{2}$ applied to $\mathrm{\_i}$ and the function that maps $i$ to $x_{3}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to the set of direct sums of $x_{2}$ applied to $i_{1}$ and the function that maps $j$ to $x_{3}$ applied to $i_{1}$ and $j$.

the equivalence between a direct sum indexed by a type of f (from the docstring)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the equivalence between a direct sum indexed by a type of $f$ is an additive equivalence of the set of direct sums of $x$ and the function that maps $i$ to $x_{3}$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $j$ to the set of direct sums of $\SubtypeSet {i_{1}}{(\EqtMACRoH {f (i_{1})}{j})}$ and the function that maps $i_{2}$ to $x_{3}$ applied to $i_{2}$ defined as the composition of the left equivalence congruence of the inverse of the sigma fiber equivalence of $f$ and the sigma curry equivalence.

$\operatorname{sigmaUncurry}$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to the set of direct sums of $x_{2}$ applied to $i$ and the function that maps $j$ to $x_{3}$ applied to $i$ and $j$ and the set of direct sums of $\Sigma$ applied to the function that maps $\mathrm{\_i}$ to $x_{2}$ applied to $\mathrm{\_i}$ and the function that maps $i_{1}$ to $x_{3}$ applied to $\operatorname{fst}$ applied to $i_{1}$ and $\operatorname{snd}$ applied to $i_{1}$.

the additive monoid of x6 (from the name)

Let $x_{6}$ be a function from elements $i_{1}$ of $x$ to additive monoid homomorphisms of $x_{1}$ applied to $i_{1}$ and $x_{4}$. Then the additive monoid of $i_{1}$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $x_{1}$ applied to $i$ and $x_{4}$ defined as the function that maps $x_{6}$ to $\operatorname{liftAddHom}$ applied to $i_{1}$ and $x_{6}$.

x5 is a decomposition (from the name)

Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $x_{5}$ is a decomposition.

Let $x_{6}$ be an element of $M$. Then $\operatorname{decompose'}$ applied to $x_{6}$ is a direct sum of $x$ and the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{5} (i)}{x_{7}})}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{6}$.

Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be an element of $P$. Then $\operatorname{IsHomogeneous}$ holds for $x_{5}$ and $p$, if for all elements $i$ of $x$, for all elements $m$ of $M$, if $m$ is an element of $p$, then $\MembershipmemMACRoT {p}{\operatorname{coe} (\operatorname{decompose} (x_{5}), m , i)}$.

Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{decompose}$ applied to $x_{5}$ is an equivalence from $M$ to the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{5} (i)}{x_{7}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{decompose'}$, $\operatorname{coe}$ applied to the coercion additive monoid homomorphism of $x_{5}$, $\mathrm{DirectSum\_\_Decomposition\_\_left\_inv}$ and $\mathrm{DirectSum\_\_Decomposition\_\_right\_inv}$.

Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{decomposeAddEquiv}$ applied to $x_{5}$ is an additive equivalence of $M$ and the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{5} (i)}{x_{7}})}$.

Let $x_{5}$ be a function from elements of $x$ to submodules of $R$ and $M$. Then $\operatorname{decomposeLinearEquiv}$ applied to $x_{5}$ is a linear equivalence of $M$ and the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{5} (i)}{x_{7}})}$.

the finitely supported function equivalence direct sum of M and x3 (from the name)

Let $R$, $M$ and $x_{3}$ be sets. Then the finitely supported function equivalence direct sum of $M$ and $x_{3}$ is a linear equivalence of $\FinsuppMACRoQ {x_{3}}{M}$ and the set of direct sums of $x_{3}$ and the function that maps $x_{5}$ to $M$ defined as the finitely supported function linear equivalence finitely supported function of $R$.

Let $V$ be a function from elements of $I$ to ideals of $R$. Let $i$ be an element of $I$. Then $\operatorname{idempotent}$ applied to $V$ and $i$ is an element of $R$ defined as $\operatorname{coe}$ applied to $\operatorname{decompose}$ applied to $V$, $1$ and $i$.

the coercion algebra homomorphism of A (from the name)

Let $A$ be a function from elements of $x$ to submodules of $S$ and $R$. Then the coercion algebra homomorphism of $A$ is an algebra homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {A (i)}{x_{6}})}$ and $R$.

the coercion ring homomorphism of A (from the name)

Let $A$ be a function from elements of $x$ to elements of $x_{1}$. Then the coercion ring homomorphism of $A$ is a ring homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {A (i)}{x_{6}})}$ and $R$.

the subalgebra of A (from the docstring)

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

the subring of A (from the docstring)

Let $A$ be a function from elements of $x$ to elements of $x_{1}$. Then the subring of $A$ is a subring of $R$.

the subsemiring of A (from the docstring)

Let $A$ be a function from elements of $x$ to elements of $x_{1}$. Then the subsemiring of $A$ is a subsemiring of $R$.

Assume that $A$ is internal. Let $v$ be a function from elements $i_{1}$ of $x_{1}$ to bases of $R$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {A (i_{1})}{x_{6}})}$. Then $\operatorname{collectedBasis}$ applied to $h$, $i_{1}$ and $v$ is a basis of $R$ and $M$ defined as the function that maps $v$ to $\operatorname{ofRepr}$ applied to the composition of the composition of the inverse of the linear equivalence of the coercion linear map of $A$ and $h$ and the linear equivalence of the function that maps $i$ to the representation of $i_{1}$ applied to $i$ and the inverse of the sigma finitely supported function linear equivalence finitely supported function of $R$ and $v$.

the coercion function linear map of R (from the name)

Let $R$ be a set. Then the coercion function linear map of $R$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $M$ applied to $i_{1}$ defined as the coercion function linear map of $R$.

the coercion linear map of A (from the name)

Let $A$ be a function from elements of $x_{1}$ to submodules of $R$ and $M$. Then the coercion linear map of $A$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $i$ to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {A (i)}{x_{5}})}$ and $M$ defined as the module of the function that maps $i$ to the subtype of $A$ applied to $i$.

the component of M and i (from the name)

Let $R$ and $x_{1}$ be sets. Let $M$ be a function from elements of $x_{1}$ to sets. Let $i$ be an element of $x_{1}$. Then the component of $M$ and $i$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and $M$ applied to $i$ defined as $\operatorname{lapply}$ applied to $i$.

the congruence additive equivalence of u (from the name)

Let $u$ be a function from elements $i_{2}$ of $x$ to additive equivalences of $N$ applied to $i_{2}$ and $P$ applied to $i_{2}$. Then the congruence additive equivalence of $i_{2}$ is an additive equivalence of the set of direct sums of $x$ and the function that maps $i$ to $N$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $P$ applied to $i_{1}$.

the congruence linear equivalence of u (from the name)

Let $u$ be a function from elements $i_{2}$ of $x_{1}$ to linear equivalences of $N$ applied to $i_{2}$ and $P$ applied to $i_{2}$. Then the congruence linear equivalence of $i_{2}$ is a linear equivalence of the set of direct sums of $x_{1}$ and the function that maps $i$ to $N$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $P$ applied to $i_{1}$.

the left linear equivalence congruence of R and h (from the name)

Let $R$ be a set. Let $h$ be an equivalence from $x_{1}$ to $x_{4}$. Then the left linear equivalence congruence of $R$ and $h$ is a linear equivalence of the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$ and the set of direct sums of $x_{4}$ and the function that maps $k$ to $M$ applied to $\operatorname{symm}$ applied to $h$ and $k$ defined as the domain congruence of $h$.

the linear equivalence product direct sum of R (from the name)

Let $R$ be a set. Then the linear equivalence product direct sum of $R$ is a linear equivalence of the set of direct sums of $\mathrm{Option}$ applied to $x_{1}$ and the function that maps $i$ to $x_{2}$ applied to $i$ and $\mathrm{Prod}$ applied to $x_{2}$ applied to $\operatorname{none}$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $x_{2}$ applied to $\operatorname{some}$ applied to $i_{1}$.

Let $R$ and $M$ be sets. Let $x_{1}$ be an element of $\mathrm{optParam}$ applied to the set of sets and $\mathrm{PUnit}$. Then $\operatorname{lid}$ applied to $R$, $M$ and $x_{1}$ is a linear equivalence of the set of direct sums of $x_{1}$ and the function that maps $x_{5}$ to $M$ and $M$.

the linear equivalence function on finite type of M (from the name)

Let $R$ and $x_{1}$ be sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then the linear equivalence function on finite type of $M$ is a linear equivalence of the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $M$ applied to $i_{1}$ defined as the linear equivalence function on finite type.

Let $f$ be a function from elements $i_{2}$ of $x_{1}$ to linear maps of $M$ applied to $i_{2}$ and $N$ applied to $i_{2}$. Then $\operatorname{lmap}$ applied to $i_{2}$ and $f$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $N$ applied to $i_{1}$ defined as the function that maps $f$ to the linear map of $i_{2}$.

Let $R$ and $x_{1}$ be sets. Let $M$ be a function from elements of $x_{1}$ to sets. Let $s$ be a finite set of $x_{1}$. Then $\operatorname{lmk}$ applied to $R$, $x_{1}$, $M$ and $s$ is a linear map of the set of functions from elements $i$ of $s$ to elements of $M$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as $\operatorname{lmk}$ applied to $s$.

Let $R$ and $x_{1}$ be sets. Let $M$ be a function from elements of $x_{1}$ to sets. Let $i$ be an element of $x_{1}$. Then $\operatorname{lof}$ applied to $R$, $x_{1}$, $M$ and $i$ is a linear map of $M$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as $\operatorname{lsingle}$ applied to $i$.

Let $R$ be a set. Let $S$ and $T$ be elements of $\wp x_{1}$ such that $S \leq T$. Then $\operatorname{lsetToSet}$ applied to $R$, $S$, $T$ and $H$ is a linear map of the set of direct sums of the set of elements of $S$ and the function that maps $i$ to $M$ applied to $i$ and the set of direct sums of the set of elements of $T$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as the module of the function that maps $i_{1}$ to $\operatorname{lof}$ applied to $R$, the set of elements of $T$, the function that maps $i_{2}$ to $M$ applied to $i_{2}$ and $i_{1}$.

Let $R$ be a set. Then $\operatorname{sigmaLcurry}$ applied to $R$ is a linear map of the set of direct sums of $\Sigma$ applied to the function that maps $x_{7}$ to $x_{2}$ applied to $x_{7}$ and the function that maps $i$ to $x_{3}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to the set of direct sums of $x_{2}$ applied to $i_{1}$ and the function that maps $j$ to $x_{3}$ applied to $i_{1}$ and $j$.

Let $R$ be a set. Then $\operatorname{sigmaLcurryEquiv}$ applied to $R$ is a linear equivalence of the set of direct sums of $\Sigma$ applied to the function that maps $x_{7}$ to $x_{2}$ applied to $x_{7}$ and the function that maps $i$ to $x_{3}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to the set of direct sums of $x_{2}$ applied to $i_{1}$ and the function that maps $j$ to $x_{3}$ applied to $i_{1}$ and $j$ defined as the sigma curry equivalence.

Let $R$ be a set. Then $\operatorname{sigmaLuncurry}$ applied to $R$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $i$ to the set of direct sums of $x_{2}$ applied to $i$ and the function that maps $j$ to $x_{3}$ applied to $i$ and $j$ and the set of direct sums of $\Sigma$ applied to the function that maps $x_{7}$ to $x_{2}$ applied to $x_{7}$ and the function that maps $i_{1}$ to $x_{3}$ applied to $\operatorname{fst}$ applied to $i_{1}$ and $\operatorname{snd}$ applied to $i_{1}$.

the module of x7 (from the name)

Let $R$, $x_{1}$ and $N$ be sets. Let $x_{7}$ be a function from elements $i_{1}$ of $x_{1}$ to linear maps of $M$ applied to $i_{1}$ and $N$. Then the module of $i_{1}$ is a linear map of the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$ and $N$ defined as the function that maps $x_{7}$ to $\operatorname{lsum}$ applied to $\Natural$, $i_{1}$ and $x_{7}$.

A is a commutative ring (from the name)

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

A is a commutative semiring (from the name)

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

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

A is a ring (from the name)

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

the integer cast of x3 (from the name)

Let $x_{3}$ be an integer. Then the integer cast of $x_{3}$ is an element of $A$ applied to $0$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{3}$.

A is a semiring (from the name)

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

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

the natural cast of x3 (from the name)

Let $x_{3}$ be a natural number. Then the natural cast of $x_{3}$ is an element of $A$ applied to $0$ defined as $\operatorname{proj8}$ applied to $\mathrm{self}$ and $x_{3}$.

the multiplicative homomorphism of A (from the name)

Let $A$ be a function from elements of $x$ to sets. Then the multiplicative homomorphism of $A$ is an additive monoid homomorphism of $A$ applied to $i$ and the set of additive monoid homomorphisms of $A$ applied to $j$ and $A$ applied to $i + j$.

the lift ring homomorphism (from the name)

The lift ring homomorphism is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{and} (\EqtMACRoH {f (0 , \operatorname{one})}{1}, \mathrm{forall} (x , \lambda i . \mathrm{forall} (x , \lambda j . \mathrm{forall} (A (i), \lambda \mathrm{ai} . \mathrm{forall} (A (j), \lambda \mathrm{aj} . \EqtMACRoH {f (i + j , \operatorname{mul} (\mathrm{ai} , \mathrm{aj}))}{(f (i , \mathrm{ai})\times f (j , \mathrm{aj}))})))))})}{\mathrm{RingHom} (\mathrm{DirectSum} (x , \lambda i_{1} . A (i_{1})), R)}$.

the multiplicative homomorphism of A (from the name)

Let $A$ be a function from elements of $x$ to sets. Then the multiplicative homomorphism of $A$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $A$ applied to $i$ and the set of additive monoid homomorphisms of the set of direct sums of $x$ and the function that maps $i_{1}$ to $A$ applied to $i_{1}$ and the set of direct sums of $x$ and the function that maps $i_{2}$ to $A$ applied to $i_{2}$ defined as the additive monoid of the function that maps $x_{5}$ to the flip of the additive monoid of the function that maps $x_{6}$ to the flip of the composition of $\operatorname{compHom}$ applied to $\operatorname{of}$ applied to $A$ and $x_{5} + x_{6}$ and the multiplicative homomorphism of $A$.

the direct sum of A (from the name)

Let $A$ be a function from elements of $x$ to sets. Then the direct sum of $A$ is a ring homomorphism of $A$ applied to $0$ and the set of direct sums of $x$ and the function that maps $i$ to $A$ applied to $i$.

the semiring of f (from the name)

Let $f$ be a function from elements $i_{2}$ of $x$ to additive monoid homomorphisms of $A$ applied to $i_{2}$ and $R$ such that $f$ applied to $0$ and the one is equal to $1$ and for all elements $i_{1}$ of $x$, for all elements $j$ of $x$, for all elements $\mathrm{ai}$ of $A$ applied to $i_{1}$, for all elements $\mathrm{aj}$ of $A$ applied to $j$, $f$ applied to $i_{1} + j$ and the product of $\mathrm{ai}$ and $\mathrm{aj}$ is equal to $f (i_{1} , \mathrm{ai})\times f (j , \mathrm{aj})$. Then the semiring of $i_{2}$ is a ring homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $A$ applied to $i$ and $R$.

x is a decomposition monoid (by hand)

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

a is primal (by hand)

Let $a$ be an element of $x$. Then $a$ is primal, if for all elements $b$ and $c$ of $x$, if $a$ divides $b \times c$, then there exist elements $x_{2}$ and $x_{3}$ of $x$, such that $x_{2}$ divides $b$, $x_{3}$ divides $c$ and $\EqtMACRoH {a}{x_{2} \times x_{3}}$.

Let $a$ and $b$ be elements of $x$. Then $\mathrm{RightDvd}$ holds for $a$ and $b$, if there exists an element $c$ of $x$, such that $\EqtMACRoH {b}{c \times a}$.

Let $x_{2}$ and $y$ be elements of $x$. Then $\mathrm{IsRelPrime}$ holds for $x_{2}$ and $y$, if for all elements $d$ of $x$, if $d$ divides $x_{2}$, then if $d$ divides $y$, then $d$ is a unit.

dual number of R (from the name)

Let $R$ be a set. Then a dual number of $R$ is an element of the function that maps $R$ to the set of trivial square zero extensions of $R$ and $R$.

$\operatorname{eps}$ is a dual number of $R$ defined as the right injection of $1$.

the lift (from the name)

The lift is an equivalence from $\SubtypeSet {\mathrm{fe}}{\mathrm{and} (\EqtMACRoH {(\ProdsndMACRoAA {\mathrm{fe}}\times \ProdsndMACRoAA {\mathrm{fe}})}{0}, \mathrm{forall} (A , \lambda a . \mathrm{Commute} (\ProdsndMACRoAA {\mathrm{fe}}, \operatorname{fst} (\mathrm{fe} , a))))}$ to the set of algebra homomorphisms of the set of dual numbers of $A$ and $B$.

the dual number equivalence (from the name)

The dual number equivalence is an algebra isomorphism of the set of quaternions of the set of dual numbers of $R$ and the set of dual numbers of the set of quaternions of $R$.