Definitions: Mathlib.Algebra, part 6 of 17

AddEquiv.mulOpdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the multiplicative opposite (from the name)

English

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

AddEquiv.mulUnopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the multiplicative opposite (from the name)

English

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

AddEquiv.neg'defMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the negation of G (from the name)

English

Let $G$ be a set. Then the negation of $G$ is an additive equivalence of $G$ and the set of additive opposites of $G$.

AddEquiv.opdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of additive equivalences of $x$ and $x_{1}$ to the set of additive equivalences of the set of additive opposites of $x$ and the set of additive opposites of $x_{1}$.

AddEquiv.opOpdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite opposite of M (from the name)

English

Let $M$ be a set. Then the opposite opposite of $M$ is an additive equivalence of $M$ and the set of additive opposites of the set of additive opposites of $M$.

AddEquiv.unopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

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

AddHom.fromOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

no wording

English

Let $f$ be an additive homomorphism of $M$ and $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\mathrm{AddCommute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then $\operatorname{fromOpposite}$ applied to $f$ and $\mathrm{hf}$ is an additive homomorphism of the set of additive opposites of $M$ and $N$.

AddHom.mulOpdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the multiplicative opposite (from the name)

English

The multiplicative opposite is an equivalence from the set of additive homomorphisms of $M$ and $N$ to the set of additive homomorphisms of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $N$.

AddHom.mulUnopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the multiplicative opposite (from the name)

English

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

AddHom.opdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of additive homomorphisms of $M$ and $N$ to the set of additive homomorphisms of the set of additive opposites of $M$ and the set of additive opposites of $N$.

AddHom.toOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite of f and hf (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\mathrm{AddCommute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then the opposite of $f$ and $\mathrm{hf}$ is an additive homomorphism of $M$ and the set of additive opposites of $N$.

AddHom.unopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of additive homomorphisms of the set of additive opposites of $M$ and the set of additive opposites of $N$ to the set of additive homomorphisms of $M$ and $N$ defined as the inverse of the opposite.

AddMonoidHom.fromOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\mathrm{AddCommute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then $\operatorname{fromOpposite}$ applied to $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of additive opposites of $M$ and $N$.

AddMonoidHom.mulOpdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the multiplicative opposite (from the name)

English

The multiplicative opposite is an equivalence from the set of additive monoid homomorphisms of $M$ and $N$ to the set of additive monoid homomorphisms of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $N$.

AddMonoidHom.mulUnopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the multiplicative opposite (from the name)

English

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

AddMonoidHom.opdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of additive monoid homomorphisms of $M$ and $N$ to the set of additive monoid homomorphisms of the set of additive opposites of $M$ and the set of additive opposites of $N$.

AddMonoidHom.toOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite of f and hf (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\mathrm{AddCommute}$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$. Then the opposite of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of $M$ and the set of additive opposites of $N$.

AddMonoidHom.unopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of additive monoid homomorphisms of the set of additive opposites of $M$ and the set of additive opposites of $N$ to the set of additive monoid homomorphisms of $M$ and $N$ defined as the inverse of the opposite.

AddOpposite.opAddEquivdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite additive equivalence (from the name)

English

The opposite additive equivalence is an additive equivalence of $M$ and the set of additive opposites of $M$.

AddOpposite.opMulEquivdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite multiplicative equivalence (from the name)

English

The opposite multiplicative equivalence is a multiplicative equivalence of $x$ and the set of additive opposites of $x$.

MonoidHom.fromOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

no wording

English

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

MonoidHom.opdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of monoid homomorphisms of $M$ and $N$ to the set of monoid homomorphisms of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $N$.

MonoidHom.toOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite of f and hf (from the name)

English

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

MonoidHom.unopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of monoid homomorphisms of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $N$ to the set of monoid homomorphisms of $M$ and $N$ defined as the inverse of the opposite.

MulEquiv.inv'defMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the inverse of G (from the name)

English

Let $G$ be a set. Then the inverse of $G$ is a multiplicative equivalence of $G$ and the set of multiplicative opposites of $G$.

MulEquiv.opdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

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

MulEquiv.opOpdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite opposite of M (from the name)

English

Let $M$ be a set. Then the opposite opposite of $M$ is a multiplicative equivalence of $M$ and the set of multiplicative opposites of the set of multiplicative opposites of $M$.

MulEquiv.unopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

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

MulHom.fromOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

no wording

English

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

MulHom.opdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of multiplicative homomorphisms of $M$ and $N$ to the set of multiplicative homomorphisms of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $N$.

MulHom.toOppositedefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite of f and hf (from the name)

English

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

MulHom.unopdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite (from the name)

English

The opposite is an equivalence from the set of multiplicative homomorphisms of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $N$ to the set of multiplicative homomorphisms of $M$ and $N$ defined as the inverse of the opposite.

MulOpposite.opAddEquivdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite additive equivalence (from the name)

English

The opposite additive equivalence is an additive equivalence of $x$ and the set of multiplicative opposites of $x$.

MulOpposite.opMulEquivdefMathlib.Algebra.Group.Equiv.Opposite, function or constant

Wording

the opposite multiplicative equivalence (from the name)

English

The opposite multiplicative equivalence is a multiplicative equivalence of $M$ and the set of multiplicative opposites of $M$.

Mathlib.Algebra.Group.Equiv.TypeTags

AddEquiv.additiveMultiplicativedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the additive multiplicative of G (from the name)

English

Let $G$ be a set. Then the additive multiplicative of $G$ is an additive equivalence of $\mathrm{Additive}$ applied to the set of multiplicatives of $G$ and $G$ defined as $\operatorname{toAdditiveLeft}$ applied to the identity map of the set of multiplicatives of $G$.

AddEquiv.funAdditivedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

Let $x$ and $G$ be sets. Then $\operatorname{funAdditive}$ applied to $x$ and $G$ is an additive equivalence of $\mathrm{Additive}$ applied to the set of functions from elements of $x$ to elements of $G$ and the set of functions from elements of $x$ to elements of $\mathrm{Additive}$ applied to $G$ defined as $\operatorname{piAdditive}$ applied to the function that maps $x_{2}$ to $G$.

AddEquiv.piAdditivedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

Let $K$ be a function from elements of $x$ to sets. Then $\operatorname{piAdditive}$ applied to $K$ is an additive equivalence of $\mathrm{Additive}$ applied to the set of functions from elements $i$ of $x$ to elements of $K$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $\mathrm{Additive}$ applied to $K$ applied to $i_{1}$.

AddEquiv.prodAdditivedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

Let $G$ and $H$ be sets. Then $\operatorname{prodAdditive}$ applied to $G$ and $H$ is an additive equivalence of $\mathrm{Additive}$ applied to $\mathrm{Prod}$ applied to $G$ and $H$ and $\mathrm{Prod}$ applied to $\mathrm{Additive}$ applied to $G$ and $\mathrm{Additive}$ applied to $H$.

AddEquiv.toMultiplicativedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the multiplicative (from the name)

English

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

AddEquiv.toMultiplicativeLeftdefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the left multiplicative (from the name)

English

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

AddEquiv.toMultiplicativeRightdefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the right multiplicative (from the name)

English

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

MulEquiv.addMonoidEnddefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the additive monoid end of A (from the name)

English

Let $A$ be a set. Then the additive monoid end of $A$ is a multiplicative equivalence of the set of ends of $A$ and the set of ends of the set of multiplicatives of $A$.

MulEquiv.funMultiplicativedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the function multiplicative of x and G (from the name)

English

Let $x$ and $G$ be sets. Then the function multiplicative of $x$ and $G$ is a multiplicative equivalence of the set of multiplicatives of the set of functions from elements of $x$ to elements of $G$ and the set of functions from elements of $x$ to multiplicatives of $G$ defined as the product multiplicative of the function that maps $x_{2}$ to $G$.

MulEquiv.monoidEnddefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the monoid end of M (from the name)

English

Let $M$ be a set. Then the monoid end of $M$ is a multiplicative equivalence of the set of ends of $M$ and the set of ends of $\mathrm{Additive}$ applied to $M$.

MulEquiv.multiplicativeAdditivedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

Let $H$ be a set. Then $\operatorname{multiplicativeAdditive}$ applied to $H$ is a multiplicative equivalence of the set of multiplicatives of $\mathrm{Additive}$ applied to $H$ and $H$ defined as $\operatorname{toMultiplicativeLeft}$ applied to the identity map of $\mathrm{Additive}$ applied to $H$.

MulEquiv.piMultiplicativedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the product multiplicative of K (from the name)

English

Let $K$ be a function from elements of $x$ to sets. Then the product multiplicative of $K$ is a multiplicative equivalence of the set of multiplicatives of the set of functions from elements $i$ of $x$ to elements of $K$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to multiplicatives of $K$ applied to $i_{1}$.

MulEquiv.prodMultiplicativedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

the product multiplicative of G and H (from the name)

English

Let $G$ and $H$ be sets. Then the product multiplicative of $G$ and $H$ is a multiplicative equivalence of the set of multiplicatives of $\mathrm{Prod}$ applied to $G$ and $H$ and $\mathrm{Prod}$ applied to the set of multiplicatives of $G$ and the set of multiplicatives of $H$.

MulEquiv.toAdditivedefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

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

MulEquiv.toAdditiveLeftdefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

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

MulEquiv.toAdditiveRightdefMathlib.Algebra.Group.Equiv.TypeTags, function or constant

Wording

no wording

English

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

Mathlib.Algebra.Group.Even

EvendefMathlib.Algebra.Group.Even, predicate

Wording

no wording

English

Let $a$ be an element of $x$. Then $\mathrm{Even}$ holds for $a$, if there exists an element $r$ of $x$, such that $\EqtMACRoH {a}{r + r}$.

IsSquaredefMathlib.Algebra.Group.Even, predicate

Wording

a is a square (by hand)

English

Let $a$ be an element of $x$. Then $a$ is a square, if there exists an element $r$ of $x$, such that $\EqtMACRoH {a}{r \times r}$.

Mathlib.Algebra.Group.EvenFunction

Function.EvendefMathlib.Algebra.Group.EvenFunction, predicate

Wording

f is even (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is even, if for all elements $a$ of $x$, $\EqtMACRoH {f (\operatorname{neg} (a))}{f (a)}$.

Function.OdddefMathlib.Algebra.Group.EvenFunction, predicate

Wording

f is odd (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is odd, if for all elements $a$ of $x$, $\EqtMACRoH {f (\operatorname{neg} (a))}{\operatorname{neg} (f (a))}$.

Mathlib.Algebra.Group.Finsupp

Finsupp.addEquivFunOnFinitedefMathlib.Algebra.Group.Finsupp, function or constant

Wording

no wording

English

$\operatorname{addEquivFunOnFinite}$ is an additive equivalence of $\FinsuppMACRoQ {x_{1}}{M}$ and the set of functions from elements of $x_{1}$ to elements of $M$.

Finsupp.applyAddHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{applyAddHom}$ applied to $a$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $M$.

Finsupp.coeFnAddHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the coercion function additive homomorphism (from the name)

English

The coercion function additive homomorphism is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and the set of functions from elements of $x$ to elements of $M$.

Finsupp.embDomain.addMonoidHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be an embedding of $x$ and $F$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {F}{M}$.

Finsupp.eraseAddHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{eraseAddHom}$ applied to $a$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{M}$.

Finsupp.mapRange.addEquivdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the additive equivalence of #1 (from the name)

English

Let $\mathrm{em'}$ be an additive equivalence of $M$ and $N$. Then the additive equivalence of $\mathrm{em'}$ is an additive equivalence of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{N}$.

Finsupp.mapRange.addMonoidHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{N}$.

Finsupp.mapRange.zeroHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the zero homomorphism of f (from the name)

English

Let $f$ be a zero homomorphism of $M$ and $N$. Then the zero homomorphism of $f$ is a zero homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{N}$.

Finsupp.singleAddHomdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the single additive homomorphism of a (from the name)

English

Let $a$ be an element of $x$. Then the single additive homomorphism of $a$ is an additive monoid homomorphism of $M$ and $\FinsuppMACRoQ {x}{M}$.

Finsupp.uniqueAddEquivdefMathlib.Algebra.Group.Finsupp, function or constant

Wording

the unique additive equivalence of i (from the name)

English

Let $i$ be an element of $x$. Then the unique additive equivalence of $i$ is an additive equivalence of $\FinsuppMACRoQ {x}{M}$ and $M$.

Mathlib.Algebra.Group.ForwardDiff

fwdDiffdefMathlib.Algebra.Group.ForwardDiff, function or constant

Wording

no wording

English

Let $h$ and $x_{2}$ be elements of $M$. Let $f$ be a function from elements of $M$ to elements of $G$. Then $\mathrm{fwdDiff}$ applied to $h$, $f$ and $x_{2}$ is an element of $G$ defined as $f (x_{2} + h)- f (x_{2})$.

fwdDiff_aux.fwdDiffₗdefMathlib.Algebra.Group.ForwardDiff, function or constant

Wording

no wording

English

Let $M$ and $G$ be sets. Let $h$ be an element of $M$. Then $\mathrm{fwdDiff\_aux\_\_fwdDiff\_u2097\_}$ applied to $M$, $G$ and $h$ is an end of $\Integer$ and the set of functions from elements of $M$ to elements of $G$.

fwdDiff_aux.shiftₗdefMathlib.Algebra.Group.ForwardDiff, function or constant

Wording

the shift of h (from the name)

English

Let $M$ and $G$ be sets. Let $h$ be an element of $M$. Then the shift of $h$ is an end of $\Integer$ and the set of functions from elements of $M$ to elements of $G$ defined as $\mathrm{fwdDiff\_aux\_\_fwdDiff\_u2097\_} (M , G , h)+ 1$.

Mathlib.Algebra.Group.FunLike

FunLike.coeAddHomdefMathlib.Algebra.Group.FunLike, function or constant

Wording

the coercion additive homomorphism of x and x1 (from the name)

English

Let $F$, $x$ and $x_{1}$ be sets. Then the coercion additive homomorphism of $x$ and $x_{1}$ is an additive homomorphism of $F$ and the set of functions from elements of $x$ to elements of $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $f$ to $\operatorname{coe}$ applied to $f$ and $\mathrm{FunLike\_\_coe\_add}$.

FunLike.coeAddMonoidHomdefMathlib.Algebra.Group.FunLike, function or constant

Wording

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

English

Let $F$, $x$ and $x_{1}$ be sets. Then the coercion additive monoid homomorphism of $x$ and $x_{1}$ is an additive monoid homomorphism of $F$ and the set of functions from elements of $x$ to elements of $x_{1}$.

FunLike.coeMonoidHomdefMathlib.Algebra.Group.FunLike, function or constant

Wording

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

English

Let $F$, $x$ and $x_{1}$ be sets. Then the coercion monoid homomorphism of $x$ and $x_{1}$ is a monoid homomorphism of $F$ and the set of functions from elements of $x$ to elements of $x_{1}$.

FunLike.coeMulHomdefMathlib.Algebra.Group.FunLike, function or constant

Wording

the coercion multiplicative homomorphism of x and x1 (from the name)

English

Let $F$, $x$ and $x_{1}$ be sets. Then the coercion multiplicative homomorphism of $x$ and $x_{1}$ is a multiplicative homomorphism of $F$ and the set of functions from elements of $x$ to elements of $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $f$ to $\operatorname{coe}$ applied to $f$ and $\mathrm{FunLike\_\_coe\_mul}$.

Mathlib.Algebra.Group.Graph

AddMonoidHom.graphdefMathlib.Algebra.Group.Graph, function or constant

Wording

the graph of f (from the docstring)

English

Let $f$ be an additive monoid homomorphism of $G$ and $H$. Then the graph of $f$ is an additive subgroup of $\mathrm{Prod}$ applied to $G$ and $H$.

AddMonoidHom.mgraphdefMathlib.Algebra.Group.Graph, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $G$ and $H$. Then $\operatorname{mgraph}$ applied to $f$ is an additive submonoid of $\mathrm{Prod}$ applied to $G$ and $H$.

MonoidHom.graphdefMathlib.Algebra.Group.Graph, function or constant

Wording

the graph of f (from the docstring)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Then the graph of $f$ is a subgroup of $\mathrm{Prod}$ applied to $G$ and $H$.

MonoidHom.mgraphdefMathlib.Algebra.Group.Graph, function or constant

Wording

no wording

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Then $\operatorname{mgraph}$ applied to $f$ is a submonoid of $\mathrm{Prod}$ applied to $G$ and $H$.

Mathlib.Algebra.Group.Hom.Basic

AddMonoidHom.ofMapAddNegdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the additive monoid homomorphism of f and map_sub (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $H$ such that for all elements $a$ and $b$ of $G$, $\EqtMACRoH {f (a + \operatorname{neg} (b))}{f (a)+ \operatorname{neg} (f (b))}$. Then the additive monoid homomorphism of $f$ and $\mathrm{map\_sub}$ is an additive monoid homomorphism of $G$ and $H$.

AddMonoidHom.ofMapSubdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the additive monoid homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $H$ such that for all elements $x_{2}$ and $y$ of $G$, $\EqtMACRoH {f (x_{2} - y)}{f (x_{2})- f (y)}$. Then the additive monoid homomorphism of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of $G$ and $H$.

MonoidHom.ofMapDivdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the monoid homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $H$ such that for all elements $x_{2}$ and $y$ of $G$, $\EqtMACRoH {f (\frac{ x_{2}}{y})}{\frac{ f (x_{2})}{f (y)}}$. Then the monoid homomorphism of $f$ and $\mathrm{hf}$ is a monoid homomorphism of $G$ and $H$.

MonoidHom.ofMapMulInvdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the monoid homomorphism of f and map_div (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $H$ such that for all elements $a$ and $b$ of $G$, $\EqtMACRoH {f (a \times \operatorname{inv} (b))}{f (a)\times \operatorname{inv} (f (b))}$. Then the monoid homomorphism of $f$ and $\mathrm{map\_div}$ is a monoid homomorphism of $G$ and $H$.

invMonoidHomdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the inverse monoid homomorphism (from the name)

English

The inverse monoid homomorphism is a monoid homomorphism of $x$ and $x$.

negAddMonoidHomdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the negation additive monoid homomorphism (from the name)

English

The negation additive monoid homomorphism is an additive monoid homomorphism of $x$ and $x$.

nsmulAddMonoidHomdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the natural multiple additive monoid homomorphism of n (from the name)

English

Let $n$ be a natural number. Then the natural multiple additive monoid homomorphism of $n$ is an additive monoid homomorphism of $x$ and $x$.

powMonoidHomdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the power monoid homomorphism of n (from the name)

English

Let $n$ be a natural number. Then the power monoid homomorphism of $n$ is a monoid homomorphism of $x$ and $x$.

zpowGroupHomdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the integer power group homomorphism of n (from the name)

English

Let $n$ be an integer. Then the integer power group homomorphism of $n$ is a monoid homomorphism of $x$ and $x$.

zsmulAddGroupHomdefMathlib.Algebra.Group.Hom.Basic, function or constant

Wording

the integer multiple additive group homomorphism of n (from the name)

English

Let $n$ be an integer. Then the integer multiple additive group homomorphism of $n$ is an additive monoid homomorphism of $x$ and $x$.

Mathlib.Algebra.Group.Hom.CompTypeclasses

MonoidHom.CompTripleclassMathlib.Algebra.Group.Hom.CompTypeclasses, predicate

Wording

no wording

English

Let $x_{3}$ be a monoid homomorphism of $M$ and $N$. Let $x_{4}$ be a monoid homomorphism of $N$ and $P$. Let $x_{5}$ be an element of $\mathrm{outParam}$ applied to the set of monoid homomorphisms of $M$ and $P$. Then we can say that $\operatorname{CompTriple}$ holds for $x_{3}$, $x_{4}$ and $x_{5}$.

MonoidHom.CompTriple.IsIdclassMathlib.Algebra.Group.Hom.CompTypeclasses, predicate

Wording

x1 is a identity (from the name)

English

Let $x_{1}$ be a monoid homomorphism of $M$ and $M$. Then we can say that $x_{1}$ is an identity.

Mathlib.Algebra.Group.Hom.Defs

AddHomstructureMathlib.Algebra.Group.Hom.Defs, type

Wording

additive homomorphism of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the additive homomorphisms of $M$ and $N$ are a basic type.

AddHom.compdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be an additive homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be an additive homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is an additive homomorphism of $M$ and $P$.

AddHom.copydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

AddHom.iddefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the identity map of M (from the docstring)

English

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

AddHom.inversedefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

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

AddHom.toFundefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

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

English

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

AddHomClassclassMathlib.Algebra.Group.Hom.Defs, predicate

Wording

no wording

English

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

AddHomClass.toAddHomdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the additive homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the additive homomorphism of $f$ is an additive homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{AddHomClass\_\_map\_add}$ applied to $f$.

AddMonoid.EnddefMathlib.Algebra.Group.Hom.Defs, type

Wording

end of M (from the name)

English

Let $M$ be a set. Then an end of $M$ is an element of the function that maps $M$ to the set of additive monoid homomorphisms of $M$ and $M$.

AddMonoidHomstructureMathlib.Algebra.Group.Hom.Defs, type

Wording

additive monoid homomorphism of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the additive monoid homomorphisms of $M$ and $N$ are a basic type.

AddMonoidHom.compdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be an additive monoid homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be an additive monoid homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is an additive monoid homomorphism of $M$ and $P$.

AddMonoidHom.copydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

AddMonoidHom.iddefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the identity map of M (from the docstring)

English

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

AddMonoidHom.inversedefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be an additive monoid homomorphism of $A$ and $B$. Let $g$ be a function from elements of $B$ to elements of $A$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$ and $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is an additive monoid homomorphism of $B$ and $A$.

AddMonoidHom.mk'defMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $M$ to elements of $G$ such that for all elements $a$ and $b$ of $M$, $\EqtMACRoH {f (a + b)}{f (a)+ f (b)}$. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_add}$ is an additive monoid homomorphism of $M$ and $G$.

AddMonoidHom.ofClassdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $M$ and $N$.

AddMonoidHom.toAddHomdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the additive homomorphism of self (from the name)

English

Let $\mathrm{self}$ be an additive monoid homomorphism of $M$ and $N$. Then the additive homomorphism of $\mathrm{self}$ is an additive homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toZeroHom}$ applied to $\mathrm{self}$ and $\mathrm{AddMonoidHom\_\_map\_add'}$ applied to $\mathrm{self}$.

AddMonoidHomClassclassMathlib.Algebra.Group.Hom.Defs, predicate

Wording

no wording

English

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

LibraryNote.hom_simp_lemma_prioritydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_hom\_simp\_lemma\_priority}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Monoid.EnddefMathlib.Algebra.Group.Hom.Defs, type

Wording

end of M (from the name)

English

Let $M$ be a set. Then an end of $M$ is an element of the function that maps $M$ to the set of monoid homomorphisms of $M$ and $M$.

MonoidHomstructureMathlib.Algebra.Group.Hom.Defs, type

Wording

monoid homomorphism of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the monoid homomorphisms of $M$ and $N$ are a basic type.

MonoidHom.compdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be a monoid homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be a monoid homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is a monoid homomorphism of $M$ and $P$.

MonoidHom.copydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

MonoidHom.iddefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the identity map of M (from the docstring)

English

Let $M$ be a set. Then the identity map of $M$ is a monoid homomorphism of $M$ and $M$.

MonoidHom.inversedefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

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

MonoidHom.mk'defMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $M$ to elements of $G$ such that for all elements $a$ and $b$ of $M$, $\EqtMACRoH {f (a \times b)}{f (a)\times f (b)}$. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{map\_mul}$ is a monoid homomorphism of $M$ and $G$.

MonoidHom.ofClassdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the monoid homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the monoid homomorphism of $f$ is a monoid homomorphism of $M$ and $N$.

MonoidHom.toMulHomdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the multiplicative homomorphism of self (from the name)

English

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

MonoidHomClassclassMathlib.Algebra.Group.Hom.Defs, predicate

Wording

no wording

English

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

MulHomstructureMathlib.Algebra.Group.Hom.Defs, type

Wording

multiplicative homomorphism of M and N (from the name)

English

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

MulHom.compdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be a multiplicative homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be a multiplicative homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is a multiplicative homomorphism of $M$ and $P$.

MulHom.copydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

MulHom.iddefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the identity map of M (from the docstring)

English

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

MulHom.inversedefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

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

MulHom.toFundefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the multiplicative homomorphism of self and x2 (from the name)

English

Let $\mathrm{self}$ be a multiplicative homomorphism of $M$ and $N$. Let $x_{2}$ be an element of $M$. Then the multiplicative homomorphism of $\mathrm{self}$ and $x_{2}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

MulHomClassclassMathlib.Algebra.Group.Hom.Defs, predicate

Wording

no wording

English

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

MulHomClass.toMulHomdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the multiplicative homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the multiplicative homomorphism of $f$ is a multiplicative homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{MulHomClass\_\_map\_mul}$ applied to $f$.

OneHomstructureMathlib.Algebra.Group.Hom.Defs, type

Wording

one homomorphism of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the one homomorphisms of $M$ and $N$ are a basic type.

OneHom.compdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be an one homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be an one homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is an one homomorphism of $M$ and $P$.

OneHom.copydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

OneHom.iddefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the identity of M (from the name)

English

Let $M$ be a set. Then the identity of $M$ is an one homomorphism of $M$ and $M$.

OneHom.inversedefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be an one homomorphism of $M$ and $N$. Let $g$ be a function from elements of $N$ to elements of $M$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is an one homomorphism of $N$ and $M$.

OneHom.toFundefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the one homomorphism of self and x2 (from the name)

English

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

OneHomClassclassMathlib.Algebra.Group.Hom.Defs, predicate

Wording

no wording

English

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

OneHomClass.toOneHomdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the one homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the one homomorphism of $f$ is an one homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{OneHomClass\_\_map\_one}$ applied to $f$.

ZeroHomstructureMathlib.Algebra.Group.Hom.Defs, type

Wording

zero homomorphism of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the zero homomorphisms of $M$ and $N$ are a basic type.

ZeroHom.compdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be a zero homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be a zero homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is a zero homomorphism of $M$ and $P$.

ZeroHom.copydefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

ZeroHom.iddefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the identity map of M (from the docstring)

English

Let $M$ be a set. Then the identity map of $M$ is a zero homomorphism of $M$ and $M$.

ZeroHom.inversedefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

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

ZeroHom.toFundefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the zero homomorphism of self and x2 (from the name)

English

Let $\mathrm{self}$ be a zero homomorphism of $M$ and $N$. Let $x_{2}$ be an element of $M$. Then the zero homomorphism of $\mathrm{self}$ and $x_{2}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

ZeroHomClassclassMathlib.Algebra.Group.Hom.Defs, predicate

Wording

no wording

English

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

ZeroHomClass.toZeroHomdefMathlib.Algebra.Group.Hom.Defs, function or constant

Wording

the zero homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the zero homomorphism of $f$ is a zero homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{ZeroHomClass\_\_map\_zero}$ applied to $f$.

Mathlib.Algebra.Group.Hom.Instances

AddMonoidHom.compHomdefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the composition homomorphism (from the name)

English

The composition homomorphism is an additive monoid homomorphism of the set of additive monoid homomorphisms of $N$ and $P$ and the set of additive monoid homomorphisms of the set of additive monoid homomorphisms of $M$ and $N$ and the set of additive monoid homomorphisms of $M$ and $P$.

AddMonoidHom.compHom'defMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the composition homomorphism of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then the composition homomorphism of $f$ is an additive monoid homomorphism of the set of additive monoid homomorphisms of $N$ and $P$ and the set of additive monoid homomorphisms of $M$ and $P$ defined as the flip of the composition of the evaluation and $f$.

AddMonoidHom.compl₂defMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the complement of f and g (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of $N$ and $P$. Let $g$ be an additive monoid homomorphism of $Q$ and $N$. Then the complement of $f$ and $g$ is an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of $Q$ and $P$ defined as the composition of the composition homomorphism of $g$ and $f$.

AddMonoidHom.compr₂defMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of $N$ and $P$. Let $g$ be an additive monoid homomorphism of $P$ and $Q$. Then $\mathrm{AddMonoidHom\_\_compr\_u2082\_}$ applied to $f$ and $g$ is an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of $N$ and $Q$ defined as the composition of $\operatorname{compHom}$ applied to $g$ and $f$.

AddMonoidHom.evaldefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the evaluation (from the name)

English

The evaluation is an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of the set of additive monoid homomorphisms of $M$ and $N$ and $N$ defined as the flip of the identity map of the set of additive monoid homomorphisms of $M$ and $N$.

AddMonoidHom.flipdefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the flip of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of $N$ and $P$. Then the flip of $f$ is an additive monoid homomorphism of $N$ and the set of additive monoid homomorphisms of $M$ and $P$.

AddMonoidHom.flipHomdefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the flip homomorphism (from the name)

English

The flip homomorphism is an additive monoid homomorphism of the set of additive monoid homomorphisms of $M$ and the set of additive monoid homomorphisms of $N$ and $P$ and the set of additive monoid homomorphisms of $N$ and the set of additive monoid homomorphisms of $M$ and $P$.

MonoidHom.compHomdefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the composition homomorphism (from the name)

English

The composition homomorphism is a monoid homomorphism of the set of monoid homomorphisms of $N$ and $P$ and the set of monoid homomorphisms of the set of monoid homomorphisms of $M$ and $N$ and the set of monoid homomorphisms of $M$ and $P$.

MonoidHom.compHom'defMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the composition homomorphism of f (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Then the composition homomorphism of $f$ is a monoid homomorphism of the set of monoid homomorphisms of $N$ and $P$ and the set of monoid homomorphisms of $M$ and $P$ defined as the flip of the composition of the evaluation and $f$.

MonoidHom.compl₂defMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the complement of f and g (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and the set of monoid homomorphisms of $N$ and $P$. Let $g$ be a monoid homomorphism of $Q$ and $N$. Then the complement of $f$ and $g$ is a monoid homomorphism of $M$ and the set of monoid homomorphisms of $Q$ and $P$ defined as the composition of the composition homomorphism of $g$ and $f$.

MonoidHom.compr₂defMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

no wording

English

Let $f$ be a monoid homomorphism of $M$ and the set of monoid homomorphisms of $N$ and $P$. Let $g$ be a monoid homomorphism of $P$ and $Q$. Then $\mathrm{MonoidHom\_\_compr\_u2082\_}$ applied to $f$ and $g$ is a monoid homomorphism of $M$ and the set of monoid homomorphisms of $N$ and $Q$ defined as the composition of $\operatorname{compHom}$ applied to $g$ and $f$.

MonoidHom.evaldefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the evaluation (from the name)

English

The evaluation is a monoid homomorphism of $M$ and the set of monoid homomorphisms of the set of monoid homomorphisms of $M$ and $N$ and $N$ defined as the flip of the identity map of the set of monoid homomorphisms of $M$ and $N$.

MonoidHom.flipdefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the flip of f (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and the set of monoid homomorphisms of $N$ and $P$. Then the flip of $f$ is a monoid homomorphism of $N$ and the set of monoid homomorphisms of $M$ and $P$.

MonoidHom.flipHomdefMathlib.Algebra.Group.Hom.Instances, function or constant

Wording

the flip homomorphism (from the name)

English

The flip homomorphism is a monoid homomorphism of the set of monoid homomorphisms of $M$ and the set of monoid homomorphisms of $N$ and $P$ and the set of monoid homomorphisms of $N$ and the set of monoid homomorphisms of $M$ and $P$.

Mathlib.Algebra.Group.Ideal

AddSemigroupIdealdefMathlib.Algebra.Group.Ideal, type

Wording

additive semigroup ideal of M (from the name)

English

Let $M$ be a set. Then an additive semigroup ideal of $M$ is an element of the function that maps $M$ to the set of difference additive actions of $M$ and $M$.

AddSemigroupIdeal.FGdefMathlib.Algebra.Group.Ideal, predicate

Wording

no wording

English

Let $I$ be an additive semigroup ideal of $M$. Then $\operatorname{FG}$ holds for $I$, if there exists an element $s$ of $\wp M$, such that $s$ is finite and $I$ is equal to the closure of $s$.

AddSemigroupIdeal.closuredefMathlib.Algebra.Group.Ideal, function or constant

Wording

the closure of s (from the name)

English

Let $s$ be an element of $\wp M$. Then the closure of $s$ is an additive semigroup ideal of $M$ defined as the closure of $M$ and $s$.

SemigroupIdealdefMathlib.Algebra.Group.Ideal, type

Wording

semigroup ideal of M (from the name)

English

Let $M$ be a set. Then a semigroup ideal of $M$ is an element of the function that maps $M$ to the set of difference multiplicative actions of $M$ and $M$.

SemigroupIdeal.FGdefMathlib.Algebra.Group.Ideal, predicate

Wording

no wording

English

Let $I$ be a semigroup ideal of $M$. Then $\operatorname{FG}$ holds for $I$, if there exists an element $s$ of $\wp M$, such that $s$ is finite and $I$ is equal to the closure of $s$.

SemigroupIdeal.closuredefMathlib.Algebra.Group.Ideal, function or constant

Wording

the closure of s (from the name)

English

Let $s$ be an element of $\wp M$. Then the closure of $s$ is a semigroup ideal of $M$ defined as the closure of $M$ and $s$.

Mathlib.Algebra.Group.Idempotent

IsIdempotentElemdefMathlib.Algebra.Group.Idempotent, predicate

Wording

a is a idempotent element (from the name)

English

Let $a$ be an element of $M$. Then $a$ is an idempotent element, if $\EqtMACRoH {a \times a}{a}$.

Mathlib.Algebra.Group.Indicator

Set.indicatorHomdefMathlib.Algebra.Group.Indicator, function or constant

Wording

the indicator homomorphism of M and s (from the name)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then the indicator homomorphism of $M$ and $s$ is an additive monoid homomorphism of the set of functions from elements of $x$ to elements of $M$ and the set of functions from elements of $x$ to elements of $M$.

Set.mulIndicatorHomdefMathlib.Algebra.Group.Indicator, function or constant

Wording

the multiplicative indicator homomorphism of M and s (from the name)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then the multiplicative indicator homomorphism of $M$ and $s$ is a monoid homomorphism of the set of functions from elements of $x$ to elements of $M$ and the set of functions from elements of $x$ to elements of $M$.

Mathlib.Algebra.Group.Invertible.Basic

Invertible.mulLeftdefMathlib.Algebra.Group.Invertible.Basic, function or constant

Wording

the left multiplicative of x2 and b (from the name)

English

Assume that $a$ is invertible. Let $b$ be an element of $x$. Then the left multiplicative of $x_{2}$ and $b$ is an equivalence from the proposition that $b$ is invertible to the proposition that $a \times b$ is invertible.

Invertible.mulRightdefMathlib.Algebra.Group.Invertible.Basic, function or constant

Wording

the right multiplicative of a and x2 (from the name)

English

Let $a$ be an element of $x$. Assume that $b$ is invertible. Then the right multiplicative of $a$ and $x_{2}$ is an equivalence from the proposition that $a$ is invertible to the proposition that $a \times b$ is invertible.

invertibleEquivOfLeftInversedefMathlib.Algebra.Group.Invertible.Basic, function or constant

Wording

the invertible equivalence of g and r (from the name)

English

Let $f$ be an element of $F$. Let $g$ be an element of $G$. Let $r$ be an element of $R$. Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to $g$ and $\operatorname{coe}$ applied to $f$. Then the invertible equivalence of $g$ and $r$ is an equivalence from the proposition that $f$ applied to $r$ is invertible to the proposition that $r$ is invertible.

unitOfInvertibledefMathlib.Algebra.Group.Invertible.Basic, function or constant

Wording

the unit of a (from the name)

English

Let $a$ be an element of $x$. Then the unit of $a$ is a unit of $x$.

Mathlib.Algebra.Group.Invertible.Defs

InvertibleclassMathlib.Algebra.Group.Invertible.Defs, predicate

Wording

a is invertible (from the name)

English

Let $a$ be an element of $x$. Then we can say that $a$ is invertible.

Invertible.invOfdefMathlib.Algebra.Group.Invertible.Defs, function or constant

Wording

the inverse of a (from the docstring)

English

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

Mathlib.Algebra.Group.Irreducible.Defs

AddIrreduciblestructureMathlib.Algebra.Group.Irreducible.Defs, predicate

Wording

no wording

English

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

IrreduciblestructureMathlib.Algebra.Group.Irreducible.Defs, predicate

Wording

p is irreducible (by hand)

English

Let $p$ be an element of $M$. Then we can say that $p$ is irreducible.

Mathlib.Algebra.Group.Irreducible.Indecomposable

IsAddIndecomposabledefMathlib.Algebra.Group.Irreducible.Indecomposable, predicate

Wording

no wording

English

Let $v$ be a function from elements of $x$ to elements of $M$. Let $s$ be an element of $\wp x$. Let $i$ be an element of $x$. Then $\mathrm{IsAddIndecomposable}$ holds for $v$, $s$ and $i$, if $i$ is an element of $s$ and for all elements $j$ of $x$, if $j$ is an element of $s$, then for all elements $k$ of $x$, if $k$ is an element of $s$, then if $\EqtMACRoH {v (i)}{v (j)+ v (k)}$, then $\EqtMACRoH {v (j)}{0}$ or $\EqtMACRoH {v (k)}{0}$.

IsAddIndecomposable.baseOfdefMathlib.Algebra.Group.Irreducible.Indecomposable, function or constant

Wording

the base of v and f (from the name)

English

Let $v$ be a function from elements of $x$ to elements of $M$. Let $f$ be an additive monoid homomorphism of $M$ and $S$. Then the base of $v$ and $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $j$ to $\mathrm{IsAddIndecomposable}$ applied to $v$, $\operatorname{ofPred}$ applied to the function that maps $i$ to $\mathrm{Lt} (0 , f (v (i)))$ and $j$.

IsMulIndecomposabledefMathlib.Algebra.Group.Irreducible.Indecomposable, predicate

Wording

no wording

English

Let $v$ be a function from elements of $x$ to elements of $M$. Let $s$ be an element of $\wp x$. Let $i$ be an element of $x$. Then $\mathrm{IsMulIndecomposable}$ holds for $v$, $s$ and $i$, if $i$ is an element of $s$ and for all elements $j$ of $x$, if $j$ is an element of $s$, then for all elements $k$ of $x$, if $k$ is an element of $s$, then if $\EqtMACRoH {v (i)}{v (j)\times v (k)}$, then $\EqtMACRoH {v (j)}{1}$ or $\EqtMACRoH {v (k)}{1}$.

IsMulIndecomposable.baseOfdefMathlib.Algebra.Group.Irreducible.Indecomposable, function or constant

Wording

the base of v and f (from the name)

English

Let $v$ be a function from elements of $x$ to elements of $M$. Let $f$ be a monoid homomorphism of $M$ and $S$. Then the base of $v$ and $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $j$ to $\mathrm{IsMulIndecomposable}$ applied to $v$, $\operatorname{ofPred}$ applied to the function that maps $i$ to $\mathrm{Lt} (1 , f (v (i)))$ and $j$.

Mathlib.Algebra.Group.IsApply

IsAddApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsDivApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsIntCastApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsIntCastApplyEqSMulclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsInvApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsMulApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsMulApplyEqCompclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsNatCastApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsNatCastApplyEqSMulclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsNegApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsOneApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsOneApplyEqSelfclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsPowApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsSMulApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsSubApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsVAddApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

IsZeroApplyclassMathlib.Algebra.Group.IsApply, predicate

Wording

no wording

English

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

Mathlib.Algebra.Group.ModEq

AddCommGroup.ModEqdefMathlib.Algebra.Group.ModEq, predicate

Wording

no wording

English

Let $p$, $a$ and $b$ be elements of $M$. Then $\operatorname{ModEq}$ holds for $p$, $a$ and $b$, if there exist natural numbers $m$ and $n$, such that $\EqtMACRoH {\HSMulhSMulMACRoAL {m}{p}+ a}{\HSMulhSMulMACRoAL {n}{p}+ b}$.

Mathlib.Algebra.Group.Monoid

AddCancelCommMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

AddCancelMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

AddCommMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is an additive commutative monoid (by hand)

English

Let $M$ be a set. Then we can say that $M$ is an additive commutative monoid.

AddLeftCancelMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

AddMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a additive monoid (from the name)

English

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

AddRightCancelMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

AddZeroclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a additive zero (from the name)

English

Let $M$ be a set. Then we can say that $M$ is an additive zero.

AddZeroClassclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a additive zero class (from the name)

English

Let $M$ be a set. Then we can say that $M$ is an additive zero class.

CancelCommMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

CancelMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

CommMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a commutative monoid (by hand)

English

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

HasUniqueDivclassMathlib.Algebra.Group.Monoid, predicate

Wording

M has unique quotients (from the name)

English

Let $M$ be a set. Then we can say that $M$ has unique quotients.

HasUniqueRootsclassMathlib.Algebra.Group.Monoid, predicate

Wording

M has unique roots (from the name)

English

Let $M$ be a set. Then we can say that $M$ has unique roots.

IsAddTorsionFreeclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a additive torsion free (from the name)

English

Let $M$ be a set. Then we can say that $M$ is an additive torsion free.

IsDedekindFiniteAddMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a Dedekind finite additive monoid (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a Dedekind finite additive monoid.

IsDedekindFiniteMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a Dedekind finite monoid (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a Dedekind finite monoid.

IsMulTorsionFreeclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a multiplicative torsion free (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a multiplicative torsion free.

IsNotUnitalclassMathlib.Algebra.Group.Monoid, predicate

Wording

A is not unital (from the name)

English

Let $A$ be a set. Then we can say that $A$ is not unital.

IsUnitalclassMathlib.Algebra.Group.Monoid, predicate

Wording

A is unital (from the name)

English

Let $A$ be a set. Then we can say that $A$ is unital.

LeftCancelMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

LibraryNote.forgetful_inheritancedefMathlib.Algebra.Group.Monoid, function or constant

Wording

the forgetful inheritance (from the name)

English

The forgetful inheritance is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

MonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a monoid (by hand)

English

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

MulOneclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a multiplicative one (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a multiplicative one.

MulOneClassclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a multiplicative one class (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a multiplicative one class.

NPowclassMathlib.Algebra.Group.Monoid, predicate

Wording

M is a power (from the name)

English

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

NPow.npowdefMathlib.Algebra.Group.Monoid, function or constant

Wording

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

English

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

NSMulclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

NSMul.nsmuldefMathlib.Algebra.Group.Monoid, function or constant

Wording

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

English

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

RightCancelMonoidclassMathlib.Algebra.Group.Monoid, predicate

Wording

no wording

English

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

npowBinRecdefMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $x_{2}$ be an element of $M$. Then $\mathrm{npowBinRec}$ applied to $k$ and $x_{2}$ is an element of $M$ defined as $\operatorname{go}$ applied to $k$, $1$ and $x_{2}$.

npowBinRecAutodefMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $m$ be an element of $M$. Then $\mathrm{npowBinRecAuto}$ applied to $k$ and $m$ is an element of $M$ defined as $\mathrm{npowBinRec}$ applied to $k$ and $m$.

npowRec'defMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $x_{2}$ be a natural number. Let $x_{3}$ be an element of $M$. Then $\mathrm{npowRec'}$ applied to $x_{2}$ and $x_{3}$ is an element of $M$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{npowRec'\_\_\_f}$ and $x_{3}$.

npowRecAutodefMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $m$ be an element of $M$. Then $\mathrm{npowRecAuto}$ applied to $k$ and $m$ is an element of $M$ defined as $\mathrm{npowRec}$ applied to $k$ and $m$.

nsmulBinRecdefMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $x_{2}$ be an element of $M$. Then $\mathrm{nsmulBinRec}$ applied to $k$ and $x_{2}$ is an element of $M$ defined as $\operatorname{go}$ applied to $k$, $0$ and $x_{2}$.

nsmulBinRecAutodefMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $m$ be an element of $M$. Then $\mathrm{nsmulBinRecAuto}$ applied to $k$ and $m$ is an element of $M$ defined as $\mathrm{nsmulBinRec}$ applied to $k$ and $m$.

nsmulRec'defMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $x_{2}$ be a natural number. Let $x_{3}$ be an element of $M$. Then $\mathrm{nsmulRec'}$ applied to $x_{2}$ and $x_{3}$ is an element of $M$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{nsmulRec'\_\_\_f}$ and $x_{3}$.

nsmulRecAutodefMathlib.Algebra.Group.Monoid, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $m$ be an element of $M$. Then $\mathrm{nsmulRecAuto}$ applied to $k$ and $m$ is an element of $M$ defined as $\mathrm{nsmulRec}$ applied to $k$ and $m$.

Mathlib.Algebra.Group.Nat.Hom

multiplesAddHomdefMathlib.Algebra.Group.Nat.Hom, function or constant

Wording

the multiple additive homomorphism of M (from the name)

English

Let $M$ be a set. Then the multiple additive homomorphism of $M$ is an additive equivalence of $M$ and the set of additive monoid homomorphisms of $\Natural$ and $M$.

multiplesHomdefMathlib.Algebra.Group.Nat.Hom, function or constant

Wording

the multiple homomorphism of M (from the name)

English

Let $M$ be a set. Then the multiple homomorphism of $M$ is an equivalence from $M$ to the set of additive monoid homomorphisms of $\Natural$ and $M$.

powersHomdefMathlib.Algebra.Group.Nat.Hom, function or constant

Wording

the power homomorphism of M (from the name)

English

Let $M$ be a set. Then the power homomorphism of $M$ is an equivalence from $M$ to the set of monoid homomorphisms of the set of multiplicatives of $\Natural$ and $M$ defined as the composition of $\operatorname{ofMul}$ and the composition of the multiple homomorphism of $\mathrm{Additive}$ applied to $M$ and the left multiplicative.

powersMulHomdefMathlib.Algebra.Group.Nat.Hom, function or constant

Wording

the power multiplicative homomorphism of M (from the name)

English

Let $M$ be a set. Then the power multiplicative homomorphism of $M$ is a multiplicative equivalence of $M$ and the set of monoid homomorphisms of the set of multiplicatives of $\Natural$ and $M$.

Mathlib.Algebra.Group.NatPowAssoc

NatPowAssocclassMathlib.Algebra.Group.NatPowAssoc, predicate

Wording

M is a natural power associator (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a natural power associator.

Mathlib.Algebra.Group.PNatPowAssoc

PNatPowAssocclassMathlib.Algebra.Group.PNatPowAssoc, predicate

Wording

M is a natural power associator (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a natural power associator.

Mathlib.Algebra.Group.Pi.Lemmas

AddHom.coeFndefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the coercion function of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the coercion function of $x$ and $x_{1}$ is an additive homomorphism of the set of additive homomorphisms of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

AddHom.compLeftdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

AddHom.pidefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product of g (from the name)

English

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

AddHom.piMapdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product map of g (from the name)

English

Let $g$ be a function from elements $i_{2}$ of $x$ to additive homomorphisms of $M$ applied to $i_{2}$ and $N$ applied to $i_{2}$. Then the product map of $i_{2}$ is an additive homomorphism of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $N$ applied to $i_{1}$ defined as the function that maps $g$ to the product of the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the evaluation additive homomorphism of $M$ and $i$.

AddMonoidHom.coeFndefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the coercion function of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the coercion function of $x$ and $x_{1}$ is an additive monoid homomorphism of the set of additive monoid homomorphisms of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

AddMonoidHom.compLeftdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

AddMonoidHom.pidefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product of g (from the name)

English

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

AddMonoidHom.piMapdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product map of g (from the name)

English

Let $g$ be a function from elements $i_{2}$ of $x$ to additive monoid homomorphisms of $M$ applied to $i_{2}$ and $N$ applied to $i_{2}$. Then the product map of $i_{2}$ is an additive monoid homomorphism of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $N$ applied to $i_{1}$ defined as the function that maps $g$ to the product of the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the evaluation additive monoid homomorphism of $M$ and $i$.

AddMonoidHom.singledefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

no wording

English

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

Function.ExtendByOne.homdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the homomorphism of R and s (from the name)

English

Let $R$ be a set. Let $s$ be a function from elements of $x$ to elements of $x_{1}$. Then the homomorphism of $R$ and $s$ is a monoid homomorphism of the set of functions from elements of $x$ to elements of $R$ and the set of functions from elements of $x_{1}$ to elements of $R$.

Function.ExtendByZero.homdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the homomorphism of R and s (from the name)

English

Let $R$ be a set. Let $s$ be a function from elements of $x$ to elements of $x_{1}$. Then the homomorphism of $R$ and $s$ is an additive monoid homomorphism of the set of functions from elements of $x$ to elements of $R$ and the set of functions from elements of $x_{1}$ to elements of $R$.

MonoidHom.coeFndefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the coercion function of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the coercion function of $x$ and $x_{1}$ is a monoid homomorphism of the set of monoid homomorphisms of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

MonoidHom.compLeftdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

MonoidHom.mulSingledefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

no wording

English

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

MonoidHom.pidefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product of g (from the name)

English

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

MonoidHom.piMapdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product map of g (from the name)

English

Let $g$ be a function from elements $i_{2}$ of $x$ to monoid homomorphisms of $M$ applied to $i_{2}$ and $N$ applied to $i_{2}$. Then the product map of $i_{2}$ is a monoid homomorphism of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $N$ applied to $i_{1}$ defined as the function that maps $g$ to the product of the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the evaluation monoid homomorphism of $M$ and $i$.

MulHom.coeFndefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the coercion function of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the coercion function of $x$ and $x_{1}$ is a multiplicative homomorphism of the set of multiplicative homomorphisms of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

MulHom.compLeftdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

MulHom.pidefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product of g (from the name)

English

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

MulHom.piMapdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

the product map of g (from the name)

English

Let $g$ be a function from elements $i_{2}$ of $x$ to multiplicative homomorphisms of $M$ applied to $i_{2}$ and $N$ applied to $i_{2}$. Then the product map of $i_{2}$ is a multiplicative homomorphism of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $N$ applied to $i_{1}$ defined as the function that maps $g$ to the product of the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the evaluation multiplicative homomorphism of $M$ and $i$.

OneHom.mulSingledefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then $\operatorname{mulSingle}$ applied to $f$ and $i$ is an one homomorphism of $f$ applied to $i$ and the set of functions from elements $i_{1}$ of $I$ to elements of $f$ applied to $i_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mulSingle}$ applied to $i$ and $\mathrm{Pi\_\_mulSingle\_one}$ applied to $i$.

Pi.constAddHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

Pi.constAddMonoidHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

Pi.constMonoidHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

Pi.constMulHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

Pi.evalAddHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

Let $f$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then the evaluation additive homomorphism of $f$ and $i$ is an additive homomorphism of the set of functions from elements $i_{1}$ of $I$ to elements of $f$ applied to $i_{1}$ and $f$ applied to $i$ defined as $\operatorname{mk}$ applied to the function that maps $g$ to $g$ applied to $i$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Pi\_\_add\_apply}$ applied to $x_{1}$, $x_{2}$ and $i$.

Pi.evalAddMonoidHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

Pi.evalMonoidHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

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

Pi.evalMulHomdefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

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

English

Let $f$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then the evaluation multiplicative homomorphism of $f$ and $i$ is a multiplicative homomorphism of the set of functions from elements $i_{1}$ of $I$ to elements of $f$ applied to $i_{1}$ and $f$ applied to $i$ defined as $\operatorname{mk}$ applied to the function that maps $g$ to $g$ applied to $i$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Pi\_\_mul\_apply}$ applied to $x_{1}$, $x_{2}$ and $i$.

ZeroHom.singledefMathlib.Algebra.Group.Pi.Lemmas, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then $\operatorname{single}$ applied to $f$ and $i$ is a zero homomorphism of $f$ applied to $i$ and the set of functions from elements $i_{1}$ of $I$ to elements of $f$ applied to $i_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $i$ and $\mathrm{Pi\_\_single\_zero}$ applied to $i$.

Mathlib.Algebra.Group.Pi.Units

AddEquiv.piAddUnitsdefMathlib.Algebra.Group.Pi.Units, function or constant

Wording

the product additive unit (from the name)

English

The product additive unit is an additive equivalence of the set of additive units of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to additive units of $M$ applied to $i_{1}$.

MulEquiv.piUnitsdefMathlib.Algebra.Group.Pi.Units, function or constant

Wording

the product unit (from the name)

English

The product unit is a multiplicative equivalence of $\UnitsMACRoAO {(\mathrm{Elem} (x)\rightarrow M (i))}$ and the set of functions from elements $i_{1}$ of $x$ to units of $M$ applied to $i_{1}$.

Mathlib.Algebra.Group.Pointwise.Finset.Basic

Finset.coeAddMonoidHomdefMathlib.Algebra.Group.Pointwise.Finset.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 the set of finite sets of $x$ and $\wp x$.

Finset.coeMonoidHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the coercion monoid homomorphism (from the name)

English

The coercion monoid homomorphism is a monoid homomorphism of the set of finite sets of $x$ and $\wp x$.

Finset.imageAddHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the image additive homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the image additive homomorphism of $f$ is an additive homomorphism of the set of finite sets of $x$ and the set of finite sets of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{image}$ applied to $\operatorname{coe}$ applied to $f$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Finset\_\_image\_add}$ applied to $f$.

Finset.imageAddMonoidHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

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

English

Let $f$ be an element of $F$. Then the image additive monoid homomorphism of $f$ is an additive monoid homomorphism of the set of finite sets of $x$ and the set of finite sets of $x_{1}$.

Finset.imageMonoidHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the image monoid homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the image monoid homomorphism of $f$ is a monoid homomorphism of the set of finite sets of $x$ and the set of finite sets of $x_{1}$.

Finset.imageMulHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the image multiplicative homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the image multiplicative homomorphism of $f$ is a multiplicative homomorphism of the set of finite sets of $x$ and the set of finite sets of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{image}$ applied to $\operatorname{coe}$ applied to $f$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Finset\_\_image\_mul}$ applied to $f$.

Finset.imageOneHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the image one homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the image one homomorphism of $f$ is an one homomorphism of the set of finite sets of $x$ and the set of finite sets of $x_{1}$.

Finset.imageZeroHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the image zero homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the image zero homomorphism of $f$ is a zero homomorphism of the set of finite sets of $x$ and the set of finite sets of $x_{1}$.

Finset.singletonAddHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is an additive homomorphism of $x$ and the set of finite sets of $x$.

Finset.singletonAddMonoidHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is an additive monoid homomorphism of $x$ and the set of finite sets of $x$.

Finset.singletonMonoidHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is a monoid homomorphism of $x$ and the set of finite sets of $x$.

Finset.singletonMulHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is a multiplicative homomorphism of $x$ and the set of finite sets of $x$.

Finset.singletonOneHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is an one homomorphism of $x$ and the set of finite sets of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{singleton}$ and $\mathrm{Finset\_\_singleton\_one}$.

Finset.singletonZeroHomdefMathlib.Algebra.Group.Pointwise.Finset.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is a zero homomorphism of $x$ and the set of finite sets of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{singleton}$ and $\mathrm{Finset\_\_singleton\_zero}$.

Mathlib.Algebra.Group.Pointwise.Set.Basic

LibraryNote.pointwise_nat_actiondefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the pointwise natural action (from the name)

English

The pointwise natural action is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Set.singletonAddHomdefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is an additive homomorphism of $x$ and $\wp x$.

Set.singletonAddMonoidHomdefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is an additive monoid homomorphism of $x$ and $\wp x$.

Set.singletonMonoidHomdefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is a monoid homomorphism of $x$ and $\wp x$.

Set.singletonMulHomdefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is a multiplicative homomorphism of $x$ and $\wp x$.

Set.singletonOneHomdefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is an one homomorphism of $x$ and $\wp x$ defined as $\operatorname{mk}$ applied to $\operatorname{singleton}$ and $\mathrm{Set\_\_singleton\_one}$.

Set.singletonZeroHomdefMathlib.Algebra.Group.Pointwise.Set.Basic, function or constant

Wording

the singleton operation (from the docstring)

English

The singleton operation is a zero homomorphism of $x$ and $\wp x$ defined as $\operatorname{mk}$ applied to $\operatorname{singleton}$ and $\mathrm{Set\_\_singleton\_zero}$.

Mathlib.Algebra.Group.Prod

AddEquiv.currydefMathlib.Algebra.Group.Prod, function or constant

Wording

the curry of x1 and M (from the name)

English

Let $x$, $x_{1}$ and $M$ be sets. Then the curry of $x_{1}$ and $M$ is an additive equivalence of the set of functions from elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ to elements of $M$ and the set of functions from elements of $x$ and elements of $x_{1}$ to elements of $M$.

AddEquiv.prodAddUnitsdefMathlib.Algebra.Group.Prod, function or constant

Wording

the product additive unit (from the name)

English

The product additive unit is an additive equivalence of the set of additive units of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to the set of additive units of $M$ and the set of additive units of $N$.

AddEquiv.prodAssocdefMathlib.Algebra.Group.Prod, function or constant

Wording

the product associator (from the name)

English

The product associator is an additive equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $N$ and $P$ and $\mathrm{Prod}$ applied to $M$ and $\mathrm{Prod}$ applied to $N$ and $P$.

AddEquiv.prodCommdefMathlib.Algebra.Group.Prod, function or constant

Wording

no wording

English

$\operatorname{prodComm}$ is an additive equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $N$ and $M$.

AddEquiv.prodCongrdefMathlib.Algebra.Group.Prod, function or constant

Wording

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

English

Let $f$ be an additive equivalence of $M$ and $\mathrm{M'}$. Let $g$ be an additive equivalence of $N$ and $\mathrm{N'}$. Then the product congruence of $f$ and $g$ is an additive equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$.

AddEquiv.prodProdProdCommdefMathlib.Algebra.Group.Prod, function or constant

Wording

no wording

English

Let $M$, $N$, $\mathrm{M'}$ and $\mathrm{N'}$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $M$, $N$, $\mathrm{M'}$ and $\mathrm{N'}$ is an additive equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$ and $\mathrm{Prod}$ applied to $N$ and $\mathrm{N'}$.

AddEquiv.prodUniquedefMathlib.Algebra.Group.Prod, function or constant

Wording

no wording

English

$\operatorname{prodUnique}$ is an additive equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$.

AddEquiv.uniqueProddefMathlib.Algebra.Group.Prod, function or constant

Wording

the unique product (from the name)

English

The unique product is an additive equivalence of $\mathrm{Prod}$ applied to $N$ and $M$ and $M$.

AddHom.coproddefMathlib.Algebra.Group.Prod, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $P$. Let $g$ be an additive homomorphism of $N$ and $P$. Then the coproduct of $f$ and $g$ is an additive homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$ defined as the sum of the composition of $f$ and the first component of $M$ and $N$ and the composition of $g$ and the second component of $M$ and $N$.

AddHom.fstdefMathlib.Algebra.Group.Prod, function or constant

Wording

the first component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the first component of $M$ and $N$ is an additive homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$.

AddHom.proddefMathlib.Algebra.Group.Prod, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $g$ be an additive homomorphism of $M$ and $P$. Then the product of $f$ and $g$ is an additive homomorphism of $M$ and $\mathrm{Prod}$ applied to $N$ and $P$.

AddHom.prodMapdefMathlib.Algebra.Group.Prod, function or constant

Wording

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

English

Let $f$ be an additive homomorphism of $M$ and $\mathrm{M'}$. Let $g$ be an additive homomorphism of $N$ and $\mathrm{N'}$. Then the product map of $f$ and $g$ is an additive homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$ defined as the product of the composition of $f$ and the first component of $M$ and $N$ and the composition of $g$ and the second component of $M$ and $N$.

AddHom.snddefMathlib.Algebra.Group.Prod, function or constant

Wording

the second component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the second component of $M$ and $N$ is an additive homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $N$.

AddMonoidHom.coproddefMathlib.Algebra.Group.Prod, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $P$. Let $g$ be an additive monoid homomorphism of $N$ and $P$. Then the coproduct of $f$ and $g$ is an additive monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$ defined as the sum of the composition of $f$ and the first component of $M$ and $N$ and the composition of $g$ and the second component of $M$ and $N$.

AddMonoidHom.fstdefMathlib.Algebra.Group.Prod, function or constant

Wording

the first component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the first component of $M$ and $N$ is an additive monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$.

AddMonoidHom.inldefMathlib.Algebra.Group.Prod, function or constant

Wording

the left injection of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the left injection of $M$ and $N$ is an additive monoid homomorphism of $M$ and $\mathrm{Prod}$ applied to $M$ and $N$.

AddMonoidHom.inrdefMathlib.Algebra.Group.Prod, function or constant

Wording

the right injection of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the right injection of $M$ and $N$ is an additive monoid homomorphism of $N$ and $\mathrm{Prod}$ applied to $M$ and $N$.

AddMonoidHom.proddefMathlib.Algebra.Group.Prod, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $g$ be an additive monoid homomorphism of $M$ and $P$. Then the product of $f$ and $g$ is an additive monoid homomorphism of $M$ and $\mathrm{Prod}$ applied to $N$ and $P$.

AddMonoidHom.prodMapdefMathlib.Algebra.Group.Prod, function or constant

Wording

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

English

Let $f$ be an additive monoid homomorphism of $M$ and $\mathrm{M'}$. Let $g$ be an additive monoid homomorphism of $N$ and $\mathrm{N'}$. Then the product map of $f$ and $g$ is an additive monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$ defined as the product of the composition of $f$ and the first component of $M$ and $N$ and the composition of $g$ and the second component of $M$ and $N$.

AddMonoidHom.snddefMathlib.Algebra.Group.Prod, function or constant

Wording

the second component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the second component of $M$ and $N$ is an additive monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $N$.

AddUnits.embedProductdefMathlib.Algebra.Group.Prod, function or constant

Wording

the embed product of x (from the name)

English

Let $x$ be a set. Then the embed product of $x$ is an additive monoid homomorphism of the set of additive units of $x$ and $\mathrm{Prod}$ applied to $x$ and the set of additive opposites of $x$.

MonoidHom.coproddefMathlib.Algebra.Group.Prod, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $P$. Let $g$ be a monoid homomorphism of $N$ and $P$. Then the coproduct of $f$ and $g$ is a monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$ defined as the product of the composition of $f$ and the first component of $M$ and $N$ and the composition of $g$ and the second component of $M$ and $N$.

MonoidHom.fstdefMathlib.Algebra.Group.Prod, function or constant

Wording

the first component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the first component of $M$ and $N$ is a monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$.

MonoidHom.inldefMathlib.Algebra.Group.Prod, function or constant

Wording

the left injection of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the left injection of $M$ and $N$ is a monoid homomorphism of $M$ and $\mathrm{Prod}$ applied to $M$ and $N$.

MonoidHom.inrdefMathlib.Algebra.Group.Prod, function or constant

Wording

the right injection of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the right injection of $M$ and $N$ is a monoid homomorphism of $N$ and $\mathrm{Prod}$ applied to $M$ and $N$.

MonoidHom.proddefMathlib.Algebra.Group.Prod, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Let $g$ be a monoid homomorphism of $M$ and $P$. Then the product of $f$ and $g$ is a monoid homomorphism of $M$ and $\mathrm{Prod}$ applied to $N$ and $P$.

MonoidHom.prodMapdefMathlib.Algebra.Group.Prod, function or constant

Wording

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

English

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

MonoidHom.snddefMathlib.Algebra.Group.Prod, function or constant

Wording

the second component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the second component of $M$ and $N$ is a monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $N$.

MulEquiv.currydefMathlib.Algebra.Group.Prod, function or constant

Wording

the curry of x1 and M (from the name)

English

Let $x$, $x_{1}$ and $M$ be sets. Then the curry of $x_{1}$ and $M$ is a multiplicative equivalence of the set of functions from elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ to elements of $M$ and the set of functions from elements of $x$ and elements of $x_{1}$ to elements of $M$.

MulEquiv.prodAssocdefMathlib.Algebra.Group.Prod, function or constant

Wording

the product associator (from the name)

English

The product associator is a multiplicative equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $N$ and $P$ and $\mathrm{Prod}$ applied to $M$ and $\mathrm{Prod}$ applied to $N$ and $P$.

MulEquiv.prodCommdefMathlib.Algebra.Group.Prod, function or constant

Wording

no wording

English

$\operatorname{prodComm}$ is a multiplicative equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $N$ and $M$.

MulEquiv.prodCongrdefMathlib.Algebra.Group.Prod, function or constant

Wording

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

English

Let $f$ be a multiplicative equivalence of $M$ and $\mathrm{M'}$. Let $g$ be a multiplicative equivalence of $N$ and $\mathrm{N'}$. Then the product congruence of $f$ and $g$ is a multiplicative equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$.

MulEquiv.prodProdProdCommdefMathlib.Algebra.Group.Prod, function or constant

Wording

no wording

English

Let $M$, $N$, $\mathrm{M'}$ and $\mathrm{N'}$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $M$, $N$, $\mathrm{M'}$ and $\mathrm{N'}$ is a multiplicative equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$ and $\mathrm{Prod}$ applied to $N$ and $\mathrm{N'}$.

MulEquiv.prodUniquedefMathlib.Algebra.Group.Prod, function or constant

Wording

no wording

English

$\operatorname{prodUnique}$ is a multiplicative equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$.

MulEquiv.prodUnitsdefMathlib.Algebra.Group.Prod, function or constant

Wording

the product unit (from the name)

English

The product unit is a multiplicative equivalence of $\UnitsMACRoAO {\mathrm{Prod} (M , N)}$ and $\mathrm{Prod}$ applied to $\UnitsMACRoAO {M}$ and $\UnitsMACRoAO {N}$.

MulEquiv.uniqueProddefMathlib.Algebra.Group.Prod, function or constant

Wording

the unique product (from the name)

English

The unique product is a multiplicative equivalence of $\mathrm{Prod}$ applied to $N$ and $M$ and $M$.

MulHom.coproddefMathlib.Algebra.Group.Prod, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be a multiplicative homomorphism of $M$ and $P$. Let $g$ be a multiplicative homomorphism of $N$ and $P$. Then the coproduct of $f$ and $g$ is a multiplicative homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$ defined as the product of the composition of $f$ and the first component of $M$ and $N$ and the composition of $g$ and the second component of $M$ and $N$.

MulHom.fstdefMathlib.Algebra.Group.Prod, function or constant

Wording

the first component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the first component of $M$ and $N$ is a multiplicative homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $M$.

MulHom.proddefMathlib.Algebra.Group.Prod, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Let $g$ be a multiplicative homomorphism of $M$ and $P$. Then the product of $f$ and $g$ is a multiplicative homomorphism of $M$ and $\mathrm{Prod}$ applied to $N$ and $P$.

MulHom.prodMapdefMathlib.Algebra.Group.Prod, function or constant

Wording

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

English

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

MulHom.snddefMathlib.Algebra.Group.Prod, function or constant

Wording

the second component of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the second component of $M$ and $N$ is a multiplicative homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $N$.

Units.embedProductdefMathlib.Algebra.Group.Prod, function or constant

Wording

the embed product of x (from the name)

English

Let $x$ be a set. Then the embed product of $x$ is a monoid homomorphism of $\UnitsMACRoAO {x}$ and $\mathrm{Prod}$ applied to $x$ and the set of multiplicative opposites of $x$.

addAddHomdefMathlib.Algebra.Group.Prod, function or constant

Wording

the additive additive homomorphism (from the name)

English

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

addAddMonoidHomdefMathlib.Algebra.Group.Prod, function or constant

Wording

the additive additive monoid homomorphism (from the name)

English

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

divMonoidHomdefMathlib.Algebra.Group.Prod, function or constant

Wording

the quotient monoid homomorphism (from the name)

English

The quotient monoid homomorphism is a monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.

mulMonoidHomdefMathlib.Algebra.Group.Prod, function or constant

Wording

the multiplicative monoid homomorphism (from the name)

English

The multiplicative monoid homomorphism is a monoid homomorphism of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.

mulMulHomdefMathlib.Algebra.Group.Prod, function or constant

Wording

the multiplicative multiplicative homomorphism (from the name)

English

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

subAddMonoidHomdefMathlib.Algebra.Group.Prod, function or constant

Wording

the difference additive monoid homomorphism (from the name)

English

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

Mathlib.Algebra.Group.SelfInv

IsSelfInvdefMathlib.Algebra.Group.SelfInv, predicate

Wording

a is a self inverse (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a self inverse, if $\EqtMACRoH {\operatorname{inv} (a)}{a}$.

IsSelfNegdefMathlib.Algebra.Group.SelfInv, predicate

Wording

a is a self negation (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a self negation, if $\EqtMACRoH {\operatorname{neg} (a)}{a}$.

Mathlib.Algebra.Group.Semigroup

AddCommMagmaclassMathlib.Algebra.Group.Semigroup, predicate

Wording

G is a additive commutative magma (from the name)

English

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

AddCommSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

G is a additive commutative semigroup (from the name)

English

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

AddCommutedefMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

Let $a$ and $b$ be elements of $M$. Then $\mathrm{AddCommute}$ holds for $a$ and $b$, if $\mathrm{AddSemiconjBy}$ holds for $a$, $b$ and $b$.

AddLeftCancelSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

AddRightCancelSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

AddSemiconjBydefMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

Let $a$, $x_{1}$ and $y$ be elements of $M$. Then $\mathrm{AddSemiconjBy}$ holds for $a$, $x_{1}$ and $y$, if $\EqtMACRoH {a + x_{1}}{y + a}$.

AddSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

G is a additive semigroup (from the name)

English

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

CommMagmaclassMathlib.Algebra.Group.Semigroup, predicate

Wording

G is a commutative magma (from the name)

English

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

CommSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

G is a commutative semigroup (from the name)

English

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

CommutedefMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

Let $a$ and $b$ be elements of $M$. Then $\mathrm{Commute}$ holds for $a$ and $b$, if $\mathrm{SemiconjBy}$ holds for $a$, $b$ and $b$.

IsAddCommutativeclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsCancelAddclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsCancelMulclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsLeftCancelAddclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsLeftCancelMulclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsMulCommutativeclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsRightCancelAddclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

IsRightCancelMulclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

LeftCancelSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

LibraryNote.lower_cancel_prioritydefMathlib.Algebra.Group.Semigroup, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_lower\_cancel\_priority}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

RightCancelSemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

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

SemiconjBydefMathlib.Algebra.Group.Semigroup, predicate

Wording

no wording

English

Let $a$, $x_{1}$ and $y$ be elements of $M$. Then $\mathrm{SemiconjBy}$ holds for $a$, $x_{1}$ and $y$, if $\EqtMACRoH {a \times x_{1}}{y \times a}$.

SemigroupclassMathlib.Algebra.Group.Semigroup, predicate

Wording

G is a semigroup (from the name)

English

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

Mathlib.Algebra.Group.Shrink

Shrink.addEquivdefMathlib.Algebra.Group.Shrink, function or constant

Wording

the additive equivalence (from the name)

English

The additive equivalence is an additive equivalence of the set of shrinks of $x$ and $x$ defined as the additive equivalence of the inverse of the equivalence shrink of $x$.

Shrink.mulEquivdefMathlib.Algebra.Group.Shrink, function or constant

Wording

the multiplicative equivalence (from the name)

English

The multiplicative equivalence is a multiplicative equivalence of the set of shrinks of $x$ and $x$ defined as the multiplicative equivalence of the inverse of the equivalence shrink of $x$.

Mathlib.Algebra.Group.Subgroup.Basic

AddAut.characteristicdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the characteristic of H (from the name)

English

Let $H$ be an additive subgroup of $G$. Then the characteristic of $H$ is an additive monoid homomorphism of the set of additive automorphisms of $G$ and the set of additive automorphisms of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$.

AddGroup.addConjugatesOfSetdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the additive conjugate of s (from the name)

English

Let $s$ be an element of $\wp G$. Then the additive conjugate of $s$ is an element of $\wp G$ defined as the union of the function that maps $a$ to the union of the function that maps $h$ to the additive conjugate of $a$.

AddMonoidHom.liftOfRightInversedefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the lift of f and f_neg (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$. Let $\mathrm{f\_neg}$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{RightInverse}$ holds for $\mathrm{f\_neg}$ and $\operatorname{coe}$ applied to $f$. Then the lift of $f$ and $\mathrm{f\_neg}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{AddMonoidHom} (x_{1} , x_{2})}$.

AddMonoidHom.liftOfSurjectivedefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the lift of f and hf (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the lift of $f$ and $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{AddMonoidHom} (x_{1} , x_{2})}$.

AddNormalizerConditiondefMathlib.Algebra.Group.Subgroup.Basic, predicate

Wording

G is a additive normalizer condition (from the name)

English

Let $G$ be a set. Then $G$ is an additive normalizer condition, if for all additive subgroups $H$ of $G$, if $H$ is less than the top, then $H$ is less than the normalizer of $H$.

AddSubgroup.CharacteristicclassMathlib.Algebra.Group.Subgroup.Basic, predicate

Wording

H is characteristic (from the name)

English

Let $H$ be an additive subgroup of $A$. Then we can say that $H$ is characteristic.

AddSubgroup.inertiadefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the inertia of I and G (from the name)

English

Let $I$ be an additive subgroup of $M$. Let $G$ be a set. Then the inertia of $I$ and $G$ is a subgroup of $G$.

AddSubgroup.normalClosuredefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the normal closure of s (from the docstring)

English

Let $s$ be an element of $\wp G$. Then the normal closure of $s$ is an additive subgroup of $G$ defined as the closure of the additive conjugate of $s$.

AddSubgroup.normalCoredefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the normal core of H (from the docstring)

English

Let $H$ be an additive subgroup of $G$. Then the normal core of $H$ is an additive subgroup of $G$.

AddSubgroup.pidefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the product of I and H (from the name)

English

Let $I$ be an element of $\wp x$. Let $H$ be a function from elements $i_{1}$ of $x$ to additive subgroups of $f$ applied to $i_{1}$. Then the product of $I$ and $i_{1}$ is an additive subgroup of the set of functions from elements $i$ of $x$ to elements of $f$ applied to $i$.

AddSubgroup.proddefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the product of H and K (from the name)

English

Let $H$ be an additive subgroup of $G$. Let $K$ be an additive subgroup of $N$. Then the product of $H$ and $K$ is an additive subgroup of $\mathrm{Prod}$ applied to $G$ and $N$.

AddSubgroup.prodEquivdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the product equivalence of H and K (from the name)

English

Let $H$ be an additive subgroup of $G$. Let $K$ be an additive subgroup of $N$. Then the product equivalence of $H$ and $K$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{prod} (H , K)}{x_{2}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {K}{x_{4}})}$.

ConjClasses.noncenterdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{noncenter}$ applied to $G$ is an element of the power set of the set of conjugate classes of $G$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that the carrier of $x_{1}$ is nontrivial.

Group.conjugatesOfSetdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the conjugate of s (from the name)

English

Let $s$ be an element of $\wp G$. Then the conjugate of $s$ is an element of $\wp G$ defined as the union of the function that maps $a$ to the union of the function that maps $h$ to the conjugate of $a$.

MonoidHom.liftOfRightInversedefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the lift of f and f_inv (from the name)

English

Let $f$ be a monoid homomorphism of $x$ and $x_{1}$. Let $\mathrm{f\_inv}$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{RightInverse}$ holds for $\mathrm{f\_inv}$ and $\operatorname{coe}$ applied to $f$. Then the lift of $f$ and $\mathrm{f\_inv}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{MonoidHom} (x_{1} , x_{2})}$.

MonoidHom.liftOfSurjectivedefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the lift of f and hf (from the name)

English

Let $f$ be a monoid homomorphism of $x$ and $x_{1}$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the lift of $f$ and $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{MonoidHom} (x_{1} , x_{2})}$.

MulAut.characteristicdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the characteristic of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the characteristic of $H$ is a monoid homomorphism of the set of multiplicative automorphisms of $G$ and the set of multiplicative automorphisms of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$.

NormalizerConditiondefMathlib.Algebra.Group.Subgroup.Basic, predicate

Wording

G is a normalizer condition (from the name)

English

Let $G$ be a set. Then $G$ is a normalizer condition, if for all subgroups $H$ of $G$, if $H$ is less than the top, then $H$ is less than the normalizer of $H$.

Subgroup.CharacteristicclassMathlib.Algebra.Group.Subgroup.Basic, predicate

Wording

H is characteristic (from the docstring)

English

Let $H$ be a subgroup of $G$. Then we can say that $H$ is characteristic.

Subgroup.normalClosuredefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the normal closure of s (from the docstring)

English

Let $s$ be an element of $\wp G$. Then the normal closure of $s$ is a subgroup of $G$ defined as the closure of the conjugate of $s$.

Subgroup.normalCoredefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the normal core of H (from the docstring)

English

Let $H$ be a subgroup of $G$. Then the normal core of $H$ is a subgroup of $G$.

Subgroup.pidefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the product of I and H (from the name)

English

Let $I$ be an element of $\wp x$. Let $H$ be a function from elements $i_{1}$ of $x$ to subgroups of $f$ applied to $i_{1}$. Then the product of $I$ and $i_{1}$ is a subgroup of the set of functions from elements $i$ of $x$ to elements of $f$ applied to $i$.

Subgroup.proddefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the product of H and K (from the name)

English

Let $H$ be a subgroup of $G$. Let $K$ be a subgroup of $N$. Then the product of $H$ and $K$ is a subgroup of $\mathrm{Prod}$ applied to $G$ and $N$.

Subgroup.prodEquivdefMathlib.Algebra.Group.Subgroup.Basic, function or constant

Wording

the product equivalence of H and K (from the name)

English

Let $H$ be a subgroup of $G$. Let $K$ be a subgroup of $N$. Then the product equivalence of $H$ and $K$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{prod} (H , K)}{x_{2}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {K}{x_{4}})}$.