Definitions: Mathlib.Algebra, part 15 of 17

OrderAddMonoidHomstructureMathlib.Algebra.Order.Hom.Monoid, type

Wording

order additive monoid homomorphism of x and x1 (from the name)

English

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

OrderAddMonoidHom.compdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an order additive monoid homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be an order additive monoid homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an order additive monoid homomorphism of $x$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toAddMonoidHom}$ applied to $f$ and the additive monoid homomorphism of $g$ and $\operatorname{monotone'}$ applied to the composition of the order homomorphism of $f$ and the order homomorphism of $g$.

OrderAddMonoidHom.copydefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the copy of f and h (from the name)

English

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

OrderAddMonoidHom.iddefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the identity map of x (from the docstring)

English

Let $x$ be a set. Then the identity map of $x$ is an order additive monoid homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity map of $x$ and $\operatorname{monotone'}$ applied to the identity function.

OrderAddMonoidHom.mk'defMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is monotone and for all elements $a$ of $x$, for all elements $b$ of $x$, $\EqtMACRoH {f (a + b)}{f (a)+ f (b)}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{map\_add}$ is an order additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_add}$ and $\mathrm{hf}$.

OrderAddMonoidHom.toOrderHomdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order homomorphism of f (from the name)

English

Let $f$ be an order additive monoid homomorphism of $x$ and $x_{1}$. Then the order homomorphism of $f$ is an order homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toZeroHom}$ applied to $\operatorname{toAddMonoidHom}$ applied to $f$ and $\operatorname{monotone'}$ applied to $f$.

OrderAddMonoidIsostructureMathlib.Algebra.Order.Hom.Monoid, type

Wording

order additive monoid isomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the order additive monoid isomorphisms of $x$ and $x_{1}$ are a basic type.

OrderAddMonoidIso.mk'defMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

no wording

English

Let $f$ be an equivalence from $x$ to $x_{1}$ such that for all elements $a_{1}$ of $x$, for all elements $b_{1}$ of $x$, $f (a_{1})\leq f (b_{1})$, if and only if $a_{1} \leq b_{1}$ and for all elements $a$ of $x$, for all elements $b$ of $x$, $\EqtMACRoH {f (a + b)}{f (a)+ f (b)}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{map\_add}$ is an order additive monoid isomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_add}$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{hf}$ applied to $x_{6}$ and $x_{7}$.

OrderAddMonoidIso.refldefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the identity map of x (from the docstring)

English

Let $x$ be a set. Then the identity map of $x$ is an order additive monoid isomorphism of $x$ and $x$.

OrderAddMonoidIso.symmdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the inverse of f (from the docstring)

English

Let $f$ be an order additive monoid isomorphism of $x$ and $x_{1}$. Then the inverse of $f$ is an order additive monoid isomorphism of $x_{1}$ and $x$.

OrderAddMonoidIso.toOrderIsodefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order isomorphism of f (from the name)

English

Let $f$ be an order additive monoid isomorphism of $x$ and $x_{1}$. Then the order isomorphism of $f$ is an order isomorphism of $x$ and $x_{1}$.

OrderAddMonoidIso.transdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an order additive monoid isomorphism of $x$ and $x_{1}$. Let $g$ be an order additive monoid isomorphism of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an order additive monoid isomorphism of $x$ and $x_{2}$.

OrderMonoidHomstructureMathlib.Algebra.Order.Hom.Monoid, type

Wording

order monoid homomorphism of x and x1 (from the name)

English

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

OrderMonoidHom.compdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an order monoid homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be an order monoid homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an order monoid homomorphism of $x$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toMonoidHom}$ applied to $f$ and the monoid homomorphism of $g$ and $\operatorname{monotone'}$ applied to the composition of the order homomorphism of $f$ and the order homomorphism of $g$.

OrderMonoidHom.copydefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the copy of f and h (from the name)

English

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

OrderMonoidHom.iddefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the identity map of x (from the docstring)

English

Let $x$ be a set. Then the identity map of $x$ is an order monoid homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity map of $x$ and $\operatorname{monotone'}$ applied to the identity function.

OrderMonoidHom.mk'defMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is monotone and for all elements $a$ of $x$, for all elements $b$ of $x$, $\EqtMACRoH {f (a \times b)}{f (a)\times f (b)}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{map\_mul}$ is an order monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_mul}$ and $\mathrm{hf}$.

OrderMonoidHom.toOrderHomdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order homomorphism of f (from the name)

English

Let $f$ be an order monoid homomorphism of $x$ and $x_{1}$. Then the order homomorphism of $f$ is an order homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $f$ and $\operatorname{monotone'}$ applied to $f$.

OrderMonoidHomClass.toOrderAddMonoidHomdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

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

English

Let $f$ be an element of $F$. Then the order additive monoid homomorphism of $f$ is an order additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the additive monoid homomorphism of $f$ and $\operatorname{monotone}$ applied to $f$.

OrderMonoidHomClass.toOrderMonoidHomdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order monoid homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the order monoid homomorphism of $f$ is an order monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the monoid homomorphism of $f$ and $\operatorname{monotone}$ applied to $f$.

OrderMonoidIsostructureMathlib.Algebra.Order.Hom.Monoid, type

Wording

order monoid isomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the order monoid isomorphisms of $x$ and $x_{1}$ are a basic type.

OrderMonoidIso.mk'defMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

no wording

English

Let $f$ be an equivalence from $x$ to $x_{1}$ such that for all elements $a_{1}$ of $x$, for all elements $b_{1}$ of $x$, $f (a_{1})\leq f (b_{1})$, if and only if $a_{1} \leq b_{1}$ and for all elements $a$ of $x$, for all elements $b$ of $x$, $\EqtMACRoH {f (a \times b)}{f (a)\times f (b)}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{map\_mul}$ is an order monoid isomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_mul}$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{hf}$ applied to $x_{6}$ and $x_{7}$.

OrderMonoidIso.refldefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the identity map of x (from the docstring)

English

Let $x$ be a set. Then the identity map of $x$ is an order monoid isomorphism of $x$ and $x$.

OrderMonoidIso.symmdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the inverse of f (from the docstring)

English

Let $f$ be an order monoid isomorphism of $x$ and $x_{1}$. Then the inverse of $f$ is an order monoid isomorphism of $x_{1}$ and $x$.

OrderMonoidIso.toOrderIsodefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order isomorphism of f (from the name)

English

Let $f$ be an order monoid isomorphism of $x$ and $x_{1}$. Then the order isomorphism of $f$ is an order isomorphism of $x$ and $x_{1}$.

OrderMonoidIso.transdefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an order monoid isomorphism of $x$ and $x_{1}$. Let $g$ be an order monoid isomorphism of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an order monoid isomorphism of $x$ and $x_{2}$.

OrderMonoidIsoClass.toOrderAddMonoidIsodefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order additive monoid isomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the order additive monoid isomorphism of $f$ is an order additive monoid isomorphism of $x$ and $x_{1}$.

OrderMonoidIsoClass.toOrderMonoidIsodefMathlib.Algebra.Order.Hom.Monoid, function or constant

Wording

the order monoid isomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the order monoid isomorphism of $f$ is an order monoid isomorphism of $x$ and $x_{1}$.

Mathlib.Algebra.Order.Hom.MonoidWithZero

OrderMonoidIso.unitsWithZerodefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

the unit with zero (from the name)

English

The unit with zero is an order monoid isomorphism of $\UnitsMACRoAO {\mathrm{WithZero} (x)}$ and $x$.

OrderMonoidIso.withZerodefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

no wording

English

$\operatorname{withZero}$ is an equivalence from the set of order monoid isomorphisms of $G$ and $H$ to the set of order monoid isomorphisms of $\mathrm{WithZero}$ applied to $G$ and $\mathrm{WithZero}$ applied to $H$.

OrderMonoidIso.withZeroUnitsdefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

no wording

English

$\operatorname{withZeroUnits}$ is an order monoid isomorphism of $\mathrm{WithZero}$ applied to $\UnitsMACRoAO {x}$ and $x$.

OrderMonoidWithZeroHomstructureMathlib.Algebra.Order.Hom.MonoidWithZero, type

Wording

order monoid with zero homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the order monoid with zero homomorphisms of $x$ and $x_{1}$ are a basic type.

OrderMonoidWithZeroHom.compdefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an order monoid with zero homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be an order monoid with zero homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an order monoid with zero homomorphism of $x$ and $x_{2}$.

OrderMonoidWithZeroHom.copydefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

the copy of f and h (from the name)

English

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

OrderMonoidWithZeroHom.iddefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

the identity map of x (from the docstring)

English

Let $x$ be a set. Then the identity map of $x$ is an order monoid with zero homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity of $x$ and $\operatorname{monotone'}$ applied to the identity function.

OrderMonoidWithZeroHom.toOrderMonoidHomdefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

the order monoid homomorphism of f (from the name)

English

Let $f$ be an order monoid with zero homomorphism of $x$ and $x_{1}$. Then the order monoid homomorphism of $f$ is an order monoid homomorphism of $x$ and $x_{1}$.

OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHomdefMathlib.Algebra.Order.Hom.MonoidWithZero, function or constant

Wording

the order monoid with zero homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the order monoid with zero homomorphism of $f$ is an order monoid with zero homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the monoid with zero homomorphism of $f$ and $\operatorname{monotone}$ applied to $f$.

Mathlib.Algebra.Order.Hom.Ring

OrderRingHomstructureMathlib.Algebra.Order.Hom.Ring, type

Wording

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

English

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

OrderRingHom.compdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the composition of f and g (from the name)

English

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

OrderRingHom.copydefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the copy of f and h (from the name)

English

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

OrderRingHom.iddefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the identity of x (from the docstring)

English

Let $x$ be a set. Then the identity of $x$ is an order ring homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity ring homomorphism of $x$ and $\operatorname{monotone'}$ applied to the identity function.

OrderRingHom.toOrderAddMonoidHomdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

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

English

Let $f$ be an order ring homomorphism of $x$ and $x_{1}$. Then the order additive monoid homomorphism of $f$ is an order additive monoid homomorphism of $x$ and $x_{1}$.

OrderRingHom.toOrderMonoidWithZeroHomdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the order monoid with zero homomorphism of f (from the name)

English

Let $f$ be an order ring homomorphism of $x$ and $x_{1}$. Then the order monoid with zero homomorphism of $f$ is an order monoid with zero homomorphism of $x$ and $x_{1}$.

OrderRingHomClass.toOrderRingHomdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the order ring homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the order ring homomorphism of $f$ is an order ring homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the ring homomorphism of $f$ and $\operatorname{monotone}$ applied to $f$.

OrderRingIsostructureMathlib.Algebra.Order.Hom.Ring, type

Wording

order ring isomorphism of x and x1 (from the name)

English

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

OrderRingIso.refldefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the identity map of x (from the docstring)

English

Let $x$ be a set. Then the identity map of $x$ is an order ring isomorphism of $x$ and $x$.

OrderRingIso.symmdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the inverse of e (from the docstring)

English

Let $e$ be an order ring isomorphism of $x$ and $x_{1}$. Then the inverse of $e$ is an order ring isomorphism of $x_{1}$ and $x$.

OrderRingIso.toOrderIsodefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the order isomorphism of f (from the name)

English

Let $f$ be an order ring isomorphism of $x$ and $x_{1}$. Then the order isomorphism of $f$ is an order isomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\operatorname{toRingEquiv}$ applied to $f$ and the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{OrderRingIso\_\_map\_le\_map\_iff'}$ applied to $f$.

OrderRingIso.toOrderRingHomdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the order ring homomorphism of f (from the name)

English

Let $f$ be an order ring isomorphism of $x$ and $x_{1}$. Then the order ring homomorphism of $f$ is an order ring homomorphism of $x$ and $x_{1}$.

OrderRingIso.transdefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an order ring isomorphism of $x$ and $x_{1}$. Let $g$ be an order ring isomorphism of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an order ring isomorphism of $x$ and $x_{2}$.

OrderRingIsoClass.toOrderRingIsodefMathlib.Algebra.Order.Hom.Ring, function or constant

Wording

the order ring isomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the order ring isomorphism of $f$ is an order ring isomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the ring isomorphism of $f$ and the function that maps $x_{9}$ and $x_{10}$ to $\mathrm{OrderIsoClass\_\_map\_le\_map\_iff}$ applied to $f$.

Mathlib.Algebra.Order.Hom.RingNorm

MulRingNormClassclassMathlib.Algebra.Order.Hom.RingNorm, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulRingNormClass}$ holds for $F$, $x$ and $x_{1}$.

MulRingSeminormClassclassMathlib.Algebra.Order.Hom.RingNorm, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulRingSeminormClass}$ holds for $F$, $x$ and $x_{1}$.

RingNormClassclassMathlib.Algebra.Order.Hom.RingNorm, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{RingNormClass}$ holds for $F$, $x$ and $x_{1}$.

RingSeminormClassclassMathlib.Algebra.Order.Hom.RingNorm, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{RingSeminormClass}$ holds for $F$, $x$ and $x_{1}$.

Mathlib.Algebra.Order.Hom.Submonoid

Submonoid.topOrderMonoidIsodefMathlib.Algebra.Order.Hom.Submonoid, function or constant

Wording

the top submonoid (from the docstring)

English

The top submonoid is an order monoid isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$ and $x$.

Mathlib.Algebra.Order.Hom.TypeTags

OrderAddMonoidIso.toAdditive_toMultiplicativedefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

the additive version (from the docstring)

English

The additive version is an order additive monoid isomorphism of $\mathrm{Additive}$ applied to the set of multiplicatives of $G$ and $G$ defined as $\operatorname{toAdditiveLeft}$ applied to $\operatorname{toMultiplicative}$ applied to the identity map of $G$.

OrderAddMonoidIso.toMultiplicativedefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

the multiplicative (from the name)

English

The multiplicative is an equivalence from the set of order additive monoid isomorphisms of $G$ and $H$ to the set of order monoid isomorphisms of the set of multiplicatives of $G$ and the set of multiplicatives of $H$.

OrderAddMonoidIso.toMultiplicativeLeftdefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

the left multiplicative (from the name)

English

The left multiplicative is an equivalence from the set of order additive monoid isomorphisms of $G$ and $\mathrm{Additive}$ applied to $H$ to the set of order monoid isomorphisms of the set of multiplicatives of $G$ and $H$.

OrderAddMonoidIso.toMultiplicativeRightdefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

the right multiplicative (from the name)

English

The right multiplicative is an equivalence from the set of order additive monoid isomorphisms of $\mathrm{Additive}$ applied to $G$ and $H$ to the set of order monoid isomorphisms of $G$ and the set of multiplicatives of $H$.

OrderMonoidIso.toAdditivedefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

no wording

English

$\operatorname{toAdditive}$ is an equivalence from the set of order monoid isomorphisms of $G$ and $H$ to the set of order additive monoid isomorphisms of $\mathrm{Additive}$ applied to $G$ and $\mathrm{Additive}$ applied to $H$.

OrderMonoidIso.toAdditiveLeftdefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

no wording

English

$\operatorname{toAdditiveLeft}$ is an equivalence from the set of order monoid isomorphisms of $G$ and the set of multiplicatives of $H$ to the set of order additive monoid isomorphisms of $\mathrm{Additive}$ applied to $G$ and $H$ defined as the inverse of the right multiplicative.

OrderMonoidIso.toAdditiveRightdefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

no wording

English

$\operatorname{toAdditiveRight}$ is an equivalence from the set of order monoid isomorphisms of the set of multiplicatives of $G$ and $H$ to the set of order additive monoid isomorphisms of $G$ and $\mathrm{Additive}$ applied to $H$ defined as the inverse of the left multiplicative.

OrderMonoidIso.toMultiplicative_toAdditivedefMathlib.Algebra.Order.Hom.TypeTags, function or constant

Wording

the multiplicative version (from the docstring)

English

The multiplicative version is an order monoid isomorphism of the set of multiplicatives of $\mathrm{Additive}$ applied to $G$ and $G$ defined as $\operatorname{toMultiplicativeLeft}$ applied to $\operatorname{toAdditive}$ applied to the identity map of $G$.

Mathlib.Algebra.Order.Hom.Units

OrderMonoidIso.unitsCongrdefMathlib.Algebra.Order.Hom.Units, function or constant

Wording

the unit congruence of e (from the name)

English

Let $e$ be an order monoid isomorphism of $x$ and $x_{1}$. Then the unit congruence of $e$ is an order monoid isomorphism of $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$.

Mathlib.Algebra.Order.Interval.Basic

Interval.lengthdefMathlib.Algebra.Order.Interval.Basic, function or constant

Wording

the length of x3 (from the docstring)

English

Let $x_{3}$ be an interval of $x$. Then the length of $x_{3}$ is an element of $x$.

NonemptyInterval.lengthdefMathlib.Algebra.Order.Interval.Basic, function or constant

Wording

the length of s (from the docstring)

English

Let $s$ be a nonempty interval of $x$. Then the length of $s$ is an element of $x$ defined as $\ProdsndMACRoAA {\operatorname{toProd} (s)}- \ProdfstMACRoZ {\operatorname{toProd} (s)}$.

Mathlib.Algebra.Order.Interval.Set.Instances

Set.Icc.coeMonoidWithZeroHomdefMathlib.Algebra.Order.Interval.Set.Instances, function or constant

Wording

the coercion monoid with zero homomorphism (from the name)

English

The coercion monoid with zero homomorphism is a monoid with zero homomorphism of the set of elements of $\SetIccMACRoP {0}{1}$ and $R$.

Set.Ico.coeMulHomdefMathlib.Algebra.Order.Interval.Set.Instances, function or constant

Wording

the coercion multiplicative homomorphism (from the name)

English

The coercion multiplicative homomorphism is a multiplicative homomorphism of the set of elements of $\operatorname{Ico}$ applied to $0$ and $1$ and $R$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {\operatorname{Ico} (0 , 1)}{x_{2}}$ and $\mathrm{Set\_\_Ico\_\_coe\_mul}$.

Set.Ioc.coeMonoidHomdefMathlib.Algebra.Order.Interval.Set.Instances, function or constant

Wording

the coercion monoid homomorphism (from the name)

English

The coercion monoid homomorphism is a monoid homomorphism of the set of elements of $\operatorname{Ioc}$ applied to $0$ and $1$ and $R$.

Set.Ioo.coeMulHomdefMathlib.Algebra.Order.Interval.Set.Instances, function or constant

Wording

the coercion multiplicative homomorphism (from the name)

English

The coercion multiplicative homomorphism is a multiplicative homomorphism of the set of elements of the open interval of $0$ and $1$ and $R$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to the proposition that $x_{2}$ is an element of the open interval of $0$ and $1$ and $\mathrm{Set\_\_Ioo\_\_coe\_mul}$.

Mathlib.Algebra.Order.IsBotOne

IsBotOneClassclassMathlib.Algebra.Order.IsBotOne, predicate

Wording

x is a bottom one class (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a bottom one class.

IsBotZeroClassclassMathlib.Algebra.Order.IsBotOne, predicate

Wording

x is a bottom zero class (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a bottom zero class.

Mathlib.Algebra.Order.Kleene

IdemCommSemiringclassMathlib.Algebra.Order.Kleene, predicate

Wording

no wording

English

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

IdemSemiringclassMathlib.Algebra.Order.Kleene, predicate

Wording

no wording

English

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

KStarclassMathlib.Algebra.Order.Kleene, predicate

Wording

x is a star (from the name)

English

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

KStar.kstardefMathlib.Algebra.Order.Kleene, function or constant

Wording

no wording

English

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

KleeneAlgebraclassMathlib.Algebra.Order.Kleene, predicate

Wording

no wording

English

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

Mathlib.Algebra.Order.Module.Archimedean

FiniteArchimedeanClass.balldefMathlib.Algebra.Order.Module.Archimedean, function or constant

Wording

the ball of K and c (from the name)

English

Let $K$ be a set. Let $c$ be a finite archimedean class of $M$. Then the ball of $K$ and $c$ is a submodule of $K$ and $M$ defined as the submodule of $K$ and $\operatorname{Ioi}$ applied to $c$.

FiniteArchimedeanClass.closedBalldefMathlib.Algebra.Order.Module.Archimedean, function or constant

Wording

the closed ball of K and c (from the name)

English

Let $K$ be a set. Let $c$ be a finite archimedean class of $M$. Then the closed ball of $K$ and $c$ is a submodule of $K$ and $M$ defined as the submodule of $K$ and $\operatorname{Ici}$ applied to $c$.

FiniteArchimedeanClass.submoduledefMathlib.Algebra.Order.Module.Archimedean, function or constant

Wording

the submodule of K and s (from the name)

English

Let $K$ be a set. Let $s$ be a upper set of the set of finite archimedean classes of $M$. Then the submodule of $K$ and $s$ is a submodule of $K$ and $M$.

Mathlib.Algebra.Order.Module.Defs

IsOrderedModuleclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

IsStrictOrderedModuleclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

OrderIso.smulRightdefMathlib.Algebra.Order.Module.Defs, function or constant

Wording

the right scalar multiple of ha (from the name)

English

Assume that $0 < a$. Then the right scalar multiple of $\mathrm{ha}$ is an order isomorphism of $x_{1}$ and $x_{1}$.

PosSMulMonoclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

PosSMulReflectLEclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

PosSMulReflectLTclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

PosSMulStrictMonoclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

SMulPosMonoclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

SMulPosReflectLEclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

SMulPosReflectLTclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

SMulPosStrictMonoclassMathlib.Algebra.Order.Module.Defs, predicate

Wording

no wording

English

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

Mathlib.Algebra.Order.Module.Equiv

ofLexLinearEquivdefMathlib.Algebra.Order.Module.Equiv, function or constant

Wording

the lexicographic linear equivalence of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the lexicographic linear equivalence of $x$ and $x_{1}$ is a linear equivalence of $\mathrm{Lex}$ applied to $x_{1}$ and $x_{1}$.

toLexLinearEquivdefMathlib.Algebra.Order.Module.Equiv, function or constant

Wording

the lexicographic linear equivalence of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the lexicographic linear equivalence of $x$ and $x_{1}$ is a linear equivalence of $x_{1}$ and $\mathrm{Lex}$ applied to $x_{1}$.

Mathlib.Algebra.Order.Module.Field

OrderIso.smulRightDualdefMathlib.Algebra.Order.Module.Field, function or constant

Wording

the scalar multiple right dual of G and ha (from the name)

English

Let $G$ be a set. Assume that $a < 0$. Then the scalar multiple right dual of $G$ and $\mathrm{ha}$ is an order isomorphism of $G$ and the set of order duals of $G$.

Mathlib.Algebra.Order.Module.HahnEmbedding

HahnEmbedding.ArchimedeanStratastructureMathlib.Algebra.Order.Module.HahnEmbedding, type

Wording

no wording

English

Let $K$ and $M$ be sets. Then the elements of $\operatorname{ArchimedeanStrata}$ applied to $K$ and $M$ are a basic type.

HahnEmbedding.ArchimedeanStrata.baseDomaindefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the base domain of u (from the name)

English

Let $u$ be an element of $\operatorname{ArchimedeanStrata}$ applied to $K$ and $M$. Then the base domain of $u$ is a submodule of $K$ and $M$ defined as the supremum of the function that maps $c$ to the stratum of $u$ and $c$.

HahnEmbedding.ArchimedeanStrata.stratumdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the stratum of self and x5 (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{ArchimedeanStrata}$ applied to $K$ and $M$. Let $x_{5}$ be a finite archimedean class of $M$. Then the stratum of $\mathrm{self}$ and $x_{5}$ is a submodule of $K$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.

HahnEmbedding.ArchimedeanStrata.stratum'defMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the stratum of u and c (from the name)

English

Let $u$ be an element of $\operatorname{ArchimedeanStrata}$ applied to $K$ and $M$. Let $c$ be a finite archimedean class of $M$. Then the stratum of $u$ and $c$ is a submodule of $K$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{baseDomain} (u)}{x_{5}})}$ defined as the preimage of the subtype of the base domain of $u$ and the stratum of $u$ and $c$.

HahnEmbedding.IsPartialstructureMathlib.Algebra.Order.Module.HahnEmbedding, predicate

Wording

no wording

English

Let $\mathrm{seed}$ be an element of $\operatorname{Seed}$ applied to $K$, $M$ and $R$. Let $f$ be a linear map of $M$ and $\mathrm{Lex}$ applied to the set of Hahn series of the set of finite archimedean classes of $M$ and $R$. Then we can say that $\operatorname{IsPartial}$ holds for $\mathrm{seed}$ and $f$.

HahnEmbedding.PartialdefMathlib.Algebra.Order.Module.HahnEmbedding, type

Wording

no wording

English

Let $\mathrm{seed}$ be an element of $\operatorname{Seed}$ applied to $K$, $M$ and $R$. Then an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$ is an element of the function that maps $\mathrm{seed}$ to $\SubtypeSet {f}{\operatorname{IsPartial} (\mathrm{seed} , f)}$.

HahnEmbedding.Partial.evaldefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the evaluation of f and x8 (from the name)

English

Let $f$ be an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$. Let $x_{8}$ be an element of $M$. Then the evaluation of $f$ and $x_{8}$ is an element of $\mathrm{Lex}$ applied to the set of Hahn series of the set of finite archimedean classes of $M$ and $R$.

HahnEmbedding.Partial.evalCoeffdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the evaluation coefficient of x8 and c (from the name)

English

Let $f$ be an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$. Let $x_{8}$ be an element of $M$. Let $c$ be a finite archimedean class of $M$. Then the evaluation coefficient of $x_{8}$ and $c$ is an element of $R$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $y$ of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{domain} (f)}{x_{9}})}$, such that $\MembershipmemMACRoT {\operatorname{ball} (K , c)}{y - x_{8}}$, the function that maps $h_{4}$ to the coefficient function of $\operatorname{ofLex}$ applied to the function of $f$ and $\operatorname{choose}$ applied to $h_{4}$ and $c$ and the function that maps $h_{5}$ to $0$.

HahnEmbedding.Partial.extenddefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

no wording

English

Let $f$ be an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$ such that $x_{8}$ is not an element of the domain of $f$. Then $\operatorname{extend}$ applied to $f$ and $\mathrm{hx}$ is an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$ defined as $\operatorname{extendFun}$ applied to $f$ and $\mathrm{hx}$.

HahnEmbedding.Partial.extendFundefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

no wording

English

Let $f$ be an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$ such that $x_{8}$ is not an element of the domain of $f$. Then $\operatorname{extendFun}$ applied to $f$ and $\mathrm{hx}$ is a linear map of $M$ and $\mathrm{Lex}$ applied to the set of Hahn series of the set of finite archimedean classes of $M$ and $R$ defined as the supremum span singleton of $x_{8}$ and the evaluation of $f$ and $x_{8}$.

HahnEmbedding.Partial.sSupdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the supremum of hnonempty and hc (from the name)

English

Assume that $c$ is nonempty. Assume that $\mathrm{DirectedOn}$ holds for the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{Leq} (x_{8} , x_{9})$ and $c$. Then the supremum of $\mathrm{hnonempty}$ and $\mathrm{hc}$ is an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$ defined as the supremum function of $\mathrm{hc}$.

HahnEmbedding.Partial.sSupFundefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the supremum function of hc (from the name)

English

Assume that $\mathrm{DirectedOn}$ holds for the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{Leq} (x_{8} , x_{9})$ and $c$. Then the supremum function of $\mathrm{hc}$ is a linear map of $M$ and $\mathrm{Lex}$ applied to the set of Hahn series of the set of finite archimedean classes of $M$ and $R$.

HahnEmbedding.Partial.toOrderAddMonoidHomdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

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

English

Let $f$ be an element of $\operatorname{Partial}$ applied to $\mathrm{seed}$. Then the order additive monoid homomorphism of $f$ is an order additive monoid homomorphism of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{domain} (f)}{x_{8}})}$ and $\mathrm{Lex}$ applied to the set of Hahn series of the set of finite archimedean classes of $M$ and $R$.

HahnEmbedding.SeedstructureMathlib.Algebra.Order.Module.HahnEmbedding, type

Wording

no wording

English

Let $K$, $M$ and $R$ be sets. Then the elements of $\operatorname{Seed}$ applied to $K$, $M$ and $R$ are a basic type.

HahnEmbedding.Seed.baseEmbeddingdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the base embedding of seed (from the name)

English

Let $\mathrm{seed}$ be an element of $\operatorname{Seed}$ applied to $K$, $M$ and $R$. Then the base embedding of $\mathrm{seed}$ is a linear map of $M$ and $\mathrm{Lex}$ applied to the set of Hahn series of the set of finite archimedean classes of $M$ and $R$ defined as $\operatorname{mk}$ applied to the base domain of $\operatorname{toArchimedeanStrata}$ applied to $\mathrm{seed}$ and the composition of $\operatorname{toLinearMap}$ applied to the lexicographic linear equivalence of $K$ and the set of Hahn series of the set of finite archimedean classes of $M$ and $R$ and the composition of the Hahn series of $K$ and the composition of $\operatorname{toLinearMap}$ applied to the inverse of the finitely supported function linear equivalence finitely supported function of $K$ and the Hahn coefficient of $\mathrm{seed}$.

HahnEmbedding.Seed.coeffdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the coefficient of self and c (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{Seed}$ applied to $K$, $M$ and $R$. Let $c$ be a finite archimedean class of $M$. Then the coefficient of $\mathrm{self}$ and $c$ is a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{stratum} (\operatorname{toArchimedeanStrata} (\mathrm{self}), c)}{x_{8}})}$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $c$.

HahnEmbedding.Seed.coeff'defMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the coefficient of seed and c (from the name)

English

Let $\mathrm{seed}$ be an element of $\operatorname{Seed}$ applied to $K$, $M$ and $R$. Let $c$ be a finite archimedean class of $M$. Then the coefficient of $\mathrm{seed}$ and $c$ is a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{stratum'} (\operatorname{toArchimedeanStrata} (\mathrm{seed}), c)}{x_{8}})}$ and $R$ defined as the composition of the coefficient of $\mathrm{seed}$ and $c$ and the submodule preimage of the subtype of the base domain of $\operatorname{toArchimedeanStrata}$ applied to $\mathrm{seed}$ and the stratum of $\operatorname{toArchimedeanStrata}$ applied to $\mathrm{seed}$ and $c$.

HahnEmbedding.Seed.hahnCoeffdefMathlib.Algebra.Order.Module.HahnEmbedding, function or constant

Wording

the Hahn coefficient of seed (from the name)

English

Let $\mathrm{seed}$ be an element of $\operatorname{Seed}$ applied to $K$, $M$ and $R$. Then the Hahn coefficient of $\mathrm{seed}$ is a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{baseDomain} (\operatorname{toArchimedeanStrata} (\mathrm{seed}))}{x_{8}})}$ and the set of direct sums of the set of finite archimedean classes of $M$ and the function that maps $x_{9}$ to $R$ defined as the composition of $\operatorname{lmap}$ applied to $\operatorname{coeff'}$ applied to $\mathrm{seed}$ and $\operatorname{toLinearMap}$ applied to $\operatorname{decomposeLinearEquiv}$ applied to $\operatorname{stratum'}$ applied to $\operatorname{toArchimedeanStrata}$ applied to $\mathrm{seed}$.

Mathlib.Algebra.Order.Module.PositiveLinearMap

PositiveLinearMapstructureMathlib.Algebra.Order.Module.PositiveLinearMap, type

Wording

positive linear map of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the positive linear maps of $x$ and $x_{1}$ are a basic type.

PositiveLinearMap.compdefMathlib.Algebra.Order.Module.PositiveLinearMap, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a positive linear map of $x_{1}$ and $x_{2}$. Let $f$ be a positive linear map of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a positive linear map of $x$ and $x_{2}$.

PositiveLinearMap.iddefMathlib.Algebra.Order.Module.PositiveLinearMap, function or constant

Wording

the identity of R and x (from the docstring)

English

Let $R$ and $x$ be sets. Then the identity of $R$ and $x$ is a positive linear map of $x$ and $x$.

PositiveLinearMap.mk₀defMathlib.Algebra.Order.Module.PositiveLinearMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $x$ and $x_{1}$ such that for all elements $x_{9}$ of $x$, if $0 \leq x_{9}$, then $0 \leq f (x_{9})$. Then $\mathrm{PositiveLinearMap\_\_mk\_u2080\_}$ applied to $f$ and $\mathrm{hf}$ is a positive linear map of $x$ and $x_{1}$.

PositiveLinearMap.ofClassdefMathlib.Algebra.Order.Module.PositiveLinearMap, function or constant

Wording

the positive linear map of f (from the name)

English

Let $f$ be an element of $F$. Then the positive linear map of $f$ is a positive linear map of $x$ and $x_{1}$.

PositiveLinearMap.toOrderHomdefMathlib.Algebra.Order.Module.PositiveLinearMap, function or constant

Wording

the order homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a positive linear map of $x$ and $x_{1}$. Then the order homomorphism of $\mathrm{self}$ is an order homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddHom}$ applied to $\operatorname{toLinearMap}$ applied to $\mathrm{self}$ and $\operatorname{monotone'}$ applied to $\mathrm{self}$.

Mathlib.Algebra.Order.Monoid.Basic

OrderEmbedding.addLeftdefMathlib.Algebra.Order.Monoid.Basic, function or constant

Wording

no wording

English

Let $m$ be an element of $x$. Then $\operatorname{addLeft}$ applied to $m$ is an order embedding of $x$ and $x$.

OrderEmbedding.addRightdefMathlib.Algebra.Order.Monoid.Basic, function or constant

Wording

no wording

English

Let $m$ be an element of $x$. Then $\operatorname{addRight}$ applied to $m$ is an order embedding of $x$ and $x$.

OrderEmbedding.mulLeftdefMathlib.Algebra.Order.Monoid.Basic, function or constant

Wording

the left multiplicative of m (from the name)

English

Let $m$ be an element of $x$. Then the left multiplicative of $m$ is an order embedding of $x$ and $x$.

OrderEmbedding.mulRightdefMathlib.Algebra.Order.Monoid.Basic, function or constant

Wording

the right multiplicative of m (from the name)

English

Let $m$ be an element of $x$. Then the right multiplicative of $m$ is an order embedding of $x$ and $x$.

Mathlib.Algebra.Order.Monoid.Canonical.Defs

CanonicallyOrderedAddclassMathlib.Algebra.Order.Monoid.Canonical.Defs, predicate

Wording

x is a canonically ordered sum (from the name)

English

generation took over the time limit

CanonicallyOrderedMulclassMathlib.Algebra.Order.Monoid.Canonical.Defs, predicate

Wording

x is a canonically ordered product (from the name)

English

generation took over the time limit

Mathlib.Algebra.Order.Monoid.Defs

IsOrderedAddMonoidclassMathlib.Algebra.Order.Monoid.Defs, predicate

Wording

x is a ordered additive monoid (from the name)

English

Let $x$ be a set. Then we can say that $x$ is an ordered additive monoid.

IsOrderedCancelAddMonoidclassMathlib.Algebra.Order.Monoid.Defs, predicate

Wording

no wording

English

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

IsOrderedCancelMonoidclassMathlib.Algebra.Order.Monoid.Defs, predicate

Wording

no wording

English

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

IsOrderedMonoidclassMathlib.Algebra.Order.Monoid.Defs, predicate

Wording

x is a ordered monoid (from the name)

English

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

Mathlib.Algebra.Order.Monoid.Lex

OrderAddMonoidHom.fstdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the first component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is an order additive monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

OrderAddMonoidHom.fstₗdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the first component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is an order additive monoid homomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

OrderAddMonoidHom.inldefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the left injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is an order additive monoid homomorphism of $x$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderAddMonoidHom.inlₗdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the left injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is an order additive monoid homomorphism of $x$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderAddMonoidHom.inrdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the right injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is an order additive monoid homomorphism of $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderAddMonoidHom.inrₗdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the right injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is an order additive monoid homomorphism of $x_{1}$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderAddMonoidHom.snddefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the second component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the second component of $x$ and $x_{1}$ is an order additive monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

OrderMonoidHom.fstdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the first component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is an order monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

OrderMonoidHom.fstₗdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the first component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is an order monoid homomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

OrderMonoidHom.inldefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the left injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is an order monoid homomorphism of $x$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderMonoidHom.inlₗdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the left injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is an order monoid homomorphism of $x$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderMonoidHom.inrdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the right injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is an order monoid homomorphism of $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderMonoidHom.inrₗdefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the right injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is an order monoid homomorphism of $x_{1}$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

OrderMonoidHom.snddefMathlib.Algebra.Order.Monoid.Lex, function or constant

Wording

the second component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the second component of $x$ and $x_{1}$ is an order monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

LocallyFiniteOrder.addMonoidHomdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the additive monoid homomorphism of G (from the name)

English

Let $G$ be a set. Then the additive monoid homomorphism of $G$ is an additive monoid homomorphism of $G$ and $\Integer$.

LocallyFiniteOrder.orderAddMonoidEquivdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the order additive monoid equivalence of G (from the name)

English

Let $G$ be a set. Then the order additive monoid equivalence of $G$ is an order additive monoid isomorphism of $G$ and $\Integer$.

LocallyFiniteOrder.orderAddMonoidHomdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the order additive monoid homomorphism of G (from the name)

English

Let $G$ be a set. Then the order additive monoid homomorphism of $G$ is an order additive monoid homomorphism of $G$ and $\Integer$.

LocallyFiniteOrder.orderMonoidEquivdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the order monoid equivalence of G (from the name)

English

Let $G$ be a set. Then the order monoid equivalence of $G$ is an order monoid isomorphism of $G$ and the set of multiplicatives of $\Integer$ defined as $\operatorname{toMultiplicative}$ applied to the order additive monoid equivalence of $\mathrm{Additive}$ applied to $G$.

LocallyFiniteOrder.orderMonoidHomdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the order monoid homomorphism of G (from the name)

English

Let $G$ be a set. Then the order monoid homomorphism of $G$ is an order monoid homomorphism of $G$ and the set of multiplicatives of $\Integer$.

LocallyFiniteOrder.orderMonoidWithZeroEquivdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the order monoid with zero equivalence of G (from the name)

English

Let $G$ be a set. Then the order monoid with zero equivalence of $G$ is an order monoid isomorphism of $G$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ defined as the composition of the inverse of $\operatorname{withZeroUnits}$ and $\operatorname{withZero}$ applied to the order monoid equivalence of $\UnitsMACRoAO {G}$.

LocallyFiniteOrder.orderMonoidWithZeroHomdefMathlib.Algebra.Order.Monoid.LocallyFiniteOrder, function or constant

Wording

the order monoid with zero homomorphism of G (from the name)

English

Let $G$ be a set. Then the order monoid with zero homomorphism of $G$ is an order monoid with zero homomorphism of $G$ and $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$.

Mathlib.Algebra.Order.Monoid.PNat

PNat.equivNonZeroDivisorsNatdefMathlib.Algebra.Order.Monoid.PNat, function or constant

Wording

the equivalence non zero divisor natural number (from the name)

English

The equivalence non zero divisor natural number is an order monoid isomorphism of $\PNatMACRoAD$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\Natural)}{x})}$.

Mathlib.Algebra.Order.Monoid.Submonoid

AddSubmonoid.nonnegdefMathlib.Algebra.Order.Monoid.Submonoid, function or constant

Wording

no wording

English

Let $M$ be a set. Then $\operatorname{nonneg}$ applied to $M$ is an additive submonoid of $M$.

Submonoid.oneLEdefMathlib.Algebra.Order.Monoid.Submonoid, function or constant

Wording

no wording

English

Let $M$ be a set. Then $\operatorname{oneLE}$ applied to $M$ is a submonoid of $M$.

Mathlib.Algebra.Order.Monoid.ToMulBot

WithZero.toMulBotdefMathlib.Algebra.Order.Monoid.ToMulBot, function or constant

Wording

the multiplicative bottom (from the name)

English

The multiplicative bottom is a multiplicative equivalence of $\mathrm{WithZero}$ applied to the set of multiplicatives of $x$ and the set of multiplicatives of $\mathrm{WithBot}$ applied to $x$ defined as the identity map of $\mathrm{WithZero}$ applied to the set of multiplicatives of $x$.

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

AddLECancellabledefMathlib.Algebra.Order.Monoid.Unbundled.Basic, predicate

Wording

no wording

English

Let $a$ be an element of $x$. Then $\mathrm{AddLECancellable}$ holds for $a$, if for all elements $b$ and $c$ of $x$, if $a + b \leq a + c$, then $b \leq c$.

MulLECancellabledefMathlib.Algebra.Order.Monoid.Unbundled.Basic, predicate

Wording

no wording

English

Let $a$ be an element of $x$. Then $\mathrm{MulLECancellable}$ holds for $a$, if for all elements $b$ and $c$ of $x$, if $a \times b \leq a \times c$, then $b \leq c$.

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

AddLeftMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{AddLeftMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, the function that maps $x_{2}$ and $x_{3}$ to $x_{2} + x_{3}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$.

AddLeftReflectLEclassMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

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

AddLeftReflectLTdefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{AddLeftReflectLT}$ holds for $M$, if $\mathrm{ContravariantClass}$ holds for $M$, $M$, the function that maps $x_{2}$ and $x_{3}$ to $x_{2} + x_{3}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

AddLeftStrictMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{AddLeftStrictMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, the function that maps $x_{2}$ and $x_{3}$ to $x_{2} + x_{3}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

AddRightMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{AddRightMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, $\operatorname{swap}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$.

AddRightReflectLEclassMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

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

AddRightReflectLTdefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{AddRightReflectLT}$ holds for $M$, if $\mathrm{ContravariantClass}$ holds for $M$, $M$, $\operatorname{swap}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

AddRightStrictMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{AddRightStrictMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, $\operatorname{swap}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

ContravariantdefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ and $N$ be sets. Let $x$ be a function from elements of $M$ and elements of $N$ to elements of $N$. Let $r$ be a function from elements of $N$ and elements of $N$ to propositions. Then $\mathrm{Contravariant}$ holds for $M$, $N$, $x$ and $r$, if for all elements $m$ of $M$, for all elements $x_{1}$ and $x_{2}$ of $N$, if $r$ holds for $x$ applied to $m$ and $x_{1}$ and $x$ applied to $m$ and $x_{2}$, then $r$ holds for $x_{1}$ and $x_{2}$.

ContravariantClassclassMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

CovariantdefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ and $N$ be sets. Let $x$ be a function from elements of $M$ and elements of $N$ to elements of $N$. Let $r$ be a function from elements of $N$ and elements of $N$ to propositions. Then $\mathrm{Covariant}$ holds for $M$, $N$, $x$ and $r$, if for all elements $m$ of $M$, for all elements $x_{1}$ and $x_{2}$ of $N$, if $r$ holds for $x_{1}$ and $x_{2}$, then $r$ holds for $x$ applied to $m$ and $x_{1}$ and $x$ applied to $m$ and $x_{2}$.

CovariantClassclassMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

MulLeftMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{MulLeftMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, the function that maps $x_{2}$ and $x_{3}$ to $x_{2} \times x_{3}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$.

MulLeftReflectLEclassMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

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

MulLeftReflectLTdefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{MulLeftReflectLT}$ holds for $M$, if $\mathrm{ContravariantClass}$ holds for $M$, $M$, the function that maps $x_{2}$ and $x_{3}$ to $x_{2} \times x_{3}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

MulLeftStrictMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{MulLeftStrictMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, the function that maps $x_{2}$ and $x_{3}$ to $x_{2} \times x_{3}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

MulRightMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{MulRightMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, $\operatorname{swap}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$.

MulRightReflectLEclassMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

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

MulRightReflectLTdefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{MulRightReflectLT}$ holds for $M$, if $\mathrm{ContravariantClass}$ holds for $M$, $M$, $\operatorname{swap}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

MulRightStrictMonodefMathlib.Algebra.Order.Monoid.Unbundled.Defs, predicate

Wording

no wording

English

Let $M$ be a set. Then $\mathrm{MulRightStrictMono}$ holds for $M$, if $\mathrm{CovariantClass}$ holds for $M$, $M$, $\operatorname{swap}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

ExistsAddOfLEclassMathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE, predicate

Wording

no wording

English

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

ExistsMulOfLEclassMathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE, predicate

Wording

no wording

English

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

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

AddEquiv.withBotCongrdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then $\operatorname{withBotCongr}$ applied to $e$ is an additive equivalence of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

AddEquiv.withTopCongrdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then $\operatorname{withTopCongr}$ applied to $e$ is an additive equivalence of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

AddHom.withBotMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be an additive homomorphism of $M$ and $N$. Then $\operatorname{withBotMap}$ applied to $f$ is an additive homomorphism of $\mathrm{WithBot}$ applied to $M$ and $\mathrm{WithBot}$ applied to $N$.

AddHom.withTopMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be an additive homomorphism of $M$ and $N$. Then $\operatorname{withTopMap}$ applied to $f$ is an additive homomorphism of $\mathrm{WithTop}$ applied to $M$ and $\mathrm{WithTop}$ applied to $N$.

AddMonoidHom.withBotMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then $\operatorname{withBotMap}$ applied to $f$ is an additive monoid homomorphism of $\mathrm{WithBot}$ applied to $M$ and $\mathrm{WithBot}$ applied to $N$.

AddMonoidHom.withTopMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then $\operatorname{withTopMap}$ applied to $f$ is an additive monoid homomorphism of $\mathrm{WithTop}$ applied to $M$ and $\mathrm{WithTop}$ applied to $N$.

OneHom.withBotMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be an one homomorphism of $M$ and $N$. Then $\operatorname{withBotMap}$ applied to $f$ is an one homomorphism of $\mathrm{WithBot}$ applied to $M$ and $\mathrm{WithBot}$ applied to $N$.

OneHom.withTopMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be an one homomorphism of $M$ and $N$. Then $\operatorname{withTopMap}$ applied to $f$ is an one homomorphism of $\mathrm{WithTop}$ applied to $M$ and $\mathrm{WithTop}$ applied to $N$.

WithBot.addHomdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

the additive homomorphism (from the name)

English

The additive homomorphism is an additive monoid homomorphism of $x$ and $\mathrm{WithBot}$ applied to $x$.

WithTop.addHomdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

the additive homomorphism (from the name)

English

The additive homomorphism is an additive monoid homomorphism of $x$ and $\mathrm{WithTop}$ applied to $x$.

ZeroHom.withBotMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be a zero homomorphism of $M$ and $N$. Then $\operatorname{withBotMap}$ applied to $f$ is a zero homomorphism of $\mathrm{WithBot}$ applied to $M$ and $\mathrm{WithBot}$ applied to $N$.

ZeroHom.withTopMapdefMathlib.Algebra.Order.Monoid.Unbundled.WithTop, function or constant

Wording

no wording

English

Let $f$ be a zero homomorphism of $M$ and $N$. Then $\operatorname{withTopMap}$ applied to $f$ is a zero homomorphism of $\mathrm{WithTop}$ applied to $M$ and $\mathrm{WithTop}$ applied to $N$.

Mathlib.Algebra.Order.Monoid.Units

AddUnits.orderEmbeddingValdefMathlib.Algebra.Order.Monoid.Units, function or constant

Wording

the order embedding value (from the name)

English

The order embedding value is an order embedding of the set of additive units of $x$ and $x$.

Units.orderEmbeddingValdefMathlib.Algebra.Order.Monoid.Units, function or constant

Wording

the order embedding value (from the name)

English

The order embedding value is an order embedding of $\UnitsMACRoAO {x}$ and $x$.

Mathlib.Algebra.Order.Nonneg.Basic

NonnegdefMathlib.Algebra.Order.Nonneg.Basic, type

Wording

no wording

English

Let $x$ be a set. Then an element of $\mathrm{Nonneg}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {x_{3}}{\mathrm{Leq} (0 , x_{3})}$.

Nonneg.coeAddMonoidHomdefMathlib.Algebra.Order.Nonneg.Basic, function or constant

Wording

the coercion additive monoid homomorphism (from the name)

English

The coercion additive monoid homomorphism is an additive monoid homomorphism of $\mathrm{Nonneg}$ applied to $x$ and $x$.

Nonneg.coeRingHomdefMathlib.Algebra.Order.Nonneg.Basic, function or constant

Wording

the coercion ring homomorphism (from the name)

English

The coercion ring homomorphism is a ring homomorphism of $\mathrm{Nonneg}$ applied to $x$ and $x$.

Nonneg.toNonnegdefMathlib.Algebra.Order.Nonneg.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{toNonneg}$ applied to $a$ is an element of $\mathrm{Nonneg}$ applied to $x$ defined as $\MaxmaxMACRoAF {a}{0}$.

Mathlib.Algebra.Order.Nonneg.Field

Nonneg.unitsEquivPosdefMathlib.Algebra.Order.Nonneg.Field, function or constant

Wording

the unit equivalence positive part of R (from the name)

English

Let $R$ be a set. Then the unit equivalence positive part of $R$ is a multiplicative equivalence of $\UnitsMACRoAO {\mathrm{Nonneg} (R)}$ and $\SubtypeSet {r}{\mathrm{Lt} (0 , r)}$.

Mathlib.Algebra.Order.Quantale

AddQuantalestructureMathlib.Algebra.Order.Quantale, type

Wording

additive quantale of x (from the name)

English

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

AddQuantale.leftAddResiduationdefMathlib.Algebra.Order.Quantale, function or constant

Wording

the left additive residuation of x3 and y (from the name)

English

Let $x_{3}$ and $y$ be elements of $x$. Then the left additive residuation of $x_{3}$ and $y$ is an element of $x$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $z$ to $\mathrm{Leq} (z + x_{3} , y)$.

AddQuantale.rightAddResiduationdefMathlib.Algebra.Order.Quantale, function or constant

Wording

the right additive residuation of x3 and y (from the name)

English

Let $x_{3}$ and $y$ be elements of $x$. Then the right additive residuation of $x_{3}$ and $y$ is an element of $x$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $z$ to $\mathrm{Leq} (x_{3} + z , y)$.

IsAddQuantaleclassMathlib.Algebra.Order.Quantale, predicate

Wording

x is a additive quantale (from the name)

English

Let $x$ be a set. Then we can say that $x$ is an additive quantale.

IsQuantaleclassMathlib.Algebra.Order.Quantale, predicate

Wording

x is a quantale (from the name)

English

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

QuantalestructureMathlib.Algebra.Order.Quantale, type

Wording

quantale of x (from the name)

English

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

Quantale.leftMulResiduationdefMathlib.Algebra.Order.Quantale, function or constant

Wording

the left multiplicative residuation of x3 and y (from the name)

English

Let $x_{3}$ and $y$ be elements of $x$. Then the left multiplicative residuation of $x_{3}$ and $y$ is an element of $x$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $z$ to $\mathrm{Leq} (z \times x_{3} , y)$.

Quantale.rightMulResiduationdefMathlib.Algebra.Order.Quantale, function or constant

Wording

the right multiplicative residuation of x3 and y (from the name)

English

Let $x_{3}$ and $y$ be elements of $x$. Then the right multiplicative residuation of $x_{3}$ and $y$ is an element of $x$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $z$ to $\mathrm{Leq} (x_{3} \times z , y)$.

Mathlib.Algebra.Order.Ring.Abs

absHomdefMathlib.Algebra.Order.Ring.Abs, function or constant

Wording

the absolute value homomorphism (from the name)

English

The absolute value homomorphism is a monoid with zero homomorphism of $x$ and $x$.

Mathlib.Algebra.Order.Ring.Archimedean

ArchimedeanClass.addValuationdefMathlib.Algebra.Order.Ring.Archimedean, function or constant

Wording

the additive valuation of R (from the name)

English

Let $R$ be a set. Then the additive valuation of $R$ is an additive valuation of $R$ and the set of archimedean classes of $R$.

Mathlib.Algebra.Order.Ring.Basic

IsNonarchimedeandefMathlib.Algebra.Order.Ring.Basic, predicate

Wording

f is a nonarchimedean (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $R$. Then $f$ is a nonarchimedean, if for all elements $a$ and $b$ of $x_{1}$, $f (a + b)\leq \MaxmaxMACRoAF {f (a)}{f (b)}$.

Mathlib.Algebra.Order.Ring.Cone

RingConestructureMathlib.Algebra.Order.Ring.Cone, type

Wording

ring cone of R (from the name)

English

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

RingCone.nonnegdefMathlib.Algebra.Order.Ring.Cone, function or constant

Wording

no wording

English

Let $T$ be a set. Then $\operatorname{nonneg}$ applied to $T$ is a ring cone of $T$.

RingCone.toAddGroupConedefMathlib.Algebra.Order.Ring.Cone, function or constant

Wording

the additive group cone of self (from the name)

English

Let $\mathrm{self}$ be a ring cone of $R$. Then the additive group cone of $\mathrm{self}$ is an additive group cone of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the carrier of $\operatorname{toSubsemigroup}$ applied to $\operatorname{toSubmonoid}$ applied to $\operatorname{toSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{Subsemiring\_\_add\_mem'}$ applied to $\operatorname{toSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{Subsemiring\_\_zero\_mem'}$ applied to $\operatorname{toSubsemiring}$ applied to $\mathrm{self}$ and $\mathrm{RingCone\_\_eq\_zero\_of\_mem\_of\_neg\_mem'}$ applied to $\mathrm{self}$.

RingConeClassclassMathlib.Algebra.Order.Ring.Cone, predicate

Wording

R is a ring cone class (from the name)

English

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

Mathlib.Algebra.Order.Ring.Defs

IsOrderedRingclassMathlib.Algebra.Order.Ring.Defs, predicate

Wording

R is a ordered ring (from the name)

English

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

IsStrictOrderedRingclassMathlib.Algebra.Order.Ring.Defs, predicate

Wording

R is a strict ordered ring (from the name)

English

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

Mathlib.Algebra.Order.Ring.Idempotent

OrderIso.isIdempotentElemMulZeroAddOnedefMathlib.Algebra.Order.Ring.Idempotent, function or constant

Wording

no wording

English

$\operatorname{isIdempotentElemMulZeroAddOne}$ is an order isomorphism of $\SubtypeSet {a}{\mathrm{IsIdempotentElem} (a)}$ and $\SubtypeSet {a_{1}}{\mathrm{and} (\EqtMACRoH {(\ProdfstMACRoZ {a_{1}}\times \ProdsndMACRoAA {a_{1}})}{0}, \EqtMACRoH {(\ProdfstMACRoZ {a_{1}}+ \ProdsndMACRoAA {a_{1}})}{1})}$.

Mathlib.Algebra.Order.Ring.Ordering.Basic

RingPreordering.mk'defMathlib.Algebra.Order.Ring.Ordering.Basic, function or constant

Wording

no wording

English

Let $P$ be an element of $\wp R$ such that for all elements $x_{3}$ of $R$, for all elements $y_{1}$ of $R$, if $x_{3}$ is an element of $P$, then if $y_{1}$ is an element of $P$, then $x_{3} + y_{1}$ is an element of $P$, for all elements $x_{2}$ of $R$, for all elements $y$ of $R$, if $x_{2}$ is an element of $P$, then if $y$ is an element of $P$, then $x_{2} \times y$ is an element of $P$, for all elements $x_{1}$ of $R$, $x_{1} \times x_{1}$ is an element of $P$ and $\operatorname{neg}$ applied to $1$ is not an element of $P$. Then $\operatorname{mk'}$ applied to $P$, $\mathrm{add}$, $\mathrm{mul}$, $\mathrm{sq}$ and $\mathrm{neg\_one}$ is a ring preordering of $R$.

Mathlib.Algebra.Order.Ring.Ordering.Defs

RingPreorderingstructureMathlib.Algebra.Order.Ring.Ordering.Defs, type

Wording

ring preordering of R (from the name)

English

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

RingPreordering.HasIdealSupportclassMathlib.Algebra.Order.Ring.Ordering.Defs, predicate

Wording

P has ideal supports (from the name)

English

Let $P$ be a ring preordering of $R$. Then we can say that $P$ has ideal supports.

RingPreordering.IsOrderingclassMathlib.Algebra.Order.Ring.Ordering.Defs, predicate

Wording

P is a ordering (from the name)

English

Let $P$ be a ring preordering of $R$. Then we can say that $P$ is an ordering.

RingPreordering.copydefMathlib.Algebra.Order.Ring.Ordering.Defs, function or constant

Wording

the copy of P and S (from the name)

English

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

RingPreordering.supportdefMathlib.Algebra.Order.Ring.Ordering.Defs, function or constant

Wording

the support of P (from the docstring)

English

Let $P$ be a ring preordering of $R$. Then the support of $P$ is an ideal of $R$.

RingPreordering.supportAddSubgroupdefMathlib.Algebra.Order.Ring.Ordering.Defs, function or constant

Wording

the support of P (from the docstring)

English

Let $P$ be a ring preordering of $R$. Then the support of $P$ is an additive subgroup of $R$.

Mathlib.Algebra.Order.Ring.StandardPart

ArchimedeanClass.FiniteElementdefMathlib.Algebra.Order.Ring.StandardPart, type

Wording

finite element of K (from the name)

English

Let $K$ be a set. Then a finite element of $K$ is an element of the function that maps $K$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{valuationSubring} (\operatorname{toValuation} (\operatorname{addValuation} (K)))}{x_{2}})}$.

ArchimedeanClass.FiniteElement.mkdefMathlib.Algebra.Order.Ring.StandardPart, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $K$ such that $0 \leq \operatorname{mk} (x_{2})$. Then $\operatorname{mk}$ applied to $x_{2}$ and $h_{1}$ is a finite element of $K$ defined as $x_{2}$.

ArchimedeanClass.FiniteResidueFielddefMathlib.Algebra.Order.Ring.StandardPart, type

Wording

residue field of K (from the docstring)

English

Let $K$ be a set. Then a residue field of $K$ is an element of the function that maps $K$ to the set of residue fields of the set of finite elements of $K$.

ArchimedeanClass.FiniteResidueField.mkdefMathlib.Algebra.Order.Ring.StandardPart, function or constant

Wording

no wording

English

$\operatorname{mk}$ is an order ring homomorphism of the set of finite elements of $K$ and the set of residue fields of $K$.

ArchimedeanClass.FiniteResidueField.ofArchimedeandefMathlib.Algebra.Order.Ring.StandardPart, function or constant

Wording

the finite residue field of f (from the name)

English

Let $f$ be an order ring homomorphism of $R$ and $K$. Then the finite residue field of $f$ is an order ring homomorphism of $R$ and the set of residue fields of $K$.

ArchimedeanClass.stdPartdefMathlib.Algebra.Order.Ring.StandardPart, function or constant

Wording

the standard part of x2 (from the docstring)

English

Let $x_{2}$ be an element of $K$. Then the standard part of $x_{2}$ is a real number defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (0 , \operatorname{mk} (x_{2}))$, the function that maps $h_{1}$ to $\operatorname{comp}$ applied to $\operatorname{ofNonempty}$, $\operatorname{mk}$ and $\operatorname{mk}$ applied to $x_{2}$ and $h_{1}$ and the function that maps $h_{2}$ to $0$.

Mathlib.Algebra.Order.Ring.WithTop

MonoidWithZeroHom.withBotMapdefMathlib.Algebra.Order.Ring.WithTop, function or constant

Wording

no wording

English

Let $f$ be a monoid with zero homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{withBotMap}$ applied to $f$ and $\mathrm{hf}$ is a monoid with zero homomorphism of $\mathrm{WithBot}$ applied to $R$ and $\mathrm{WithBot}$ applied to $S$.

MonoidWithZeroHom.withTopMapdefMathlib.Algebra.Order.Ring.WithTop, function or constant

Wording

no wording

English

Let $f$ be a monoid with zero homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{withTopMap}$ applied to $f$ and $\mathrm{hf}$ is a monoid with zero homomorphism of $\mathrm{WithTop}$ applied to $R$ and $\mathrm{WithTop}$ applied to $S$.

RingHom.withBotMapdefMathlib.Algebra.Order.Ring.WithTop, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{withBotMap}$ applied to $f$ and $\mathrm{hf}$ is a ring homomorphism of $\mathrm{WithBot}$ applied to $R$ and $\mathrm{WithBot}$ applied to $S$.

RingHom.withTopMapdefMathlib.Algebra.Order.Ring.WithTop, function or constant

Wording

no wording

English

Let $f$ be a ring homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{withTopMap}$ applied to $f$ and $\mathrm{hf}$ is a ring homomorphism of $\mathrm{WithTop}$ applied to $R$ and $\mathrm{WithTop}$ applied to $S$.

Mathlib.Algebra.Order.Round

rounddefMathlib.Algebra.Order.Round, function or constant

Wording

the round of x4 (from the name)

English

Let $x_{4}$ be an element of $x$. Then the round of $x_{4}$ is an element of $\Integer$ defined as $\iteMACRoG {\mathrm{Lt} (2 \times \operatorname{fract} (x_{4}), 1)}{\operatorname{floor} (x_{4})}{\operatorname{ceil} (x_{4})}$.

Mathlib.Algebra.Order.Star.Basic

SelfAdjointDecomposeclassMathlib.Algebra.Order.Star.Basic, predicate

Wording

no wording

English

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

StarOrderedRingclassMathlib.Algebra.Order.Star.Basic, predicate

Wording

R is a star ordered ring (from the name)

English

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

Mathlib.Algebra.Order.Sub.Defs

OrderedSubclassMathlib.Algebra.Order.Sub.Defs, predicate

Wording

x is a ordered difference (from the name)

English

Let $x$ be a set. Then we can say that $x$ is an ordered difference.

Mathlib.Algebra.Order.Sub.WithTop

WithTop.subdefMathlib.Algebra.Order.Sub.WithTop, function or constant

Wording

the difference of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{WithTop}$ applied to $x$. Then the difference of $x_{3}$ and $x_{4}$ is an element of $\mathrm{WithTop}$ applied to $x$.

Mathlib.Algebra.Order.SuccPred

PredSubOrderclassMathlib.Algebra.Order.SuccPred, predicate

Wording

x is a predecessor difference order (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a predecessor difference order.

SuccAddOrderclassMathlib.Algebra.Order.SuccPred, predicate

Wording

x is a successor additive order (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a successor additive order.

Mathlib.Algebra.Order.ToIntervalMod

QuotientAddGroup.equivIcoModdefMathlib.Algebra.Order.ToIntervalMod, function or constant

Wording

no wording

English

Assume that $0 < p$. Let $a$ be an element of $x$. Then $\operatorname{equivIcoMod}$ applied to $\mathrm{hp}$ and $a$ is an equivalence from the set of quotients of $x$ and $\operatorname{zmultiples}$ applied to $p$ to the set of elements of $\operatorname{Ico}$ applied to $a$ and $a + p$.

QuotientAddGroup.equivIocModdefMathlib.Algebra.Order.ToIntervalMod, function or constant

Wording

no wording

English

Assume that $0 < p$. Let $a$ be an element of $x$. Then $\operatorname{equivIocMod}$ applied to $\mathrm{hp}$ and $a$ is an equivalence from the set of quotients of $x$ and $\operatorname{zmultiples}$ applied to $p$ to the set of elements of $\operatorname{Ioc}$ applied to $a$ and $a + p$.

toIcoDivdefMathlib.Algebra.Order.ToIntervalMod, function or constant

Wording

no wording

English

Assume that $0 < p$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{toIcoDiv}$ applied to $\mathrm{hp}$, $a$ and $b$ is an integer defined as $\operatorname{choose}$ applied to $\mathrm{existsUnique\_sub\_zsmul\_mem\_Ico}$ applied to $\mathrm{hp}$, $b$ and $a$.

toIcoModdefMathlib.Algebra.Order.ToIntervalMod, function or constant

Wording

no wording

English

Assume that $0 < p$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{toIcoMod}$ applied to $\mathrm{hp}$, $a$ and $b$ is an element of $x$ defined as $b - \HSMulhSMulMACRoAL {\mathrm{toIcoDiv} (\mathrm{hp} , a , b)}{p}$.

toIocDivdefMathlib.Algebra.Order.ToIntervalMod, function or constant

Wording

no wording

English

Assume that $0 < p$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{toIocDiv}$ applied to $\mathrm{hp}$, $a$ and $b$ is an integer defined as $\operatorname{choose}$ applied to $\mathrm{existsUnique\_sub\_zsmul\_mem\_Ioc}$ applied to $\mathrm{hp}$, $b$ and $a$.

toIocModdefMathlib.Algebra.Order.ToIntervalMod, function or constant

Wording

no wording

English

Assume that $0 < p$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{toIocMod}$ applied to $\mathrm{hp}$, $a$ and $b$ is an element of $x$ defined as $b - \HSMulhSMulMACRoAL {\mathrm{toIocDiv} (\mathrm{hp} , a , b)}{p}$.

Mathlib.Algebra.Order.WithTop.Untop0

WithTop.untop₀defMathlib.Algebra.Order.WithTop.Untop0, function or constant

Wording

no wording

English

Let $a$ be an element of $\mathrm{WithTop}$ applied to $x$. Then $\mathrm{WithTop\_\_untop\_u2080\_}$ applied to $a$ is an element of $x$ defined as $\operatorname{untopD}$ applied to $0$ and $a$.

Mathlib.Algebra.Order.ZeroLEOne

ZeroLEOneClassclassMathlib.Algebra.Order.ZeroLEOne, predicate

Wording

no wording

English

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

Mathlib.Algebra.Polynomial.AlgebraMap

Polynomial.CAlgHomdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the algebra homomorphism (from the name)

English

The algebra homomorphism is an algebra homomorphism of $A$ and the set of polynomials of $A$.

Polynomial.aevaldefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the algebra evaluation of x3 (from the name)

English

Let $x_{3}$ be an element of $A$. Then the algebra evaluation of $x_{3}$ is an algebra homomorphism of the set of polynomials of $R$ and $A$ defined as $\operatorname{aevalEquiv}$ applied to $R$, $A$ and $x_{3}$.

Polynomial.aevalEquivdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the algebra evaluation equivalence of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the algebra evaluation equivalence of $R$ and $A$ is an equivalence from $A$ to the set of algebra homomorphisms of the set of polynomials of $R$ and $A$.

Polynomial.aevalTowerdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the algebra evaluation tower of f and x5 (from the name)

English

Let $f$ be an algebra homomorphism of $R$ and $\mathrm{A'}$. Let $x_{5}$ be an element of $\mathrm{A'}$. Then the algebra evaluation tower of $f$ and $x_{5}$ is an algebra homomorphism of the set of polynomials of $R$ and $\mathrm{A'}$.

Polynomial.algEquivAevalNegXdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the algebra isomorphism algebra evaluation negation (from the name)

English

The algebra isomorphism algebra evaluation negation is an algebra isomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

Polynomial.algEquivAevalXAddCdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

no wording

English

Let $t$ be an element of $R$. Then $\operatorname{algEquivAevalXAddC}$ applied to $t$ is an algebra isomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

Polynomial.algEquivCMulXAddCdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $R$. Then $\operatorname{algEquivCMulXAddC}$ applied to $a$ and $b$ is an algebra isomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

Polynomial.algEquivOfCompEqXdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the algebra isomorphism of p and q (from the name)

English

Let $p$ and $q$ be polynomials of $R$ such that the composition of $p$ and $q$ is equal to $\operatorname{X}$ and the composition of $q$ and $p$ is equal to $\operatorname{X}$. Then the algebra isomorphism of $p$ and $q$ is an algebra isomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

Polynomial.eval₂AlgHomdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the evaluation algebra homomorphism of f and b (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $b$ be an element of $B$ such that for all elements $a$ of $A$, $\mathrm{Commute}$ holds for $f$ applied to $a$ and $b$. Then the evaluation algebra homomorphism of $f$ and $b$ is an algebra homomorphism of the set of polynomials of $A$ and $B$.

Polynomial.mapAlgdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the map of R and S (from the docstring)

English

Let $R$ and $S$ be sets. Then the map of $R$ and $S$ is an algebra homomorphism of the set of polynomials of $R$ and the set of polynomials of $S$ defined as the algebra evaluation of $\operatorname{X}$.

Polynomial.mapAlgEquivdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the map algebra isomorphism of f (from the name)

English

Let $f$ be an algebra isomorphism of $A$ and $B$. Then the map algebra isomorphism of $f$ is an algebra isomorphism of the set of polynomials of $A$ and the set of polynomials of $B$.

Polynomial.mapAlgHomdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the map algebra homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the map algebra homomorphism of $f$ is an algebra homomorphism of the set of polynomials of $A$ and the set of polynomials of $B$.

Polynomial.toFinsuppIsoAlgdefMathlib.Algebra.Polynomial.AlgebraMap, function or constant

Wording

the finitely supported function isomorphism algebra of R (from the name)

English

Let $R$ be a set. Then the finitely supported function isomorphism algebra of $R$ is an algebra isomorphism of the set of polynomials of $R$ and the set of additive monoid algebras of $R$ and $\Natural$.

Mathlib.Algebra.Polynomial.Basic

PolynomialstructureMathlib.Algebra.Polynomial.Basic, type

Wording

polynomial of R (from the name)

English

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

Polynomial.CdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

no wording

English

$\operatorname{C}$ is a ring homomorphism of $R$ and the set of polynomials of $R$.

Polynomial.XdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

no wording

English

$\operatorname{X}$ is a polynomial of $R$ defined as $\operatorname{monomial}$ applied to $1$ and $1$.

Polynomial.coeffdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the coefficient of x1 (from the name)

English

Let $x_{1}$ be a polynomial of $R$. Then the coefficient of $x_{1}$ is an element of $\FinsuppMACRoQ {\Natural}{R}$.

Polynomial.coeffsdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Then $\operatorname{coeffs}$ applied to $p$ is a finite set of $R$ defined as the forward image of the support of $p$ under the function that maps $n$ to $\operatorname{coeff}$ applied to $p$ and $n$.

Polynomial.erasedefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $x_{1}$ be a polynomial of $R$. Then $\operatorname{erase}$ applied to $n$ and $x_{1}$ is a polynomial of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{Polynomial\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_Polynomial\_\_Basic\_\_2141038364\_\_\_hygCtx\_\_\_hyg\_\_2}$, $n$ and $x_{1}$.

Polynomial.monomialdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the monomial of n (from the docstring)

English

Let $n$ be a natural number. Then the monomial of $n$ is a linear map of $R$ and the set of polynomials of $R$.

Polynomial.ofMultisetdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the polynomial (from the name)

English

The polynomial is an additive characteristic of the set of multisets of $R$ and the set of polynomials of $R$.

Polynomial.sumdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the sum of p and f (from the name)

English

Let $p$ be a polynomial of $R$. Let $f$ be a function from elements of $\Natural$ and elements of $R$ to elements of $S$. Then the sum of $p$ and $f$ is an element of $S$ defined as $\FinsetSum {\operatorname{support} (p)}{n}{f (n , \operatorname{coeff} (p , n))}$.

Polynomial.supportdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the support of x1 (from the name)

English

Let $x_{1}$ be a polynomial of $R$. Then the support of $x_{1}$ is a finite set of $\Natural$.

Polynomial.toFinsuppdefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the finitely supported function of self (from the name)

English

Let $\mathrm{self}$ be a polynomial of $R$. Then the finitely supported function of $\mathrm{self}$ is an additive monoid algebra of $R$ and $\Natural$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Polynomial.toFinsuppIsodefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

the finitely supported function isomorphism of R (from the name)

English

Let $R$ be a set. Then the finitely supported function isomorphism of $R$ is a ring isomorphism of the set of polynomials of $R$ and the set of additive monoid algebras of $R$ and $\Natural$.

Polynomial.toFinsuppIsoLineardefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{toFinsuppIsoLinear}$ applied to $R$ is a linear equivalence of the set of polynomials of $R$ and the set of additive monoid algebras of $R$ and $\Natural$.

Polynomial.updatedefMathlib.Algebra.Polynomial.Basic, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Let $n$ be a natural number. Let $a$ be an element of $R$. Then $\operatorname{update}$ applied to $p$, $n$ and $a$ is a polynomial of $R$ defined as $\operatorname{ofFinsupp}$ applied to $\operatorname{update}$ applied to $n$, $a$ and the finitely supported function of $p$.

Mathlib.Algebra.Polynomial.Basis

Polynomial.basisMonomialsdefMathlib.Algebra.Polynomial.Basis, function or constant

Wording

the basis monomial of R (from the name)

English

Let $R$ be a set. Then the basis monomial of $R$ is a basis of $R$ and the set of polynomials of $R$ defined as $\operatorname{ofRepr}$ applied to the composition of $\operatorname{toFinsuppIsoLinear}$ applied to $R$ and the coefficient linear equivalence of $R$.

Mathlib.Algebra.Polynomial.Bivariate

AdjoinRoot.evalEvaldefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the evaluation evaluation of h (from the name)

English

Assume that the evaluation evaluation of $y$ and $p$ is equal to $0$. Then the evaluation evaluation of $h$ is a ring homomorphism of $\mathrm{AdjoinRoot}$ applied to $p$ and $R$.

Polynomial.Bivariate.equivMvPolynomialdefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the equivalence multivariate polynomial of R (from the name)

English

Let $R$ be a set. Then the equivalence multivariate polynomial of $R$ is an algebra isomorphism of the set of polynomials of the set of polynomials of $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $2$ and $R$.

Polynomial.Bivariate.swapdefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the swap (from the name)

English

The swap is an algebra isomorphism of the set of polynomials of the set of polynomials of $R$ and the set of polynomials of the set of polynomials of $R$.

Polynomial.CCdefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Then $\operatorname{CC}$ applied to $r$ is a polynomial of the set of polynomials of $R$ defined as $\operatorname{C}$ applied to $\operatorname{C}$ applied to $r$.

Polynomial.aevalAevaldefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the algebra evaluation algebra evaluation of x3 and y (from the name)

English

Let $x_{3}$ and $y$ be elements of $A$. Then the algebra evaluation algebra evaluation of $x_{3}$ and $y$ is an algebra homomorphism of the set of polynomials of the set of polynomials of $R$ and $A$ defined as $\operatorname{aevalAevalEquiv}$ applied to $R$, $A$ and $\ProdmkMACRoU {x_{3}}{y}$.

Polynomial.aevalAevalEquivdefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the algebra evaluation algebra evaluation equivalence of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the algebra evaluation algebra evaluation equivalence of $R$ and $A$ is an equivalence from $\mathrm{Prod}$ applied to $A$ and $A$ to the set of algebra homomorphisms of the set of polynomials of the set of polynomials of $R$ and $A$.

Polynomial.evalEvaldefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the evaluation evaluation of y and p (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Let $p$ be a polynomial of the set of polynomials of $R$. Then the evaluation evaluation of $y$ and $p$ is an element of $R$ defined as the evaluation of $x_{1}$ and the evaluation of $\operatorname{C}$ applied to $y$ and $p$.

Polynomial.evalEvalRingHomdefMathlib.Algebra.Polynomial.Bivariate, function or constant

Wording

the evaluation evaluation ring homomorphism of x1 and y (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Then the evaluation evaluation ring homomorphism of $x_{1}$ and $y$ is a ring homomorphism of the set of polynomials of the set of polynomials of $R$ and $R$ defined as the composition of the evaluation ring homomorphism of $x_{1}$ and the evaluation ring homomorphism of $\operatorname{C}$ applied to $y$.

Mathlib.Algebra.Polynomial.CancelLeads

Polynomial.cancelLeadsdefMathlib.Algebra.Polynomial.CancelLeads, function or constant

Wording

no wording

English

Let $p$ and $q$ be polynomials of $R$. Then $\operatorname{cancelLeads}$ applied to $p$ and $q$ is a polynomial of $R$ defined as the difference between the product of $\operatorname{C}$ applied to the leading coefficient of $p$, the exponentiation of $\operatorname{X}$ to the difference between the natural degree of $p$ and the natural degree of $q$ and $q$ and the product of $\operatorname{C}$ applied to the leading coefficient of $q$, the exponentiation of $\operatorname{X}$ to the difference between the natural degree of $q$ and the natural degree of $p$ and $p$.

Mathlib.Algebra.Polynomial.Coeff

Polynomial.constantCoeffdefMathlib.Algebra.Polynomial.Coeff, function or constant

Wording

the constant coefficient (from the name)

English

The constant coefficient is a ring homomorphism of the set of polynomials of $R$ and $R$.

Polynomial.lcoeffdefMathlib.Algebra.Polynomial.Coeff, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then $\operatorname{lcoeff}$ applied to $R$ and $n$ is a linear map of the set of polynomials of $R$ and $R$.

Polynomial.lsumdefMathlib.Algebra.Polynomial.Coeff, function or constant

Wording

no wording

English

Let $f$ be a function from natural numbers to linear maps of $A$ and $M$. Then $\operatorname{lsum}$ applied to $f$ is a linear map of the set of polynomials of $A$ and $M$.

Mathlib.Algebra.Polynomial.CoeffList

Polynomial.coeffListdefMathlib.Algebra.Polynomial.CoeffList, function or constant

Wording

the coefficient list of P (from the name)

English

Let $P$ be a polynomial of $R$. Then the coefficient list of $P$ is a list of elements of $R$ defined as $\operatorname{map}$ applied to $\operatorname{coe}$ applied to the coefficient of $P$ and $\operatorname{reverse}$ applied to $\operatorname{range}$ applied to the successor of the degree of $P$.

Polynomial.ofCoeffListdefMathlib.Algebra.Polynomial.CoeffList, function or constant

Wording

the polynomial of x1 (from the name)

English

Let $x_{1}$ be a list of elements of $R$. Then the polynomial of $x_{1}$ is a polynomial of $R$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Polynomial\_\_ofCoeffList\_\_\_f}$.

Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Polynomial.cardPowDegreedefMathlib.Algebra.Polynomial.Degree.CardPowDegree, function or constant

Wording

the cardinality power degree (from the name)

English

The cardinality power degree is an absolute value of the set of polynomials of $\mathrm{Fq}$ and $\Integer$.

Mathlib.Algebra.Polynomial.Degree.Defs

Polynomial.MonicdefMathlib.Algebra.Polynomial.Degree.Defs, predicate

Wording

p is monic (from the name)

English

Let $p$ be a polynomial of $R$. Then $p$ is monic, if the leading coefficient of $p$ is equal to $1$.

Polynomial.degreedefMathlib.Algebra.Polynomial.Degree.Defs, function or constant

Wording

the degree of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the degree of $p$ is an element of $\mathrm{WithBot}$ applied to $\Natural$ defined as the maximum of the support of $p$.

Polynomial.leadingCoeffdefMathlib.Algebra.Polynomial.Degree.Defs, function or constant

Wording

the leading coefficient of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the leading coefficient of $p$ is an element of $R$ defined as $\operatorname{coeff}$ applied to $p$ and the natural degree of $p$.

Polynomial.natDegreedefMathlib.Algebra.Polynomial.Degree.Defs, function or constant

Wording

the natural degree of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the natural degree of $p$ is a natural number defined as $\operatorname{unbotD}$ applied to $0$ and the degree of $p$.

Polynomial.nextCoeffdefMathlib.Algebra.Polynomial.Degree.Defs, function or constant

Wording

the next coefficient of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the next coefficient of $p$ is an element of $R$ defined as $\iteMACRoG {\mathrm{Eq} (\operatorname{natDegree} (p), 0)}{0}{\operatorname{coeff} (p , \operatorname{natDegree} (p)- 1)}$.

Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Polynomial.IsMonicOfDegreestructureMathlib.Algebra.Polynomial.Degree.IsMonicOfDegree, predicate

Wording

no wording

English

Let $p$ be a polynomial of $R$. Let $n$ be a natural number. Then we can say that $\operatorname{IsMonicOfDegree}$ holds for $p$ and $n$.

Mathlib.Algebra.Polynomial.Degree.Operations

Polynomial.degreeMonoidHomdefMathlib.Algebra.Polynomial.Degree.Operations, function or constant

Wording

the degree monoid homomorphism (from the name)

English

The degree monoid homomorphism is a monoid homomorphism of the set of polynomials of $R$ and the set of multiplicatives of $\mathrm{WithBot}$ applied to $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{degree}$ and $\mathrm{Polynomial\_\_degree\_one}$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Polynomial\_\_degree\_mul}$.

Polynomial.leadingCoeffHomdefMathlib.Algebra.Polynomial.Degree.Operations, function or constant

Wording

the leading coefficient homomorphism (from the name)

English

The leading coefficient homomorphism is a monoid homomorphism of the set of polynomials of $R$ and $R$.

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Polynomial.TrailingMonicdefMathlib.Algebra.Polynomial.Degree.TrailingDegree, predicate

Wording

no wording

English

Let $p$ be a polynomial of $R$. Then $\operatorname{TrailingMonic}$ holds for $p$, if $\EqtMACRoH {\operatorname{trailingCoeff} (p)}{1}$.

Polynomial.natTrailingDegreedefMathlib.Algebra.Polynomial.Degree.TrailingDegree, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Then $\operatorname{natTrailingDegree}$ applied to $p$ is a natural number defined as the natural number of $\operatorname{trailingDegree}$ applied to $p$.

Polynomial.nextCoeffUpdefMathlib.Algebra.Polynomial.Degree.TrailingDegree, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Then $\operatorname{nextCoeffUp}$ applied to $p$ is an element of $R$ defined as $\iteMACRoG {\mathrm{Eq} (\operatorname{natTrailingDegree} (p), 0)}{0}{\operatorname{coeff} (p , \operatorname{natTrailingDegree} (p)+ 1)}$.

Polynomial.trailingCoeffdefMathlib.Algebra.Polynomial.Degree.TrailingDegree, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Then $\operatorname{trailingCoeff}$ applied to $p$ is an element of $R$ defined as $\operatorname{coeff}$ applied to $p$ and $\operatorname{natTrailingDegree}$ applied to $p$.

Polynomial.trailingDegreedefMathlib.Algebra.Polynomial.Degree.TrailingDegree, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Then $\operatorname{trailingDegree}$ applied to $p$ is a natural number defined as the minimum of the support of $p$.

Mathlib.Algebra.Polynomial.DenomsClearable

DenomsClearabledefMathlib.Algebra.Polynomial.DenomsClearable, predicate

Wording

no wording

English

Let $a$ and $b$ be elements of $R$. Let $N$ be a natural number. Let $f$ be a polynomial of $R$. Let $i$ be a ring homomorphism of $R$ and $K$. Then $\mathrm{DenomsClearable}$ holds for $a$, $b$, $N$, $f$ and $i$, if there exists an element $D$ of $R$, such that there exists an element $\mathrm{bi}$ of $K$, such that $\EqtMACRoH {\mathrm{bi} \times i (b)}{1}$ and $i$ applied to $D$ is equal to the product of $i (b)^ {N}$ and the evaluation of $i (a)\times \mathrm{bi}$ and the map of $i$ and $f$.

Mathlib.Algebra.Polynomial.Derivation

Derivation.compAEvaldefMathlib.Algebra.Polynomial.Derivation, function or constant

Wording

the composition evaluation of d and a (from the name)

English

Let $d$ be a derivation of $A$ and $M$. Let $a$ be an element of $A$. Then the composition evaluation of $d$ and $a$ is a derivation of the set of polynomials of $R$ and the set of evaluations of $M$ and $a$.

Polynomial.derivative'defMathlib.Algebra.Polynomial.Derivation, function or constant

Wording

the derivative (from the name)

English

The derivative is a derivation of the set of polynomials of $R$ and the set of polynomials of $R$.

Polynomial.mkDerivationdefMathlib.Algebra.Polynomial.Derivation, function or constant

Wording

the derivation of R (from the name)

English

Let $R$ be a set. Then the derivation of $R$ is a linear map of $A$ and the set of derivations of the set of polynomials of $R$ and $A$.

Polynomial.mkDerivationEquivdefMathlib.Algebra.Polynomial.Derivation, function or constant

Wording

the derivation equivalence of R (from the name)

English

Let $R$ be a set. Then the derivation equivalence of $R$ is a linear equivalence of $A$ and the set of derivations of the set of polynomials of $R$ and $A$.

Mathlib.Algebra.Polynomial.Derivative

Polynomial.derivativedefMathlib.Algebra.Polynomial.Derivative, function or constant

Wording

the formal derivative of the polynomial (from the docstring)

English

The formal derivative of the polynomial is a linear map of the set of polynomials of $R$ and the set of polynomials of $R$.

Polynomial.derivativeFinsuppdefMathlib.Algebra.Polynomial.Derivative, function or constant

Wording

the derivative finitely supported function (from the name)

English

The derivative finitely supported function is a linear map of the set of polynomials of $R$ and the set of finitely supported functions from $\Natural$ to the set of polynomials of $R$.

Mathlib.Algebra.Polynomial.Div

Polynomial.divByMonicdefMathlib.Algebra.Polynomial.Div, function or constant

Wording

no wording

English

Let $p$ and $q$ be polynomials of $R$. Then $\operatorname{divByMonic}$ applied to $p$ and $q$ is a polynomial of $R$ defined as $\mathrm{dite}$ applied to the proposition that $q$ is monic, the function that maps $\mathrm{hq}$ to $\ProdfstMACRoZ {\operatorname{divModByMonicAux} (p , \mathrm{hq})}$ and the function that maps $\mathrm{hq1}$ to $0$.

Polynomial.modByMonicdefMathlib.Algebra.Polynomial.Div, function or constant

Wording

no wording

English

Let $p$ and $q$ be polynomials of $R$. Then $\operatorname{modByMonic}$ applied to $p$ and $q$ is a polynomial of $R$ defined as $\mathrm{dite}$ applied to the proposition that $q$ is monic, the function that maps $\mathrm{hq}$ to $\ProdsndMACRoAA {\operatorname{divModByMonicAux} (p , \mathrm{hq})}$ and the function that maps $\mathrm{hq1}$ to $p$.

Polynomial.rootMultiplicitydefMathlib.Algebra.Polynomial.Div, function or constant

Wording

the root multiplicity of a and p (from the name)

English

Let $a$ be an element of $R$. Let $p$ be a polynomial of $R$. Then the root multiplicity of $a$ and $p$ is a natural number defined as $\mathrm{dite}$ applied to $\EqtMACRoH {p}{0}$, the function that maps $h_{0}$ to $0$ and the function that maps $h_{01}$ to $\operatorname{find}$ applied to $\mathrm{Polynomial\_\_finiteMultiplicity\_X\_sub\_C}$ applied to $a$ and $h_{01}$.

Mathlib.Algebra.Polynomial.EraseLead

Polynomial.eraseLeaddefMathlib.Algebra.Polynomial.EraseLead, function or constant

Wording

no wording

English

Let $f$ be a polynomial of $R$. Then $\operatorname{eraseLead}$ applied to $f$ is a polynomial of $R$ defined as $\operatorname{erase}$ applied to the natural degree of $f$ and $f$.

Mathlib.Algebra.Polynomial.Eval.Coeff

Polynomial.piEquivdefMathlib.Algebra.Polynomial.Eval.Coeff, function or constant

Wording

the polynomial ring of R (from the docstring)

English

Let $R$ be a function from elements of $x$ to sets. Then the polynomial ring of $R$ is a ring isomorphism of the set of polynomials of the set of functions from elements $i$ of $x$ to elements of $R$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to polynomials of $R$ applied to $i_{1}$.

Mathlib.Algebra.Polynomial.Eval.Defs

Polynomial.IsRootdefMathlib.Algebra.Polynomial.Eval.Defs, predicate

Wording

no wording

English

Let $p$ be a polynomial of $R$. Let $a$ be an element of $R$. Then $\operatorname{IsRoot}$ holds for $p$ and $a$, if the evaluation of $a$ and $p$ is equal to $0$.

Polynomial.compdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the composition of p and q (from the name)

English

Let $p$ and $q$ be polynomials of $R$. Then the composition of $p$ and $q$ is a polynomial of $R$ defined as the evaluation of $q$ and $p$.

Polynomial.compRingHomdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the composition ring homomorphism of x1 (from the name)

English

Let $x_{1}$ be a polynomial of $R$. Then the composition ring homomorphism of $x_{1}$ is a ring homomorphism of the set of polynomials of $R$ and the set of polynomials of $R$ defined as the evaluation ring homomorphism of $\operatorname{C}$ and $x_{1}$.

Polynomial.evaldefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the evaluation of x1 and p (from the name)

English

Let $x_{1}$ be an element of $R$. Let $p$ be a polynomial of $R$. Then the evaluation of $x_{1}$ and $p$ is an element of $R$ defined as the evaluation of $x_{1}$ and $p$.

Polynomial.evalRingHomdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the evaluation ring homomorphism of x1 (from the name)

English

Let $x_{1}$ be an element of $R$. Then the evaluation ring homomorphism of $x_{1}$ is a ring homomorphism of the set of polynomials of $R$ and $R$ defined as the evaluation ring homomorphism of the identity ring homomorphism of $R$ and $x_{1}$.

Polynomial.eval₂defMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the evaluation of x2 and p (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be an element of $S$. Let $p$ be a polynomial of $R$. Then the evaluation of $x_{2}$ and $p$ is an element of $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{Polynomial\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_Polynomial\_\_Eval\_\_Defs\_\_2849575019\_\_\_hygCtx\_\_\_hyg\_\_2}$, $f$, $x_{2}$ and $p$.

Polynomial.eval₂AddMonoidHomdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the evaluation additive monoid homomorphism of f and x2 (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be an element of $S$. Then the evaluation additive monoid homomorphism of $f$ and $x_{2}$ is an additive monoid homomorphism of the set of polynomials of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{Polynomial\_\_eval\_u2082\_}$ applied to $x_{2}$ and $\mathrm{Polynomial\_\_eval\_u2082\_\_zero}$ applied to $f$ and $x_{2}$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Polynomial\_\_eval\_u2082\_\_add}$ applied to $f$ and $x_{2}$.

Polynomial.eval₂RingHomdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

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

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be an element of $S$. Then the evaluation ring homomorphism of $f$ and $x_{2}$ is a ring homomorphism of the set of polynomials of $R$ and $S$.

Polynomial.eval₂RingHom'defMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

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

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be an element of $S$ such that for all elements $a$ of $R$, $\mathrm{Commute}$ holds for $f$ applied to $a$ and $x_{2}$. Then the evaluation ring homomorphism of $f$ and $x_{2}$ is a ring homomorphism of the set of polynomials of $R$ and $S$.

Polynomial.mapdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the map of f and x2 (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be a polynomial of $R$. Then the map of $f$ and $x_{2}$ is a polynomial of $S$ defined as the evaluation of $\operatorname{X}$ and $x_{2}$.

Polynomial.mapRingHomdefMathlib.Algebra.Polynomial.Eval.Defs, function or constant

Wording

the map ring homomorphism of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map ring homomorphism of $f$ is a ring homomorphism of the set of polynomials of $R$ and the set of polynomials of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{map}$ applied to $f$ and $\mathrm{Polynomial\_\_map\_one}$ applied to $f$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Polynomial\_\_map\_mul}$ applied to $f$, $\mathrm{Polynomial\_\_map\_zero}$ applied to $f$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Polynomial\_\_map\_add}$ applied to $f$.

Mathlib.Algebra.Polynomial.Eval.Degree

Polynomial.mapEquivdefMathlib.Algebra.Polynomial.Eval.Degree, function or constant

Wording

the map equivalence of e (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$. Then the map equivalence of $e$ is a ring isomorphism of the set of polynomials of $R$ and the set of polynomials of $S$.

Mathlib.Algebra.Polynomial.Eval.SMul

Polynomial.levaldefMathlib.Algebra.Polynomial.Eval.SMul, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Then $\operatorname{leval}$ applied to $r$ is a linear map of the set of polynomials of $R$ and $R$.

Mathlib.Algebra.Polynomial.Expand

Polynomial.contractdefMathlib.Algebra.Polynomial.Expand, function or constant

Wording

no wording

English

Let $p$ be an element of $\Natural$. Let $f$ be a polynomial of $R$. Then $\operatorname{contract}$ applied to $p$ and $f$ is a polynomial of $R$ defined as $\FinsetSum {\FinsetrangeMACRoN {(\operatorname{natDegree} (f)+ 1)}}{n}{\operatorname{monomial} (n , \operatorname{coeff} (f , n \times p))}$.

Polynomial.expanddefMathlib.Algebra.Polynomial.Expand, function or constant

Wording

the expand of R and p (from the name)

English

Let $R$ be a set. Let $p$ be a natural number. Then the expand of $R$ and $p$ is an algebra homomorphism of the set of polynomials of $R$ and the set of polynomials of $R$.

Mathlib.Algebra.Polynomial.FieldDivision

Polynomial.divdefMathlib.Algebra.Polynomial.FieldDivision, function or constant

Wording

the quotient of p and q (from the name)

English

Let $p$ and $q$ be polynomials of $R$. Then the quotient of $p$ and $q$ is a polynomial of $R$ defined as the product of $\operatorname{C}$ applied to $\operatorname{inv}$ applied to the leading coefficient of $q$ and $\operatorname{divByMonic}$ applied to $p$ and the product of $q$ and $\operatorname{C}$ applied to $\operatorname{inv}$ applied to the leading coefficient of $q$.

Polynomial.moddefMathlib.Algebra.Polynomial.FieldDivision, function or constant

Wording

no wording

English

Let $p$ and $q$ be polynomials of $R$. Then $\operatorname{mod}$ applied to $p$ and $q$ is a polynomial of $R$ defined as $\operatorname{modByMonic}$ applied to $p$ and the product of $q$ and $\operatorname{C}$ applied to $\operatorname{inv}$ applied to the leading coefficient of $q$.

Mathlib.Algebra.Polynomial.GroupRingAction

MulSemiringActionHom.polynomialdefMathlib.Algebra.Polynomial.GroupRingAction, function or constant

Wording

the polynomial of g (from the name)

English

Let $g$ be a multiplicative semiring action homomorphism of $P$ and $Q$. Then the polynomial of $g$ is a multiplicative semiring action homomorphism of the set of polynomials of $P$ and the set of polynomials of $Q$.

prodXSubSMuldefMathlib.Algebra.Polynomial.GroupRingAction, function or constant

Wording

the product of G (from the docstring)

English

Let $G$ and $R$ be sets. Let $x_{4}$ be an element of $R$. Then the product of $G$ is a polynomial of $R$ defined as $\FinsetProd {\FinsetunivMACRoAC}{g}{(\operatorname{X} - \operatorname{C} (\operatorname{ofQuotientStabilizer} (x_{4} , g)))}$.

Mathlib.Algebra.Polynomial.HasseDeriv

Polynomial.hasseDerivdefMathlib.Algebra.Polynomial.HasseDeriv, function or constant

Wording

the Hasse derivative of k (from the name)

English

Let $k$ be a natural number. Then the Hasse derivative of $k$ is a linear map of the set of polynomials of $R$ and the set of polynomials of $R$ defined as $\operatorname{lsum}$ applied to the function that maps $i$ to the composition of the monomial of $i - k$ and the linear map of $\operatorname{choose}$ applied to $i$ and $k$.

Mathlib.Algebra.Polynomial.Homogenize

Polynomial.homogenizedefMathlib.Algebra.Polynomial.Homogenize, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Let $n$ be a natural number. Then $\operatorname{homogenize}$ applied to $p$ and $n$ is a multivariate polynomial of $\mathrm{Fin}$ applied to $2$ and $R$ defined as $\FinsetSum {\operatorname{antidiagonal} (n)}{\mathrm{kl}}{\operatorname{monomial} (\operatorname{update} (\FinsuppsingleMACRoS {0}{\ProdfstMACRoZ {\mathrm{kl}}}, 1 , \ProdsndMACRoAA {\mathrm{kl}}), \operatorname{coeff} (p , \ProdfstMACRoZ {\mathrm{kl}}))}$.

Polynomial.homogenizeLMdefMathlib.Algebra.Polynomial.Homogenize, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{homogenizeLM}$ applied to $n$ is a linear map of the set of polynomials of $R$ and the set of multivariate polynomials of $\mathrm{Fin}$ applied to $2$ and $R$.

Polynomial.toTupleMvPolynomialdefMathlib.Algebra.Polynomial.Homogenize, function or constant

Wording

the tuple multivariate polynomial of p and x1 (from the name)

English

Let $p$ be a polynomial of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $2$. Then the tuple multivariate polynomial of $p$ and $x_{1}$ is a multivariate polynomial of $\mathrm{Fin}$ applied to $2$ and $R$ defined as $\operatorname{vecCons}$ applied to $\operatorname{homogenize}$ applied to $p$ and the natural degree of $p$, $\operatorname{vecCons}$ applied to the exponentiation of $\operatorname{X}$ applied to $1$ to the natural degree of $p$ and $\operatorname{vecEmpty}$ and $x_{1}$.

Mathlib.Algebra.Polynomial.Identities

Polynomial.binomExpansiondefMathlib.Algebra.Polynomial.Identities, function or constant

Wording

the binom expansion of x1 and y (from the name)

English

Let $f$ be a polynomial of $R$. Let $x_{1}$ and $y$ be elements of $R$. Then the binom expansion of $x_{1}$ and $y$ is an element of $\SubtypeSet {k}{(\EqtMACRoH {\operatorname{eval} (x_{1} + y , f)}{(\operatorname{eval} (x_{1} , f)+ \operatorname{eval} (x_{1} , \operatorname{derivative} (f))\times y + k \times y ^ {2})})}$.

Polynomial.evalSubFactordefMathlib.Algebra.Polynomial.Identities, function or constant

Wording

the evaluation difference factor of x1 and y (from the name)

English

Let $f$ be a polynomial of $R$. Let $x_{1}$ and $y$ be elements of $R$. Then the evaluation difference factor of $x_{1}$ and $y$ is an element of $\SubtypeSet {z}{(\EqtMACRoH {(\operatorname{eval} (x_{1} , f)- \operatorname{eval} (y , f))}{(z \times (x_{1} - y))})}$ defined as the sum of $f$ and the function that maps $i$ and $r$ to $r \times \operatorname{powSubPowFactor} (y , i)$.

Polynomial.powAddExpansiondefMathlib.Algebra.Polynomial.Identities, function or constant

Wording

the power additive expansion of y and n (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Let $n$ be a natural number. Then the power additive expansion of $y$ and $n$ is an element of $\SubtypeSet {k}{(\EqtMACRoH {((x_{1} + y)^ {n})}{(x_{1} ^ {n}+ n \times x_{1} ^ {(n - 1)}\times y + k \times y ^ {2})})}$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{Polynomial\_\_powAddExpansion\_\_\_f}$ applied to $x_{1}$ and $y$.

Polynomial.powSubPowFactordefMathlib.Algebra.Polynomial.Identities, function or constant

Wording

the power difference power factor of y and i (from the name)

English

Let $x_{1}$ and $y$ be elements of $R$. Let $i$ be a natural number. Then the power difference power factor of $y$ and $i$ is an element of $\SubtypeSet {z}{(\EqtMACRoH {(x_{1} ^ {i}- y ^ {i})}{(z \times (x_{1} - y))})}$ defined as $\operatorname{brecOn}$ applied to $i$ and $\mathrm{Polynomial\_\_powSubPowFactor\_\_\_f}$ applied to $x_{1}$ and $y$.

Mathlib.Algebra.Polynomial.Inductions

Polynomial.divXdefMathlib.Algebra.Polynomial.Inductions, function or constant

Wording

the quotient of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the quotient of $p$ is a polynomial of $R$ defined as $\operatorname{ofFinsupp}$ applied to the quotient of the finitely supported function of $p$ and $1$.

Polynomial.divX_homdefMathlib.Algebra.Polynomial.Inductions, function or constant

Wording

the quotient homomorphism (from the name)

English

The quotient homomorphism is an additive monoid homomorphism of the set of polynomials of $R$ and the set of polynomials of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{divX}$ and $\mathrm{Polynomial\_\_divX\_zero}$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Polynomial\_\_divX\_add}$.

Polynomial.recOnHornerdefMathlib.Algebra.Polynomial.Inductions, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Let $M_{0}$ be an element of $M$ applied to $0$. Let $\mathrm{MC}$ be a function from polynomials $p_{2}$ of $R$ and elements $a$ of $R$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{coeff} (p_{2} , 0)}{0}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (a , 0)$ and elements of $M$ applied to $p_{2}$ to elements of $M$ applied to $p_{2} + \operatorname{C} (a)$. Let $\mathrm{MX}$ be a function from polynomials $p_{1}$ of $R$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (p_{1} , 0)$ and elements of $M$ applied to $p_{1}$ to elements of $M$ applied to $p_{1} \times \operatorname{X}$. Then $\operatorname{recOnHorner}$ applied to $p$, $M_{0}$, $p_{2}$, $a$, $\mathrm{MC}$, $p_{1}$ and $\mathrm{MX}$ is an element of $M$ applied to $p$ defined as the function that maps $\mathrm{MC}$, $p_{1}$ and $\mathrm{MX}$ to $\mathrm{Polynomial\_\_recOnHorner\_\_\_unary}$ applied to $M_{0}$, $p_{2}$, $a$, $p$, $\mathrm{MC}$, $p_{1}$ and $\mathrm{MX}$.

Mathlib.Algebra.Polynomial.Laurent

LaurentPolynomialdefMathlib.Algebra.Polynomial.Laurent, type

Wording

Laurent polynomial of R (from the name)

English

Let $R$ be a set. Then a Laurent polynomial of $R$ is an element of the function that maps $R$ to the set of additive monoid algebras of $R$ and $\Integer$.

LaurentPolynomial.CdefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

no wording

English

$\operatorname{C}$ is a ring homomorphism of $R$ and the set of Laurent polynomials of $R$ defined as the single zero ring homomorphism.

LaurentPolynomial.TdefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

no wording

English

Let $n$ be an integer. Then $\operatorname{T}$ applied to $n$ is a Laurent polynomial of $R$ defined as $\operatorname{single}$ applied to $n$ and $1$.

LaurentPolynomial.degreedefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

the degree of f (from the docstring)

English

Let $f$ be a Laurent polynomial of $R$. Then the degree of $f$ is an element of $\mathrm{WithBot}$ applied to $\Integer$ defined as the maximum of the support of the coefficient of $f$.

LaurentPolynomial.eval₂defMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

the evaluation of f and x2 (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Let $x_{2}$ be a unit of $S$. Then the evaluation of $f$ and $x_{2}$ is a ring homomorphism of the set of Laurent polynomials of $R$ and $S$.

LaurentPolynomial.invertdefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

no wording

English

$\operatorname{invert}$ is an algebra isomorphism of the set of Laurent polynomials of $R$ and the set of Laurent polynomials of $R$ defined as the domain congruence of the negation of $\Integer$.

LaurentPolynomial.levaldefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{4}$ be a unit of $S$. Then $\operatorname{leval}$ applied to $R$ and $x_{4}$ is a linear map of the set of Laurent polynomials of $R$ and $S$.

LaurentPolynomial.smevaldefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

no wording

English

Let $f$ be a Laurent polynomial of $R$. Let $x_{4}$ be an element of $\UnitsMACRoAO {S}$. Then $\operatorname{smeval}$ applied to $f$ and $x_{4}$ is an element of $S$ defined as the sum of the coefficient of $f$ and the function that maps $n$ and $r$ to $\HSMulhSMulMACRoAL {r}{\operatorname{val} (x_{4} ^ {n})}$.

LaurentPolynomial.truncdefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

the truncation (from the name)

English

The truncation is an additive monoid homomorphism of the set of Laurent polynomials of $R$ and the set of polynomials of $R$.

Polynomial.toLaurentdefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

no wording

English

$\operatorname{toLaurent}$ is a ring homomorphism of the set of polynomials of $R$ and the set of Laurent polynomials of $R$ defined as the composition of the map domain ring homomorphism of $R$ and the additive monoid homomorphism of the integer and the ring homomorphism of the finitely supported function isomorphism of $R$.

Polynomial.toLaurentAlgdefMathlib.Algebra.Polynomial.Laurent, function or constant

Wording

the Laurent algebra (from the name)

English

The Laurent algebra is an algebra homomorphism of the set of polynomials of $R$ and the set of Laurent polynomials of $R$ defined as the composition of the map domain algebra homomorphism of the additive monoid homomorphism of the integer and the algebra homomorphism of the finitely supported function isomorphism algebra of $R$.

Mathlib.Algebra.Polynomial.Lifts

Polynomial.liftsdefMathlib.Algebra.Polynomial.Lifts, function or constant

Wording

the lift of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the lift of $f$ is a subsemiring of the set of polynomials of $S$ defined as the range of the map ring homomorphism of $f$.

Polynomial.liftsRingdefMathlib.Algebra.Polynomial.Lifts, function or constant

Wording

the lift ring of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the lift ring of $f$ is a subring of the set of polynomials of $S$ defined as the range of the map ring homomorphism of $f$.

Mathlib.Algebra.Polynomial.Mirror

Polynomial.mirrordefMathlib.Algebra.Polynomial.Mirror, function or constant

Wording

the mirror of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the mirror of $p$ is a polynomial of $R$ defined as the product of the reverse of $p$ and $\operatorname{X} ^ {\operatorname{natTrailingDegree} (p)}$.

Mathlib.Algebra.Polynomial.Module.AEval

LinearEquiv.ofAEvaldefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

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

English

Let $a$ be an element of $A$. Let $f$ be a linear equivalence of $M$ and $N$ such that for all elements $m$ of $M$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {a}{m})}{\HSMulhSMulMACRoAL {\operatorname{X}}{f (m)}}$. Then the linear equivalence of $a$ and $f$ is a linear equivalence of the set of evaluations of $M$ and $a$ and $N$.

LinearMap.ofAEvaldefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

the linear map of a and f (from the name)

English

Let $a$ be an element of $A$. Let $f$ be a linear map of $M$ and $N$ such that for all elements $m$ of $M$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {a}{m})}{\HSMulhSMulMACRoAL {\operatorname{X}}{f (m)}}$. Then the linear map of $a$ and $f$ is a linear map of the set of evaluations of $M$ and $a$ and $N$.

Module.AEvaldefMathlib.Algebra.Polynomial.Module.AEval, type

Wording

evaluation of M and x6 (from the name)

English

Let $R$ and $M$ be sets. Let $x_{6}$ be an element of $A$. Then an evaluation of $M$ and $x_{6}$ is an element of the function that maps $R$, $M$ and $x_{6}$ to $M$.

Module.AEval'defMathlib.Algebra.Polynomial.Module.AEval, type

Wording

evaluation of x3 (from the name)

English

Let $x_{3}$ be a linear map of $M$ and $M$. Then an evaluation of $x_{3}$ is an element of the function that maps $x_{3}$ to the set of evaluations of $M$ and $x_{3}$.

Module.AEval'.ofdefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

no wording

English

Let $x_{3}$ be a linear map of $M$ and $M$. Then $\operatorname{of}$ applied to $x_{3}$ is a linear equivalence of $M$ and the set of evaluations of $x_{3}$ defined as $\operatorname{of}$ applied to $R$, $M$ and $x_{3}$.

Module.AEval.equiv_mapSubmoduledefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

the equivalence map submodule of a and p (from the name)

English

Let $a$ be an element of $A$. Let $p$ be a submodule of $R$ and $M$ such that $\MembershipmemMACRoT {\operatorname{invtSubmodule} (\operatorname{lsmul} (R , R , M , a))}{p}$. Then the equivalence map submodule of $a$ and $p$ is a linear equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{mapSubmodule} (R , M , a , p)}{x_{7}})}$.

Module.AEval.mapSubmoduledefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

the map submodule of a (from the name)

English

Let $R$ and $M$ be sets. Let $a$ be an element of $A$. Then the map submodule of $a$ is an order isomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{invtSubmodule} (\operatorname{lsmul} (R , R , M , a))}{x_{6}})}$ and the set of submodules of the set of polynomials of $R$ and the set of evaluations of $M$ and $a$.

Module.AEval.ofdefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Let $a$ be an element of $A$. Then $\operatorname{of}$ applied to $R$, $M$ and $a$ is a linear equivalence of $M$ and the set of evaluations of $M$ and $a$ defined as the identity map of $R$ and $M$.

Module.AEval.restrict_equiv_mapSubmoduledefMathlib.Algebra.Polynomial.Module.AEval, function or constant

Wording

no wording

English

Let $a$ be an element of $A$. Let $p$ be a submodule of $R$ and $M$ such that $\MembershipmemMACRoT {\operatorname{invtSubmodule} (\operatorname{lsmul} (R , R , M , a))}{p}$. Then $\mathrm{Module\_\_AEval\_\_restrict\_equiv\_mapSubmodule}$ applied to $a$, $p$ and $\mathrm{hp}$ is a linear equivalence of the set of evaluations of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\operatorname{restrict}$ applied to $\operatorname{lsmul}$ applied to $R$, $R$, $M$ and $a$ and $\mathrm{hp}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{mapSubmodule} (R , M , a , p)}{x_{7}})}$.

Mathlib.Algebra.Polynomial.Module.Basic

PolynomialModulestructureMathlib.Algebra.Polynomial.Module.Basic, type

Wording

polynomial module of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the polynomial modules of $R$ and $M$ are a basic type.

PolynomialModule.coeffdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the coefficient of self (from the name)

English

Let $\mathrm{self}$ be a polynomial module of $R$ and $M$. Then the coefficient of $\mathrm{self}$ is an element of $\FinsuppMACRoQ {\Natural}{M}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

PolynomialModule.coeffAddEquivdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the coefficient additive equivalence (from the name)

English

The coefficient additive equivalence is an additive equivalence of the set of polynomial modules of $R$ and $M$ and $\FinsuppMACRoQ {\Natural}{M}$ defined as the additive equivalence of the coefficient equivalence of $R$.

PolynomialModule.coeffEquivdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the coefficient equivalence of R (from the name)

English

Let $R$ be a set. Then the coefficient equivalence of $R$ is an equivalence from the set of polynomial modules of $R$ and $M$ to $\FinsuppMACRoQ {\Natural}{M}$.

PolynomialModule.coeffLinearEquivdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the coefficient linear equivalence of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the coefficient linear equivalence of $R$ and $S$ is a linear equivalence of the set of polynomial modules of $R$ and $M$ and $\FinsuppMACRoQ {\Natural}{M}$ defined as the linear equivalence of $S$ and the coefficient additive equivalence.

PolynomialModule.compdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the composition of p (from the docstring)

English

Let $p$ be a polynomial of $R$. Then the composition of $p$ is a linear map of the set of polynomial modules of $R$ and $M$ and the set of polynomial modules of $R$ and $M$ defined as the composition of $\operatorname{restrictScalars}$ applied to $R$ and the evaluation of $p$ and the image of the set of polynomials of $R$ and $\operatorname{lsingle}$ applied to $R$ and $0$.

PolynomialModule.equivPolynomialdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the equivalence polynomial (from the name)

English

The equivalence polynomial is a linear equivalence of the set of polynomial modules of $R$ and $S$ and the set of polynomials of $S$.

PolynomialModule.equivPolynomialSelfdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the equivalence polynomial self (from the name)

English

The equivalence polynomial self is a linear equivalence of the set of polynomial modules of $R$ and $R$ and the set of polynomials of $R$.

PolynomialModule.evaldefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the evaluation of r (from the name)

English

Let $r$ be an element of $R$. Then the evaluation of $r$ is a linear map of the set of polynomial modules of $R$ and $M$ and $M$.

PolynomialModule.lsingledefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $i$ be a natural number. Then $\operatorname{lsingle}$ applied to $R$ and $i$ is a linear map of $M$ and the set of polynomial modules of $R$ and $M$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $R$ and $R$ and $\operatorname{lsingle}$ applied to $i$.

PolynomialModule.mapdefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

the image of f and #2 (from the docstring)

English

Let $\mathrm{R'}$ be a set. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Then the image of $\mathrm{R'}$ and $f$ is a linear map of the set of polynomial modules of $R$ and $M$ and the set of polynomial modules of $\mathrm{R'}$ and $\mathrm{M'}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the coefficient linear equivalence of $\mathrm{R'}$ and $R$ and the composition of the linear map of $f$ and $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $R$ and $R$.

PolynomialModule.singledefMathlib.Algebra.Polynomial.Module.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Let $m$ be an element of $M$. Then $\operatorname{single}$ applied to $R$, $n$ and $m$ is a polynomial module of $R$ and $M$ defined as $\operatorname{ofCoeff}$ applied to $R$ and $\FinsuppsingleMACRoS {n}{m}$.

Mathlib.Algebra.Polynomial.Module.TensorProduct

PolynomialModule.polynomialTensorProductLEquivPolynomialModuledefMathlib.Algebra.Polynomial.Module.TensorProduct, function or constant

Wording

the polynomial tensor product equivalence polynomial module of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the polynomial tensor product equivalence polynomial module of $R$ and $M$ is a linear equivalence of the set of tensor products of the set of polynomials of $R$ and $M$ and the set of polynomial modules of $R$ and $M$.

Mathlib.Algebra.Polynomial.Monic

Polynomial.MonicDegreeEqdefMathlib.Algebra.Polynomial.Monic, type

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$ is an element of the function that maps $R$ and $n$ to $\SubtypeSet {p}{\mathrm{and} (\EqtMACRoH {\operatorname{coeff} (p , n)}{1}, \mathrm{forall} (\Natural , \lambda i . \mathrm{if} (\mathrm{Gt} (i , n), \EqtMACRoH {\operatorname{coeff} (p , i)}{0})))}$.

Polynomial.MonicDegreeEq.mapdefMathlib.Algebra.Polynomial.Monic, function or constant

Wording

the map of p and f (from the name)

English

Let $p$ be an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $p$ and $f$ is an element of $\operatorname{MonicDegreeEq}$ applied to $S$ and $n$ defined as the map of $f$ and $p$.

Polynomial.MonicDegreeEq.mkdefMathlib.Algebra.Polynomial.Monic, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$ such that $p$ is monic and the natural degree of $p$ is equal to $n$. Then $\operatorname{mk}$ applied to $p$, $\mathrm{hp}$ and $\mathrm{hp'}$ is an element of $\operatorname{MonicDegreeEq}$ applied to $R$ and $n$ defined as $p$.

Mathlib.Algebra.Polynomial.OfFn

Polynomial.ofFndefMathlib.Algebra.Polynomial.OfFn, function or constant

Wording

the polynomial of n (from the name)

English

Let $n$ be a natural number. Then the polynomial of $n$ is a linear map of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$ and the set of polynomials of $R$.

Polynomial.toFndefMathlib.Algebra.Polynomial.OfFn, function or constant

Wording

the function of n (from the name)

English

Let $n$ be a natural number. Then the function of $n$ is a linear map of the set of polynomials of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$ defined as the product of the function that maps $i$ to $\operatorname{lcoeff}$ applied to $R$ and $\operatorname{val}$ applied to $i$.

Mathlib.Algebra.Polynomial.Reverse

Polynomial.reflectdefMathlib.Algebra.Polynomial.Reverse, function or constant

Wording

no wording

English

Let $N$ be a natural number. Let $x_{1}$ be a polynomial of $R$. Then $\operatorname{reflect}$ applied to $N$ and $x_{1}$ is a polynomial of $R$.

Polynomial.revAtdefMathlib.Algebra.Polynomial.Reverse, function or constant

Wording

no wording

English

Let $N$ be a natural number. Then $\operatorname{revAt}$ applied to $N$ is an embedding of $\Natural$ and $\Natural$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to $\iteMACRoG {\mathrm{Leq} (i , N)}{(N - i)}{i}$ and $\mathrm{Polynomial\_\_revAtFun\_inj}$.

Polynomial.revAtFundefMathlib.Algebra.Polynomial.Reverse, function or constant

Wording

no wording

English

Let $N$ and $i$ be natural numbers. Then $\operatorname{revAtFun}$ applied to $N$ and $i$ is a natural number defined as $\iteMACRoG {\mathrm{Leq} (i , N)}{(N - i)}{i}$.

Polynomial.reversedefMathlib.Algebra.Polynomial.Reverse, function or constant

Wording

the reverse of f (from the docstring)

English

Let $f$ be a polynomial of $R$. Then the reverse of $f$ is a polynomial of $R$ defined as $\operatorname{reflect}$ applied to the natural degree of $f$ and $f$.

Mathlib.Algebra.Polynomial.RingDivision

Polynomial.divByMonicHomdefMathlib.Algebra.Polynomial.RingDivision, function or constant

Wording

the quotient by monic homomorphism of q (from the name)

English

Let $q$ be a polynomial of $R$. Then the quotient by monic homomorphism of $q$ is a linear map of the set of polynomials of $R$ and the set of polynomials of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $p$ to $\operatorname{divByMonic}$ applied to $p$ and $q$ and $\mathrm{Polynomial\_\_add\_divByMonic}$ and $\mathrm{Polynomial\_\_smul\_divByMonic}$.

Polynomial.modByMonicHomdefMathlib.Algebra.Polynomial.RingDivision, function or constant

Wording

no wording

English

Let $q$ be a polynomial of $R$. Then $\operatorname{modByMonicHom}$ applied to $q$ is a linear map of the set of polynomials of $R$ and the set of polynomials of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $p$ to $\operatorname{modByMonic}$ applied to $p$ and $q$ and $\mathrm{Polynomial\_\_add\_modByMonic}$ and $\mathrm{Polynomial\_\_smul\_modByMonic}$.

Mathlib.Algebra.Polynomial.Roots

Polynomial.arootsdefMathlib.Algebra.Polynomial.Roots, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $T$. Let $S$ be a set. Then $\operatorname{aroots}$ applied to $p$ and $S$ is a multiset of $S$ defined as the root of the map of the algebra map of $T$ and $S$ and $p$.

Polynomial.nthRootsdefMathlib.Algebra.Polynomial.Roots, function or constant

Wording

the nth root of n and a (from the name)

English

Let $n$ be a natural number. Let $a$ be an element of $R$. Then the nth root of $n$ and $a$ is a multiset of $R$ defined as the root of $\operatorname{X} ^ {n}- \operatorname{C} (a)$.

Polynomial.nthRootsFinsetdefMathlib.Algebra.Polynomial.Roots, function or constant

Wording

the nth root finite set of n and a (from the name)

English

Let $n$ be a natural number. Let $a$ be an element of $R$. Then the nth root finite set of $n$ and $a$ is a finite set of $R$ defined as the finite set of the nth root of $n$ and $a$.

Polynomial.rootSetdefMathlib.Algebra.Polynomial.Roots, function or constant

Wording

the root set of p and S (from the name)

English

Let $p$ be a polynomial of $T$. Let $S$ be a set. Then the root set of $p$ and $S$ is an element of $\wp S$ defined as the finite set of $\operatorname{aroots}$ applied to $p$ and $S$.

Polynomial.rootsdefMathlib.Algebra.Polynomial.Roots, function or constant

Wording

the root of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the root of $p$ is a multiset of $R$.

Mathlib.Algebra.Polynomial.RuleOfSigns

Polynomial.signVariationsdefMathlib.Algebra.Polynomial.RuleOfSigns, function or constant

Wording

the sign variation of P (from the name)

English

Let $P$ be a polynomial of $R$. Then the sign variation of $P$ is a natural number defined as the sign variation of the coefficient list of $P$.