Definitions: Mathlib.Algebra, part 7 of 17

AddSubgroupstructureMathlib.Algebra.Group.Subgroup.Defs, type

Wording

additive subgroup of G (from the name)

English

Let $G$ be a set. Then the additive subgroups of $G$ are a basic type.

AddSubgroup.NormalclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

H is normal (from the name)

English

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

AddSubgroup.copydefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the copy of K and s (from the name)

English

Let $K$ be an additive subgroup of $G$. Let $s$ be an element of $\wp G$ such that $\EqtMACRoH {s}{K}$. Then the copy of $K$ and $s$ is an additive subgroup of $G$.

AddSubgroup.inclusiondefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the inclusion homomorphism of h (from the docstring)

English

Assume that $H \leq K$. Then the inclusion homomorphism of $h$ is an additive monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {K}{x_{2}})}$.

AddSubgroup.normalizerdefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the normalizer of S (from the name)

English

Let $S$ be an element of $\wp G$. Then the normalizer of $S$ is an additive subgroup of $G$.

AddSubgroup.ofClassdefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the additive subgroup of s (from the name)

English

Let $s$ be an element of $S$. Then the additive subgroup of $s$ is an additive subgroup of $G$.

AddSubgroup.ofSubdefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the additive subgroup of s (from the name)

English

Let $s$ be an element of $\wp G$ such that $s$ is nonempty and for all elements $x_{1}$ of $G$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $G$, if $y$ is an element of $s$, then $x_{1} + \operatorname{neg} (y)$ is an element of $s$. Then the additive subgroup of $s$ is an additive subgroup of $G$.

AddSubgroup.subtypedefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the subtype of H (from the name)

English

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

AddSubgroupClassclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

G is a additive subgroup class (from the name)

English

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

AddSubgroupClass.inclusiondefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the inclusion homomorphism of h2 (from the docstring)

English

Assume that $H \leq K$. Then the inclusion homomorphism of $h_{2}$ is an additive monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {K}{x_{4}})}$.

AddSubgroupClass.subtypedefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the subtype of H (from the name)

English

Let $H$ be an element of $S$. Then the subtype of $H$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $G$.

HasMemOrInvMemclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

no wording

English

Let $s$ be an element of $S$. Then we can say that $\mathrm{HasMemOrInvMem}$ holds for $s$.

HasMemOrNegMemclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

no wording

English

Let $s$ be an element of $S$. Then we can say that $\mathrm{HasMemOrNegMem}$ holds for $s$.

InvMemClassclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

G is a inverse membership class (from the name)

English

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

NegMemClassclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

G is a negation membership class (from the name)

English

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

SubgroupstructureMathlib.Algebra.Group.Subgroup.Defs, type

Wording

subgroup of G (from the name)

English

Let $G$ be a set. Then the subgroups of $G$ are a basic type.

Subgroup.NormalclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

H is normal (from the name)

English

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

Subgroup.copydefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the copy of K and s (from the name)

English

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

Subgroup.inclusiondefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the inclusion homomorphism of h (from the docstring)

English

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

Subgroup.normalizerdefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the normalizer of S (from the name)

English

Let $S$ be an element of $\wp G$. Then the normalizer of $S$ is a subgroup of $G$.

Subgroup.ofClassdefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the subgroup of s (from the name)

English

Let $s$ be an element of $S$. Then the subgroup of $s$ is a subgroup of $G$.

Subgroup.ofDivdefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the subgroup of s (from the name)

English

Let $s$ be an element of $\wp G$ such that $s$ is nonempty and for all elements $x_{1}$ of $G$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $G$, if $y$ is an element of $s$, then $x_{1} \times \operatorname{inv} (y)$ is an element of $s$. Then the subgroup of $s$ is a subgroup of $G$.

Subgroup.subtypedefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the subtype of H (from the name)

English

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

SubgroupClassclassMathlib.Algebra.Group.Subgroup.Defs, predicate

Wording

G is a subgroup class (from the name)

English

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

SubgroupClass.inclusiondefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the inclusion homomorphism of h2 (from the docstring)

English

Assume that $H \leq K$. Then the inclusion homomorphism of $h_{2}$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {K}{x_{4}})}$.

SubgroupClass.subtypedefMathlib.Algebra.Group.Subgroup.Defs, function or constant

Wording

the subtype of H (from the name)

English

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

Mathlib.Algebra.Group.Subgroup.Even

AddSubgroup.evendefMathlib.Algebra.Group.Subgroup.Even, function or constant

Wording

the even of G (from the name)

English

Let $G$ be a set. Then the even of $G$ is an additive subgroup of $G$.

AddSubmonoid.evendefMathlib.Algebra.Group.Subgroup.Even, function or constant

Wording

the even of M (from the name)

English

Let $M$ be a set. Then the even of $M$ is an additive submonoid of $M$.

AddSubsemigroup.evendefMathlib.Algebra.Group.Subgroup.Even, function or constant

Wording

the even of S (from the name)

English

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

Subgroup.squaredefMathlib.Algebra.Group.Subgroup.Even, function or constant

Wording

the square of G (from the name)

English

Let $G$ be a set. Then the square of $G$ is a subgroup of $G$.

Submonoid.squaredefMathlib.Algebra.Group.Subgroup.Even, function or constant

Wording

the square of M (from the name)

English

Let $M$ be a set. Then the square of $M$ is a submonoid of $M$.

Subsemigroup.squaredefMathlib.Algebra.Group.Subgroup.Even, function or constant

Wording

the square of S (from the name)

English

Let $S$ be a set. Then the square of $S$ is a subsemigroup of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a square and the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{mul}$.

Mathlib.Algebra.Group.Subgroup.Ker

AddMonoidHom.eqLocusdefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

no wording

English

Let $f$ and $g$ be additive monoid homomorphisms of $G$ and $M$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is an additive subgroup of $G$.

AddMonoidHom.kerdefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the additive kernel of f (from the docstring)

English

Let $f$ be an additive monoid homomorphism of $G$ and $M$. Then the additive kernel of $f$ is an additive subgroup of $G$.

AddMonoidHom.ofInjectivedefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the additive monoid homomorphism of hf (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the additive monoid homomorphism of $\mathrm{hf}$ is an additive equivalence of $G$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

AddMonoidHom.ofLeftInversedefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the additive monoid homomorphism of h (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to $g$ and $\operatorname{coe}$ applied to $f$. Then the additive monoid homomorphism of $h$ is an additive equivalence of $G$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

AddMonoidHom.rangedefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be an additive monoid homomorphism of $G$ and $N$. Then the range of $f$ is an additive subgroup of $N$.

AddMonoidHom.rangeRestrictdefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $G$ and $N$. Then $\operatorname{rangeRestrict}$ applied to $f$ is an additive monoid homomorphism of $G$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

AddSubgroup.MapSubtype.orderIsodefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the order isomorphism of H (from the name)

English

Let $H$ be an additive subgroup of $G$. Then the order isomorphism of $H$ is an order isomorphism of the set of additive subgroups of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and $\SubtypeSet {\mathrm{H'}}{\mathrm{Leq} (\mathrm{H'} , H)}$.

MonoidHom.eqLocusdefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

no wording

English

Let $f$ and $g$ be monoid homomorphisms of $G$ and $M$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is a subgroup of $G$.

MonoidHom.kerdefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the multiplicative kernel of f (from the docstring)

English

Let $f$ be a monoid homomorphism of $G$ and $M$. Then the multiplicative kernel of $f$ is a subgroup of $G$.

MonoidHom.ofInjectivedefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the range of hf (from the docstring)

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the range of $\mathrm{hf}$ is a multiplicative equivalence of $G$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

MonoidHom.ofLeftInversedefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the monoid homomorphism of h (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to $g$ and $\operatorname{coe}$ applied to $f$. Then the monoid homomorphism of $h$ is a multiplicative equivalence of $G$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{2}})}$.

MonoidHom.rangedefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a monoid homomorphism of $G$ and $N$. Then the range of $f$ is a subgroup of $N$.

MonoidHom.rangeRestrictdefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

no wording

English

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

Subgroup.MapSubtype.orderIsodefMathlib.Algebra.Group.Subgroup.Ker, function or constant

Wording

the order isomorphism of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the order isomorphism of $H$ is an order isomorphism of the set of subgroups of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and $\SubtypeSet {\mathrm{H'}}{\mathrm{Leq} (\mathrm{H'} , H)}$.

Mathlib.Algebra.Group.Subgroup.Lattice

AddSubgroup.closuredefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the closure of k (from the name)

English

Let $k$ be an element of $\wp G$. Then the closure of $k$ is an additive subgroup of $G$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $K$ to $\mathrm{Leq} (k , K)$.

AddSubgroup.gidefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

no wording

English

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

AddSubgroup.toSubgroupdefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the subgroup (from the name)

English

The subgroup is an order isomorphism of the set of additive subgroups of $A$ and the set of subgroups of the set of multiplicatives of $A$.

AddSubgroup.toSubgroup'defMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the subgroup (from the name)

English

The subgroup is an order isomorphism of the set of additive subgroups of $\mathrm{Additive}$ applied to $G$ and the set of subgroups of $G$ defined as the inverse of the additive subgroup.

AddSubgroup.topEquivdefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the top additive subgroup (from the docstring)

English

The top additive subgroup is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $G$ defined as the top.

Subgroup.closuredefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the closure of k (from the name)

English

Let $k$ be an element of $\wp G$. Then the closure of $k$ is a subgroup of $G$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $K$ to $\mathrm{Leq} (k , K)$.

Subgroup.gidefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

no wording

English

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

Subgroup.toAddSubgroupdefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the additive subgroup (from the name)

English

The additive subgroup is an order isomorphism of the set of subgroups of $G$ and the set of additive subgroups of $\mathrm{Additive}$ applied to $G$.

Subgroup.toAddSubgroup'defMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the additive subgroup (from the name)

English

The additive subgroup is an order isomorphism of the set of subgroups of the set of multiplicatives of $A$ and the set of additive subgroups of $A$ defined as the inverse of the subgroup.

Subgroup.topEquivdefMathlib.Algebra.Group.Subgroup.Lattice, function or constant

Wording

the top subgroup (from the docstring)

English

The top subgroup is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $G$ defined as the top.

Mathlib.Algebra.Group.Subgroup.Map

AddEquiv.addSubgroupCongrdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the additive subgroup congruence of h (from the name)

English

Assume that $\EqtMACRoH {H}{K}$. Then the additive subgroup congruence of $h$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {K}{x_{2}})}$.

AddEquiv.addSubgroupMapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the additive subgroup map of e and H (from the name)

English

Let $e$ be an additive equivalence of $G$ and $\mathrm{G'}$. Let $H$ be an additive subgroup of $G$. Then the additive subgroup map of $e$ and $H$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{ofClass} (e), H)}{x_{3}})}$ defined as the additive submonoid map of $e$ and $\operatorname{toAddSubmonoid}$ applied to $H$.

AddEquiv.comapAddSubgroupdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the preimage additive subgroup of f (from the name)

English

Let $f$ be an additive equivalence of $G$ and $H$. Then the preimage additive subgroup of $f$ is an order isomorphism of the set of additive subgroups of $H$ and the set of additive subgroups of $G$.

AddEquiv.mapAddSubgroupdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the map additive subgroup of f (from the name)

English

Let $f$ be an additive equivalence of $G$ and $H$. Then the map additive subgroup of $f$ is an order isomorphism of the set of additive subgroups of $G$ and the set of additive subgroups of $H$.

AddMonoidHom.addSubgroupComapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the additive subgroup preimage of f and #2 (from the name)

English

Let $f$ be an additive monoid homomorphism of $G$ and $\mathrm{G'}$. Let $\mathrm{H'}$ be an additive subgroup of $\mathrm{G'}$. Then the additive subgroup preimage of $f$ and $\mathrm{H'}$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{comap} (f , \mathrm{H'})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{H'}}{x_{3}})}$ defined as the additive submonoid preimage of $f$ and $\operatorname{toAddSubmonoid}$ applied to $\mathrm{H'}$.

AddMonoidHom.addSubgroupMapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the additive subgroup map of f and H (from the name)

English

Let $f$ be an additive monoid homomorphism of $G$ and $\mathrm{G'}$. Let $H$ be an additive subgroup of $G$. Then the additive subgroup map of $f$ and $H$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , H)}{x_{3}})}$ defined as the additive submonoid map of $f$ and $\operatorname{toAddSubmonoid}$ applied to $H$.

AddSubgroup.addSubgroupOfdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the additive subgroup of H and K (from the name)

English

Let $H$ and $K$ be additive subgroups of $G$. Then the additive subgroup of $H$ and $K$ is an additive subgroup of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {K}{x_{1}})}$ defined as the preimage of the subtype of $K$ and $H$.

AddSubgroup.addSubgroupOfEquivOfLedefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the additive subgroup of h (from the name)

English

Assume that $H \leq K$. Then the additive subgroup of $h$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addSubgroupOf} (H , K)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$.

AddSubgroup.comapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the preimage of f and H (from the docstring)

English

Let $f$ be an additive monoid homomorphism of $G$ and $N$. Let $H$ be an additive subgroup of $N$. Then the preimage of $f$ and $H$ is an additive subgroup of $G$.

AddSubgroup.equivMapOfInjectivedefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

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

English

Let $H$ be an additive subgroup of $G$. Let $f$ be an additive monoid homomorphism of $G$ and $N$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $H$ and $f$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , H)}{x_{3}})}$.

AddSubgroup.mapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the map of f and H (from the name)

English

Let $f$ be an additive monoid homomorphism of $G$ and $N$. Let $H$ be an additive subgroup of $G$. Then the map of $f$ and $H$ is an additive subgroup of $N$.

MonoidHom.subgroupComapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the subgroup preimage of f and #2 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $\mathrm{G'}$. Let $\mathrm{H'}$ be a subgroup of $\mathrm{G'}$. Then the subgroup preimage of $f$ and $\mathrm{H'}$ is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{comap} (f , \mathrm{H'})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{H'}}{x_{3}})}$ defined as the submonoid preimage of $f$ and $\operatorname{toSubmonoid}$ applied to $\mathrm{H'}$.

MonoidHom.subgroupMapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the subgroup map of f and H (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $\mathrm{G'}$. Let $H$ be a subgroup of $G$. Then the subgroup map of $f$ and $H$ is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , H)}{x_{3}})}$ defined as the submonoid map of $f$ and $\operatorname{toSubmonoid}$ applied to $H$.

MulEquiv.comapSubgroupdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the preimage subgroup of f (from the name)

English

Let $f$ be a multiplicative equivalence of $G$ and $H$. Then the preimage subgroup of $f$ is an order isomorphism of the set of subgroups of $H$ and the set of subgroups of $G$.

MulEquiv.mapSubgroupdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the map subgroup of f (from the name)

English

Let $f$ be a multiplicative equivalence of $G$ and $H$. Then the map subgroup of $f$ is an order isomorphism of the set of subgroups of $G$ and the set of subgroups of $H$.

MulEquiv.subgroupCongrdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the subgroup congruence of h (from the name)

English

Assume that $\EqtMACRoH {H}{K}$. Then the subgroup congruence of $h$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {K}{x_{2}})}$.

MulEquiv.subgroupMapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the subgroup map of e and H (from the name)

English

Let $e$ be a multiplicative equivalence of $G$ and $\mathrm{G'}$. Let $H$ be a subgroup of $G$. Then the subgroup map of $e$ and $H$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{ofClass} (e), H)}{x_{3}})}$ defined as the submonoid map of $e$ and $\operatorname{toSubmonoid}$ applied to $H$.

Subgroup.comapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the preimage of f and H (from the docstring)

English

Let $f$ be a monoid homomorphism of $G$ and $N$. Let $H$ be a subgroup of $N$. Then the preimage of $f$ and $H$ is a subgroup of $G$.

Subgroup.equivMapOfInjectivedefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

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

English

Let $H$ be a subgroup of $G$. Let $f$ be a monoid homomorphism of $G$ and $N$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $H$ and $f$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , H)}{x_{3}})}$.

Subgroup.mapdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the map of f and H (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $N$. Let $H$ be a subgroup of $G$. Then the map of $f$ and $H$ is a subgroup of $N$.

Subgroup.subgroupOfdefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the subgroup of H and K (from the name)

English

Let $H$ and $K$ be subgroups of $G$. Then the subgroup of $H$ and $K$ is a subgroup of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {K}{x_{1}})}$ defined as the preimage of the subtype of $K$ and $H$.

Subgroup.subgroupOfEquivOfLedefMathlib.Algebra.Group.Subgroup.Map, function or constant

Wording

the subgroup of h (from the name)

English

Assume that $H \leq K$. Then the subgroup of $h$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{subgroupOf} (H , K)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$.

Mathlib.Algebra.Group.Subgroup.MulOpposite

AddSubgroup.equivOpdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the equivalence opposite of H (from the name)

English

Let $H$ be an additive subgroup of $G$. Then the equivalence opposite of $H$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (H)}{x_{2}})})}$.

AddSubgroup.opdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the opposite of H (from the name)

English

Let $H$ be an additive subgroup of $G$. Then the opposite of $H$ is an additive subgroup of the set of additive opposites of $G$.

AddSubgroup.opEquivdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

AddSubgroup.unopdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the opposite of H (from the name)

English

Let $H$ be an additive subgroup of the set of additive opposites of $G$. Then the opposite of $H$ is an additive subgroup of $G$.

Subgroup.equivOpdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the equivalence opposite of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the equivalence opposite of $H$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (H)}{x_{2}})})}$.

Subgroup.opdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the opposite of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the opposite of $H$ is a subgroup of the set of multiplicative opposites of $G$.

Subgroup.opEquivdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

Subgroup.unopdefMathlib.Algebra.Group.Subgroup.MulOpposite, function or constant

Wording

the opposite of H (from the name)

English

Let $H$ be a subgroup of the set of multiplicative opposites of $G$. Then the opposite of $H$ is a subgroup of $G$.

Mathlib.Algebra.Group.Subgroup.Pointwise

Subgroup.equivSMuldefMathlib.Algebra.Group.Subgroup.Pointwise, function or constant

Wording

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

English

Let $a$ be an element of $x$. Let $H$ be a subgroup of $G$. Then the equivalence product of $a$ and $H$ is a multiplicative equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(\HSMulhSMulMACRoAL {a}{H})}{x_{5}})}$ defined as the subgroup map of the multiplicative equivalence of $G$ and $a$ and $H$.

Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

AddSubgroup.zmultiplesdefMathlib.Algebra.Group.Subgroup.ZPowers.Basic, function or constant

Wording

no wording

English

Let $g$ be an element of $G$. Then $\operatorname{zmultiples}$ applied to $g$ is an additive subgroup of $G$.

Subgroup.zpowersdefMathlib.Algebra.Group.Subgroup.ZPowers.Basic, function or constant

Wording

no wording

English

Let $g$ be an element of $G$. Then $\operatorname{zpowers}$ applied to $g$ is a subgroup of $G$.

Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

AddSubgroup.zmultiplesEquivIntdefMathlib.Algebra.Group.Subgroup.ZPowers.Lemmas, function or constant

Wording

no wording

English

Assume that $a \neq 0$. Then $\operatorname{zmultiplesEquivInt}$ applied to $\mathrm{ha}$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (a)}{x_{1}})}$ and $\Integer$ defined as the inverse of the composition of the additive monoid homomorphism of $\mathrm{zmultiplesHom\_injective}$ applied to $\mathrm{ha}$ and the additive subgroup congruence of $\mathrm{AddSubgroup\_\_range\_zmultiplesHom}$ applied to $a$.

Mathlib.Algebra.Group.Submonoid.Basic

AddMonoidHom.ofClosureMEqTopLeftdefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Assume that the closure of $s$ is equal to the top. Assume that $\EqtMACRoH {f (0)}{0}$. Assume that for all elements $x_{2}$ of $M$, if $x_{2}$ is an element of $s$, then for all elements $y$ of $M$, $\EqtMACRoH {f (x_{2} + y)}{f (x_{2})+ f (y)}$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $M$ and $N$.

AddMonoidHom.ofClosureMEqTopRightdefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Assume that the closure of $s$ is equal to the top. Assume that $\EqtMACRoH {f (0)}{0}$. Assume that for all elements $x_{2}$ and $y$ of $M$, if $y$ is an element of $s$, then $\EqtMACRoH {f (x_{2} + y)}{f (x_{2})+ f (y)}$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $M$ and $N$.

AddSubmonoid.closuredefMathlib.Algebra.Group.Submonoid.Basic, 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 submonoid of $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Leq} (s , S)$.

AddSubmonoid.gidefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

no wording

English

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

IsAddUnit.addSubmonoiddefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

the additive submonoid consisting of the additive units of M (from the docstring)

English

Let $M$ be a set. Then the additive submonoid consisting of the additive units of $M$ is an additive submonoid of $M$.

IsUnit.submonoiddefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

the submonoid consisting of the units of M (from the docstring)

English

Let $M$ be a set. Then the submonoid consisting of the units of $M$ is a submonoid of $M$.

MonoidHom.ofClosureMEqTopLeftdefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

the monoid homomorphism of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Assume that the closure of $s$ is equal to the top. Assume that $\EqtMACRoH {f (1)}{1}$. Assume that for all elements $x_{2}$ of $M$, if $x_{2}$ is an element of $s$, then for all elements $y$ of $M$, $\EqtMACRoH {f (x_{2} \times y)}{f (x_{2})\times f (y)}$. Then the monoid homomorphism of $f$ is a monoid homomorphism of $M$ and $N$.

MonoidHom.ofClosureMEqTopRightdefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

the monoid homomorphism of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Assume that the closure of $s$ is equal to the top. Assume that $\EqtMACRoH {f (1)}{1}$. Assume that for all elements $x_{2}$ and $y$ of $M$, if $y$ is an element of $s$, then $\EqtMACRoH {f (x_{2} \times y)}{f (x_{2})\times f (y)}$. Then the monoid homomorphism of $f$ is a monoid homomorphism of $M$ and $N$.

Submonoid.closuredefMathlib.Algebra.Group.Submonoid.Basic, 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 submonoid of $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Leq} (s , S)$.

Submonoid.gidefMathlib.Algebra.Group.Submonoid.Basic, function or constant

Wording

no wording

English

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

Mathlib.Algebra.Group.Submonoid.Defs

AddMonoidHom.eqLocusMdefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

no wording

English

Let $f$ and $g$ be additive monoid homomorphisms of $M$ and $N$. Then $\operatorname{eqLocusM}$ applied to $f$ and $g$ is an additive submonoid of $M$.

AddSubmonoidstructureMathlib.Algebra.Group.Submonoid.Defs, type

Wording

additive submonoid of M (from the name)

English

Let $M$ be a set. Then the additive submonoids of $M$ are a basic type.

AddSubmonoid.copydefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the copy of S and s (from the name)

English

Let $S$ be an additive submonoid of $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{S}$. Then the copy of $S$ and $s$ is an additive submonoid of $M$.

AddSubmonoid.ofClassdefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the additive submonoid of s (from the name)

English

Let $s$ be an element of $S$. Then the additive submonoid of $s$ is an additive submonoid of $M$.

AddSubmonoid.subtypedefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the subtype of S (from the name)

English

Let $S$ be an additive submonoid of $M$. Then the subtype of $S$ is an additive monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $M$.

AddSubmonoidClassclassMathlib.Algebra.Group.Submonoid.Defs, predicate

Wording

M is a additive submonoid class (from the name)

English

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

AddSubmonoidClass.subtypedefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the subtype of #1 (from the name)

English

Let $\mathrm{S'}$ be an element of $A$. Then the subtype of $\mathrm{S'}$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{S'}}{x_{2}})}$ and $M$.

MonoidHom.eqLocusMdefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

no wording

English

Let $f$ and $g$ be monoid homomorphisms of $M$ and $N$. Then $\operatorname{eqLocusM}$ applied to $f$ and $g$ is a submonoid of $M$.

OneMemClassclassMathlib.Algebra.Group.Submonoid.Defs, predicate

Wording

M is a one membership class (from the name)

English

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

SubmonoidstructureMathlib.Algebra.Group.Submonoid.Defs, type

Wording

submonoid of M (from the name)

English

Let $M$ be a set. Then the submonoids of $M$ are a basic type.

Submonoid.copydefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the copy of S and s (from the name)

English

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

Submonoid.ofClassdefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the submonoid of s (from the name)

English

Let $s$ be an element of $S$. Then the submonoid of $s$ is a submonoid of $M$.

Submonoid.subtypedefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the subtype of S (from the name)

English

Let $S$ be a submonoid of $M$. Then the subtype of $S$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $M$.

SubmonoidClassclassMathlib.Algebra.Group.Submonoid.Defs, predicate

Wording

M is a submonoid class (from the name)

English

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

SubmonoidClass.subtypedefMathlib.Algebra.Group.Submonoid.Defs, function or constant

Wording

the subtype of #1 (from the name)

English

Let $\mathrm{S'}$ be an element of $A$. Then the subtype of $\mathrm{S'}$ is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{S'}}{x_{2}})}$ and $M$.

ZeroMemClassclassMathlib.Algebra.Group.Submonoid.Defs, predicate

Wording

M is a zero membership class (from the name)

English

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

Mathlib.Algebra.Group.Submonoid.Membership

AddSubmonoid.multiplesdefMathlib.Algebra.Group.Submonoid.Membership, function or constant

Wording

the multiple of x1 (from the name)

English

Let $x_{1}$ be an element of $A$. Then the multiple of $x_{1}$ is an additive submonoid of $A$.

Submonoid.logdefMathlib.Algebra.Group.Submonoid.Membership, function or constant

Wording

the logarithm of p (from the name)

English

Let $p$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{powers} (n)}{x_{2}})}$. Then the logarithm of $p$ is an element of $\Natural$.

Submonoid.powdefMathlib.Algebra.Group.Submonoid.Membership, function or constant

Wording

the power of n and m (from the name)

English

Let $n$ be an element of $M$. Let $m$ be an element of $\Natural$. Then the power of $n$ and $m$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{powers} (n)}{x_{1}})}$ defined as $\operatorname{mrangeRestrict}$ applied to $\operatorname{powersHom}$ applied to $M$ and $n$ and $\operatorname{ofAdd}$ applied to $m$.

Submonoid.powLogEquivdefMathlib.Algebra.Group.Submonoid.Membership, function or constant

Wording

the power logarithm equivalence of h (from the name)

English

Assume that the function that maps $m$ to $n ^ {m}$ is injective. Then the power logarithm equivalence of $h$ is a multiplicative equivalence of the set of multiplicatives of $\Natural$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{powers} (n)}{x_{2}})}$.

Submonoid.powersdefMathlib.Algebra.Group.Submonoid.Membership, function or constant

Wording

the power of n (from the name)

English

Let $n$ be an element of $M$. Then the power of $n$ is a submonoid of $M$.

Mathlib.Algebra.Group.Submonoid.MulOpposite

AddSubmonoid.equivOpdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the equivalence opposite of H (from the name)

English

Let $H$ be an additive submonoid of $M$. Then the equivalence opposite of $H$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (H)}{x_{2}})})}$.

AddSubmonoid.opdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be an additive submonoid of $M$. Then the opposite of $x_{1}$ is an additive submonoid of the set of additive opposites of $M$.

AddSubmonoid.opEquivdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

AddSubmonoid.unopdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be an additive submonoid of the set of additive opposites of $M$. Then the opposite of $x_{1}$ is an additive submonoid of $M$.

Submonoid.equivOpdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the equivalence opposite of H (from the name)

English

Let $H$ be a submonoid of $M$. Then the equivalence opposite of $H$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (H)}{x_{2}})})}$.

Submonoid.opdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a submonoid of $M$. Then the opposite of $x_{1}$ is a submonoid of the set of multiplicative opposites of $M$.

Submonoid.opEquivdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

Submonoid.unopdefMathlib.Algebra.Group.Submonoid.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a submonoid of the set of multiplicative opposites of $M$. Then the opposite of $x_{1}$ is a submonoid of $M$.

Mathlib.Algebra.Group.Submonoid.Operations

AddEquiv.addSubmonoidCongrdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the additive submonoid congruence of h (from the name)

English

Assume that $\EqtMACRoH {S}{T}$. Then the additive submonoid congruence of $h$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$.

AddEquiv.addSubmonoidMapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the additive submonoid map of e and S (from the name)

English

Let $e$ be an additive equivalence of $M$ and $N$. Let $S$ be an additive submonoid of $M$. Then the additive submonoid map of $e$ and $S$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (e , S)}{x_{3}})}$.

AddEquiv.ofLeftInverse'defMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

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

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the additive equivalence of $f$ and $h$ is an additive equivalence of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (f)}{x_{2}})}$.

AddMonoidHom.addSubmonoidComapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the additive submonoid preimage of f and #2 (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $\mathrm{N'}$ be an additive submonoid of $N$. Then the additive submonoid preimage of $f$ and $\mathrm{N'}$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{comap} (f , \mathrm{N'})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{3}})}$.

AddMonoidHom.addSubmonoidMapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the additive submonoid map of f and #2 (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $\mathrm{M'}$ be an additive submonoid of $M$. Then the additive submonoid map of $f$ and $\mathrm{M'}$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , \mathrm{M'})}{x_{3}})}$.

AddMonoidHom.codRestrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $s$ be an element of $S$ such that for all elements $x_{4}$ of $M$, $\MembershipmemMACRoT {s}{f (x_{4})}$. Then $\operatorname{codRestrict}$ applied to $f$, $s$ and $h_{1}$ is an additive monoid homomorphism of $M$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$.

AddMonoidHom.domRestrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $s$ be an element of $S$. Then $\operatorname{domRestrict}$ applied to $f$ and $s$ is an additive monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ and $N$ defined as the composition of $f$ and the subtype of $s$.

AddMonoidHom.domRestrictHomdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $\mathrm{M'}$ be an element of $S$. Let $A$ be a set. Then $\operatorname{domRestrictHom}$ applied to $\mathrm{M'}$ and $A$ is an additive monoid homomorphism of the set of additive monoid homomorphisms of $M$ and $A$ and the set of additive monoid homomorphisms of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{3}})}$ and $A$.

AddMonoidHom.mkerdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an element of $F$. Then $\operatorname{mker}$ applied to $f$ is an additive submonoid of $M$ defined as the preimage of $f$ and the bottom.

AddMonoidHom.mrangedefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an element of $F$. Then $\operatorname{mrange}$ applied to $f$ is an additive submonoid of $N$.

AddMonoidHom.mrangeRestrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then $\operatorname{mrangeRestrict}$ applied to $f$ is an additive monoid homomorphism of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (f)}{x_{2}})}$.

AddMonoidHom.restrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Assume that $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to $f$, $\mathrm{M'}$ and $\mathrm{N'}$. Then $\operatorname{restrict}$ applied to $h$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{3}})}$.

AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoiddefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

$\operatorname{addUnitsTypeEquivIsAddUnitAddSubmonoid}$ is an additive equivalence of the set of additive units of $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addSubmonoid} (M)}{x_{1}})}$.

AddSubmonoid.comapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the preimage of f and S (from the docstring)

English

Let $f$ be an element of $F$. Let $S$ be an additive submonoid of $N$. Then the preimage of $f$ and $S$ is an additive submonoid of $M$.

AddSubmonoid.equivMapOfInjectivedefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

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

English

Let $S$ be an additive submonoid of $M$. Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $S$ and $f$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , S)}{x_{3}})}$.

AddSubmonoid.gciMapComapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{gciMapComap}$ applied to $\mathrm{hf}$ is a Galois coinsertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

AddSubmonoid.giMapComapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then $\operatorname{giMapComap}$ applied to $\mathrm{hf}$ is a Galois insertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

AddSubmonoid.inclusiondefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the inclusion of h (from the name)

English

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

AddSubmonoid.mapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the map of f and S (from the name)

English

Let $f$ be an element of $F$. Let $S$ be an additive submonoid of $M$. Then the map of $f$ and $S$ is an additive submonoid of $N$.

AddSubmonoid.pidefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the product of I and S (from the name)

English

Let $I$ be an element of $\wp x$. Let $S$ be a function from elements $i_{1}$ of $x$ to additive submonoids of $M$ applied to $i_{1}$. Then the product of $I$ and $i_{1}$ is an additive submonoid of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$.

AddSubmonoid.proddefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be an additive submonoid of $M$. Let $t$ be an additive submonoid of $N$. Then the product of $s$ and $t$ is an additive submonoid of $\mathrm{Prod}$ applied to $M$ and $N$.

AddSubmonoid.prodEquivdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

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

English

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

AddSubmonoid.toSubmonoiddefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the submonoid (from the name)

English

The submonoid is an order isomorphism of the set of additive submonoids of $A$ and the set of submonoids of the set of multiplicatives of $A$.

AddSubmonoid.toSubmonoid'defMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the submonoid (from the name)

English

The submonoid is an order isomorphism of the set of additive submonoids of $\mathrm{Additive}$ applied to $M$ and the set of submonoids of $M$ defined as the inverse of the additive submonoid.

AddSubmonoid.topEquivdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the top (from the docstring)

English

The top is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $M$.

LibraryNote.range_copy_patterndefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the range copy pattern (from the name)

English

The range copy pattern is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

MonoidHom.codRestrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

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

MonoidHom.domRestrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

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

MonoidHom.domRestrictHomdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $\mathrm{M'}$ be an element of $S$. Let $A$ be a set. Then $\operatorname{domRestrictHom}$ applied to $\mathrm{M'}$ and $A$ is a monoid homomorphism of the set of monoid homomorphisms of $M$ and $A$ and the set of monoid homomorphisms of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{3}})}$ and $A$.

MonoidHom.mkerdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an element of $F$. Then $\operatorname{mker}$ applied to $f$ is a submonoid of $M$ defined as the preimage of $f$ and the bottom.

MonoidHom.mrangedefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be an element of $F$. Then $\operatorname{mrange}$ applied to $f$ is a submonoid of $N$.

MonoidHom.mrangeRestrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Then $\operatorname{mrangeRestrict}$ applied to $f$ is a monoid homomorphism of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (f)}{x_{2}})}$.

MonoidHom.restrictdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Assume that $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to $f$, $\mathrm{M'}$ and $\mathrm{N'}$. Then $\operatorname{restrict}$ applied to $h$ is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{3}})}$.

MonoidHom.submonoidComapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the submonoid preimage of f and #2 (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Let $\mathrm{N'}$ be a submonoid of $N$. Then the submonoid preimage of $f$ and $\mathrm{N'}$ is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{comap} (f , \mathrm{N'})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{3}})}$.

MonoidHom.submonoidMapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the submonoid map of f and #2 (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Let $\mathrm{M'}$ be a submonoid of $M$. Then the submonoid map of $f$ and $\mathrm{M'}$ is a monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , \mathrm{M'})}{x_{3}})}$.

MulEquiv.ofLeftInverse'defMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

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

English

Let $f$ be a monoid homomorphism of $M$ and $N$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the multiplicative equivalence of $f$ and $h$ is a multiplicative equivalence of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (f)}{x_{2}})}$.

MulEquiv.submonoidCongrdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the submonoid congruence of h (from the name)

English

Assume that $\EqtMACRoH {S}{T}$. Then the submonoid congruence of $h$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$.

MulEquiv.submonoidMapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the submonoid map of e and S (from the name)

English

Let $e$ be a multiplicative equivalence of $M$ and $N$. Let $S$ be a submonoid of $M$. Then the submonoid map of $e$ and $S$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (e , S)}{x_{3}})}$.

Submonoid.comapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the preimage of f and S (from the docstring)

English

Let $f$ be an element of $F$. Let $S$ be a submonoid of $N$. Then the preimage of $f$ and $S$ is a submonoid of $M$.

Submonoid.equivMapOfInjectivedefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

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

English

Let $S$ be a submonoid of $M$. Let $f$ be a monoid homomorphism of $M$ and $N$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $S$ and $f$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , S)}{x_{3}})}$.

Submonoid.gciMapComapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Submonoid.giMapComapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

Submonoid.inclusiondefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the inclusion of h (from the name)

English

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

Submonoid.mapdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the map of f and S (from the name)

English

Let $f$ be an element of $F$. Let $S$ be a submonoid of $M$. Then the map of $f$ and $S$ is a submonoid of $N$.

Submonoid.pidefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the product of I and S (from the name)

English

Let $I$ be an element of $\wp x$. Let $S$ be a function from elements $i_{1}$ of $x$ to submonoids of $M$ applied to $i_{1}$. Then the product of $I$ and $i_{1}$ is a submonoid of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$.

Submonoid.proddefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a submonoid of $M$. Let $t$ be a submonoid of $N$. Then the product of $s$ and $t$ is a submonoid of $\mathrm{Prod}$ applied to $M$ and $N$.

Submonoid.prodEquivdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

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

English

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

Submonoid.toAddSubmonoiddefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the additive submonoid (from the name)

English

The additive submonoid is an order isomorphism of the set of submonoids of $M$ and the set of additive submonoids of $\mathrm{Additive}$ applied to $M$.

Submonoid.toAddSubmonoid'defMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the additive submonoid (from the name)

English

The additive submonoid is an order isomorphism of the set of submonoids of the set of multiplicatives of $A$ and the set of additive submonoids of $A$ defined as the inverse of the submonoid.

Submonoid.topEquivdefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

the top (from the docstring)

English

The top is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $M$.

Submonoid.unitsTypeEquivIsUnitSubmonoiddefMathlib.Algebra.Group.Submonoid.Operations, function or constant

Wording

no wording

English

$\operatorname{unitsTypeEquivIsUnitSubmonoid}$ is a multiplicative equivalence of $\UnitsMACRoAO {M}$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{submonoid} (M)}{x_{1}})}$.

Mathlib.Algebra.Group.Submonoid.Pointwise

AddSubmonoid.negOrderIsodefMathlib.Algebra.Group.Submonoid.Pointwise, function or constant

Wording

the negation order isomorphism (from the name)

English

The negation order isomorphism is an order isomorphism of the set of additive submonoids of $G$ and the set of additive submonoids of $G$ defined as $\operatorname{mk}$ applied to the negation of the set of additive submonoids of $G$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{AddSubmonoid\_\_neg\_le\_neg}$ applied to $x_{1}$ and $x_{2}$.

Submonoid.invOrderIsodefMathlib.Algebra.Group.Submonoid.Pointwise, function or constant

Wording

the inverse order isomorphism (from the name)

English

The inverse order isomorphism is an order isomorphism of the set of submonoids of $G$ and the set of submonoids of $G$ defined as $\operatorname{mk}$ applied to the inverse of the set of submonoids of $G$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Submonoid\_\_inv\_le\_inv}$ applied to $x_{1}$ and $x_{2}$.

Mathlib.Algebra.Group.Submonoid.Saturation

AddSubmonoid.AddSaturateddefMathlib.Algebra.Group.Submonoid.Saturation, predicate

Wording

no wording

English

Let $s$ be an additive submonoid of $M$. Then $\operatorname{AddSaturated}$ holds for $s$, if for all elements $x_{1}$ and $y$ of $M$, if $x_{1} + y$ is an element of $s$, then $x_{1}$ is an element of $s$ and $y$ is an element of $s$.

AddSubmonoid.giSaturationdefMathlib.Algebra.Group.Submonoid.Saturation, function or constant

Wording

no wording

English

Let $M$ be a set. Then $\operatorname{giSaturation}$ applied to $M$ is a Galois insertion of $\operatorname{saturation}$ and the function that maps $x_{1}$ to $\operatorname{toAddSubmonoid}$ applied to $x_{1}$.

AddSubmonoid.saturationdefMathlib.Algebra.Group.Submonoid.Saturation, function or constant

Wording

the saturation of s (from the docstring)

English

Let $s$ be an additive submonoid of $M$. Then the saturation of $s$ is a saturated additive submonoid of $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Leq} (s , \operatorname{toAddSubmonoid} (t))$.

SaturatedAddSubmonoidstructureMathlib.Algebra.Group.Submonoid.Saturation, type

Wording

saturated additive submonoid of M (from the name)

English

Let $M$ be a set. Then the saturated additive submonoids of $M$ are a basic type.

SaturatedSubmonoidstructureMathlib.Algebra.Group.Submonoid.Saturation, type

Wording

saturated submonoid of M (from the name)

English

Let $M$ be a set. Then the saturated submonoids of $M$ are a basic type.

Submonoid.MulSaturateddefMathlib.Algebra.Group.Submonoid.Saturation, predicate

Wording

no wording

English

Let $s$ be a submonoid of $M$. Then $\operatorname{MulSaturated}$ holds for $s$, if for all elements $x_{1}$ and $y$ of $M$, if $x_{1} \times y$ is an element of $s$, then $x_{1}$ is an element of $s$ and $y$ is an element of $s$.

Submonoid.giSaturationdefMathlib.Algebra.Group.Submonoid.Saturation, function or constant

Wording

no wording

English

Submonoid.saturationdefMathlib.Algebra.Group.Submonoid.Saturation, function or constant

Wording

the saturation of s (from the docstring)

English

Let $s$ be a submonoid of $M$. Then the saturation of $s$ is a saturated submonoid of $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Leq} (s , \operatorname{toSubmonoid} (t))$.

Mathlib.Algebra.Group.Submonoid.Support

AddSubgroup.gciToAddSubmonoidSupportdefMathlib.Algebra.Group.Submonoid.Support, function or constant

Wording

the support (from the docstring)

English

The support is a Galois coinsertion of $\operatorname{toAddSubmonoid}$ and $\operatorname{support}$.

AddSubmonoid.IsPointeddefMathlib.Algebra.Group.Submonoid.Support, predicate

Wording

M is pointed (from the docstring)

English

Let $M$ be an additive submonoid of $G$. Then $M$ is pointed, if for all elements $x_{1}$ of $G$, if $x_{1}$ is an element of $M$, then if $\MembershipmemMACRoT {M}{\operatorname{neg} (x_{1})}$, then $\EqtMACRoH {x_{1}}{0}$.

AddSubmonoid.IsSpanningdefMathlib.Algebra.Group.Submonoid.Support, predicate

Wording

M is a spanning (from the name)

English

Let $M$ be an additive submonoid of $G$. Then $M$ is a spanning, if for all elements $a$ of $G$, $a$ is an element of $M$ or $\MembershipmemMACRoT {M}{\operatorname{neg} (a)}$.

AddSubmonoid.supportdefMathlib.Algebra.Group.Submonoid.Support, function or constant

Wording

the support of M (from the docstring)

English

Let $M$ be an additive submonoid of $G$. Then the support of $M$ is an additive subgroup of $G$.

Subgroup.gciToSubmonoidMulSupportdefMathlib.Algebra.Group.Submonoid.Support, function or constant

Wording

the support (from the docstring)

English

The support is a Galois coinsertion of $\operatorname{toSubmonoid}$ and $\operatorname{mulSupport}$.

Submonoid.IsMulPointeddefMathlib.Algebra.Group.Submonoid.Support, predicate

Wording

M is pointed (from the docstring)

English

Let $M$ be a submonoid of $G$. Then $M$ is pointed, if for all elements $x_{1}$ of $G$, if $x_{1}$ is an element of $M$, then if $\MembershipmemMACRoT {M}{\operatorname{inv} (x_{1})}$, then $\EqtMACRoH {x_{1}}{1}$.

Submonoid.IsMulSpanningdefMathlib.Algebra.Group.Submonoid.Support, predicate

Wording

M is a multiplicative spanning (from the name)

English

Let $M$ be a submonoid of $G$. Then $M$ is a multiplicative spanning, if for all elements $a$ of $G$, $a$ is an element of $M$ or $\MembershipmemMACRoT {M}{\operatorname{inv} (a)}$.

Submonoid.mulSupportdefMathlib.Algebra.Group.Submonoid.Support, function or constant

Wording

the support of M (from the docstring)

English

Let $M$ be a submonoid of $G$. Then the support of $M$ is a subgroup of $G$.

Mathlib.Algebra.Group.Submonoid.Units

AddSubgroup.addUnit_of_mem_ofAddUnitsdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the additive unit of S and h (from the name)

English

Let $S$ be an additive subgroup of the set of additive units of $M$ such that $x_{1}$ is an element of the additive subgroup of $S$. Then the additive unit of $S$ and $h$ is an additive unit of $M$.

AddSubgroup.addUnitsEquivSelfdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the additive unit equivalence self of H (from the name)

English

Let $H$ be an additive subgroup of $G$. Then the additive unit equivalence self of $H$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addUnits} (\operatorname{toAddSubmonoid} (H))}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ defined as the composition of the additive unit equivalence additive unit type of $\operatorname{toAddSubmonoid}$ applied to $H$ and the inverse of the additive unit.

AddSubgroup.ofAddUnitsdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the additive subgroup of S (from the name)

English

Let $S$ be an additive subgroup of the set of additive units of $M$. Then the additive subgroup of $S$ is an additive submonoid of $M$ defined as the map of the coercion homomorphism of $M$ and $\operatorname{toAddSubmonoid}$ applied to $S$.

AddSubgroup.ofAddUnitsEquivTypedefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the equivalence between the coercion of S (from the docstring)

English

Let $S$ be an additive subgroup of the set of additive units of $M$. Then the equivalence between the coercion of $S$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ofAddUnits} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

AddSubgroup.ofAddUnitsTopEquivdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the additive subgroup (from the name)

English

The additive subgroup is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ofAddUnits} (\operatorname{top})}{x_{1}})}$ and the set of additive units of $M$ defined as the composition of the equivalence between the coercion of the top and the top additive subgroup.

AddSubmonoid.addUnitsdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the additive unit of S (from the name)

English

Let $S$ be an additive submonoid of $M$. Then the additive unit of $S$ is an additive subgroup of the set of additive units of $M$.

AddSubmonoid.addUnitsEquivAddUnitsTypedefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the additive unit equivalence additive unit type of S (from the name)

English

Let $S$ be an additive submonoid of $M$. Then the additive unit equivalence additive unit type of $S$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addUnits} (S)}{x_{1}})}$ and the set of additive units of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

AddSubmonoid.addUnitsEquivIsAddUnitAddSubmonoiddefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

no wording

English

Let $S$ be an additive submonoid of $M$. Then $\operatorname{addUnitsEquivIsAddUnitAddSubmonoid}$ applied to $S$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addUnits} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{addSubmonoid} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})})}{x_{2}})}$ defined as the composition of the additive unit equivalence additive unit type of $S$ and $\operatorname{addUnitsTypeEquivIsAddUnitAddSubmonoid}$.

Subgroup.ofUnitsdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the subgroup of S (from the name)

English

Let $S$ be a subgroup of $\UnitsMACRoAO {M}$. Then the subgroup of $S$ is a submonoid of $M$ defined as the map of the coercion homomorphism of $M$ and $\operatorname{toSubmonoid}$ applied to $S$.

Subgroup.ofUnitsEquivTypedefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the equivalence between the coercion of S (from the docstring)

English

Let $S$ be a subgroup of $\UnitsMACRoAO {M}$. Then the equivalence between the coercion of $S$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ofUnits} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

Subgroup.ofUnitsTopEquivdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the subgroup (from the name)

English

The subgroup is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ofUnits} (\operatorname{top})}{x_{1}})}$ and $\UnitsMACRoAO {M}$ defined as the composition of the equivalence between the coercion of the top and the top subgroup.

Subgroup.unit_of_mem_ofUnitsdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the unit of S and h (from the name)

English

Let $S$ be a subgroup of $\UnitsMACRoAO {M}$ such that $x_{1}$ is an element of the subgroup of $S$. Then the unit of $S$ and $h$ is a unit of $M$.

Subgroup.unitsEquivSelfdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the unit equivalence self of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the unit equivalence self of $H$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{units} (\operatorname{toSubmonoid} (H))}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ defined as the composition of the unit equivalence unit type of $\operatorname{toSubmonoid}$ applied to $H$ and the inverse of the unit.

Submonoid.unitsdefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the unit of S (from the name)

English

Let $S$ be a submonoid of $M$. Then the unit of $S$ is a subgroup of $\UnitsMACRoAO {M}$.

Submonoid.unitsEquivIsUnitSubmonoiddefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $M$. Then $\operatorname{unitsEquivIsUnitSubmonoid}$ applied to $S$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{units} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{submonoid} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})})}{x_{2}})}$ defined as the composition of the unit equivalence unit type of $S$ and $\operatorname{unitsTypeEquivIsUnitSubmonoid}$.

Submonoid.unitsEquivUnitsTypedefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

the unit equivalence unit type of S (from the name)

English

Let $S$ be a submonoid of $M$. Then the unit equivalence unit type of $S$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{units} (S)}{x_{1}})}$ and $\UnitsMACRoAO {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})})}$.

ofAddUnits_addUnits_gcidefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

no wording

English

$\mathrm{ofAddUnits\_addUnits\_gci}$ is a Galois coinsertion of $\operatorname{ofAddUnits}$ and $\operatorname{addUnits}$ defined as the monotone intro of $\mathrm{AddSubmonoid\_\_ofAddUnits\_addUnits\_le}$ and $\mathrm{AddSubgroup\_\_addUnits\_ofAddUnits\_eq}$.

ofUnits_units_gcidefMathlib.Algebra.Group.Submonoid.Units, function or constant

Wording

no wording

English

$\mathrm{ofUnits\_units\_gci}$ is a Galois coinsertion of $\operatorname{ofUnits}$ and $\operatorname{units}$ defined as the monotone intro of $\mathrm{Submonoid\_\_ofUnits\_units\_le}$ and $\mathrm{Subgroup\_\_units\_ofUnits\_eq}$.

Mathlib.Algebra.Group.Subsemigroup.Basic

AddHom.ofDensedefMathlib.Algebra.Group.Subsemigroup.Basic, function or constant

Wording

the additive homomorphism of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Assume that the closure of $s$ is equal to the top. Assume that for all elements $x_{2}$ and $y$ of $M$, if $y$ is an element of $s$, then $\EqtMACRoH {f (x_{2} + y)}{f (x_{2})+ f (y)}$. Then the additive homomorphism of $f$ is an additive homomorphism of $M$ and $N$.

AddSubsemigroup.closuredefMathlib.Algebra.Group.Subsemigroup.Basic, 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 subsemigroup of $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Leq} (s , S)$.

AddSubsemigroup.gidefMathlib.Algebra.Group.Subsemigroup.Basic, function or constant

Wording

no wording

English

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

MulHom.ofDensedefMathlib.Algebra.Group.Subsemigroup.Basic, function or constant

Wording

the multiplicative homomorphism of f (from the name)

English

Let $f$ be a function from elements of $M$ to elements of $N$. Assume that the closure of $s$ is equal to the top. Assume that for all elements $x_{2}$ and $y$ of $M$, if $y$ is an element of $s$, then $\EqtMACRoH {f (x_{2} \times y)}{f (x_{2})\times f (y)}$. Then the multiplicative homomorphism of $f$ is a multiplicative homomorphism of $M$ and $N$.

Subsemigroup.closuredefMathlib.Algebra.Group.Subsemigroup.Basic, 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 subsemigroup of $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Leq} (s , S)$.

Subsemigroup.gidefMathlib.Algebra.Group.Subsemigroup.Basic, function or constant

Wording

no wording

English

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

Mathlib.Algebra.Group.Subsemigroup.Defs

AddHom.eqLocusdefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

no wording

English

Let $f$ and $g$ be additive homomorphisms of $M$ and $N$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is an additive subsemigroup of $M$.

AddMemClassclassMathlib.Algebra.Group.Subsemigroup.Defs, predicate

Wording

M is a additive membership class (from the name)

English

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

AddMemClass.subtypedefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the subtype of #1 (from the name)

English

Let $\mathrm{S'}$ be an element of $A$. Then the subtype of $\mathrm{S'}$ is an additive homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{S'}}{x_{2}})}$ and $M$.

AddSubsemigroupstructureMathlib.Algebra.Group.Subsemigroup.Defs, type

Wording

additive subsemigroup of M (from the name)

English

Let $M$ be a set. Then the additive subsemigroups of $M$ are a basic type.

AddSubsemigroup.carrierdefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the carrier of self (from the docstring)

English

Let $\mathrm{self}$ be an additive subsemigroup of $M$. Then the carrier of $\mathrm{self}$ is an element of $\wp M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AddSubsemigroup.copydefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the copy of S and s (from the name)

English

Let $S$ be an additive subsemigroup of $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{S}$. Then the copy of $S$ and $s$ is an additive subsemigroup of $M$.

AddSubsemigroup.ofClassdefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the additive subsemigroup of s (from the name)

English

Let $s$ be an element of $S$. Then the additive subsemigroup of $s$ is an additive subsemigroup of $M$ defined as $\operatorname{mk}$ applied to $s$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{AddMemClass\_\_add\_mem}$.

MulHom.eqLocusdefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

no wording

English

Let $f$ and $g$ be multiplicative homomorphisms of $M$ and $N$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is a subsemigroup of $M$.

MulMemClassclassMathlib.Algebra.Group.Subsemigroup.Defs, predicate

Wording

M is a multiplicative membership class (from the name)

English

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

MulMemClass.subtypedefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the subtype of #1 (from the name)

English

Let $\mathrm{S'}$ be an element of $A$. Then the subtype of $\mathrm{S'}$ is a multiplicative homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{S'}}{x_{2}})}$ and $M$.

SubsemigroupstructureMathlib.Algebra.Group.Subsemigroup.Defs, type

Wording

subsemigroup of M (from the name)

English

Let $M$ be a set. Then the subsemigroups of $M$ are a basic type.

Subsemigroup.carrierdefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the carrier of self (from the docstring)

English

Let $\mathrm{self}$ be a subsemigroup of $M$. Then the carrier of $\mathrm{self}$ is an element of $\wp M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Subsemigroup.copydefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the copy of S and s (from the name)

English

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

Subsemigroup.ofClassdefMathlib.Algebra.Group.Subsemigroup.Defs, function or constant

Wording

the subsemigroup of s (from the name)

English

Let $s$ be an element of $S$. Then the subsemigroup of $s$ is a subsemigroup of $M$ defined as $\operatorname{mk}$ applied to $s$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{MulMemClass\_\_mul\_mem}$.

Mathlib.Algebra.Group.Subsemigroup.MulOpposite

AddSubsemigroup.equivOpdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the equivalence opposite of H (from the name)

English

Let $H$ be an additive subsemigroup of $M$. Then the equivalence opposite of $H$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (H)}{x_{2}})})}$.

AddSubsemigroup.opdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be an additive subsemigroup of $M$. Then the opposite of $x_{1}$ is an additive subsemigroup of the set of additive opposites of $M$.

AddSubsemigroup.opEquivdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

AddSubsemigroup.unopdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be an additive subsemigroup of the set of additive opposites of $M$. Then the opposite of $x_{1}$ is an additive subsemigroup of $M$.

Subsemigroup.equivOpdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the equivalence opposite of H (from the name)

English

Let $H$ be a subsemigroup of $M$. Then the equivalence opposite of $H$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{op} (H)}{x_{2}})})}$.

Subsemigroup.opdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a subsemigroup of $M$. Then the opposite of $x_{1}$ is a subsemigroup of the set of multiplicative opposites of $M$.

Subsemigroup.opEquivdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

Subsemigroup.unopdefMathlib.Algebra.Group.Subsemigroup.MulOpposite, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a subsemigroup of the set of multiplicative opposites of $M$. Then the opposite of $x_{1}$ is a subsemigroup of $M$.

Mathlib.Algebra.Group.Subsemigroup.Operations

AddEquiv.ofLeftInversedefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

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

English

Let $f$ be an additive homomorphism of $M$ and $N$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the additive equivalence of $f$ and $h$ is an additive equivalence of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{srange} (f)}{x_{2}})}$.

AddEquiv.subsemigroupCongrdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup congruence of h (from the name)

English

Assume that $\EqtMACRoH {S}{T}$. Then the subsemigroup congruence of $h$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$.

AddEquiv.subsemigroupMapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup map of e and S (from the name)

English

Let $e$ be an additive equivalence of $M$ and $N$. Let $S$ be an additive subsemigroup of $M$. Then the subsemigroup map of $e$ and $S$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toAddHom} (e), S)}{x_{3}})}$.

AddHom.codRestrictdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $S$ be an element of $x$ such that for all elements $x_{5}$ of $M$, $\MembershipmemMACRoT {S}{f (x_{5})}$. Then $\operatorname{codRestrict}$ applied to $f$, $S$ and $h_{1}$ is an additive homomorphism of $M$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$.

AddHom.domRestrictdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $S$ be an element of $x$. Then $\operatorname{domRestrict}$ applied to $f$ and $S$ is an additive homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and $N$ defined as the composition of $f$ and the subtype of $S$.

AddHom.srangedefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

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

AddHom.srangeRestrictdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Let $f$ be an additive homomorphism of $M$ and $N$. Then $\operatorname{srangeRestrict}$ applied to $f$ is an additive homomorphism of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{srange} (f)}{x_{2}})}$.

AddHom.subsemigroupComapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup preimage of f and #2 (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $\mathrm{N'}$ be an additive subsemigroup of $N$. Then the subsemigroup preimage of $f$ and $\mathrm{N'}$ is an additive homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{comap} (f , \mathrm{N'})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{3}})}$.

AddHom.subsemigroupMapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup map of f and #2 (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $\mathrm{M'}$ be an additive subsemigroup of $M$. Then the subsemigroup map of $f$ and $\mathrm{M'}$ is an additive homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , \mathrm{M'})}{x_{3}})}$.

AddSubsemigroup.comapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the preimage of f and S (from the docstring)

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $S$ be an additive subsemigroup of $N$. Then the preimage of $f$ and $S$ is an additive subsemigroup of $M$.

AddSubsemigroup.equivMapOfInjectivedefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

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

English

Let $S$ be an additive subsemigroup of $M$. Let $f$ be an additive homomorphism of $M$ and $N$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $S$ and $f$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , S)}{x_{3}})}$.

AddSubsemigroup.gciMapComapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

AddSubsemigroup.giMapComapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

AddSubsemigroup.inclusiondefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the inclusion of h (from the name)

English

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

AddSubsemigroup.mapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the map of f and S (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $N$. Let $S$ be an additive subsemigroup of $M$. Then the map of $f$ and $S$ is an additive subsemigroup of $N$.

AddSubsemigroup.proddefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be an additive subsemigroup of $M$. Let $t$ be an additive subsemigroup of $N$. Then the product of $s$ and $t$ is an additive subsemigroup of $\mathrm{Prod}$ applied to $M$ and $N$.

AddSubsemigroup.prodEquivdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

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

English

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

AddSubsemigroup.toSubsemigroupdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup (from the name)

English

The subsemigroup is an order isomorphism of the set of additive subsemigroups of $A$ and the set of subsemigroups of the set of multiplicatives of $A$.

AddSubsemigroup.toSubsemigroup'defMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup (from the name)

English

The subsemigroup is an order isomorphism of the set of additive subsemigroups of $\mathrm{Additive}$ applied to $M$ and the set of subsemigroups of $M$ defined as the inverse of the additive subsemigroup.

AddSubsemigroup.topEquivdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the top additive subsemigroup (from the docstring)

English

The top additive subsemigroup is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $M$.

MulEquiv.ofLeftInversedefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

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

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the multiplicative equivalence of $f$ and $h$ is a multiplicative equivalence of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{srange} (f)}{x_{2}})}$.

MulEquiv.subsemigroupCongrdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup congruence of h (from the name)

English

Assume that $\EqtMACRoH {S}{T}$. Then the subsemigroup congruence of $h$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$.

MulEquiv.subsemigroupMapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup map of e and S (from the name)

English

Let $e$ be a multiplicative equivalence of $M$ and $N$. Let $S$ be a subsemigroup of $M$. Then the subsemigroup map of $e$ and $S$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toMulHom} (e), S)}{x_{3}})}$.

MulHom.codRestrictdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

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

MulHom.domRestrictdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

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

MulHom.srangedefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Then $\operatorname{srange}$ applied to $f$ is a subsemigroup of $N$.

MulHom.srangeRestrictdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Then $\operatorname{srangeRestrict}$ applied to $f$ is a multiplicative homomorphism of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{srange} (f)}{x_{2}})}$.

MulHom.subsemigroupComapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup preimage of f and #2 (from the name)

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Let $\mathrm{N'}$ be a subsemigroup of $N$. Then the subsemigroup preimage of $f$ and $\mathrm{N'}$ is a multiplicative homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{comap} (f , \mathrm{N'})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{3}})}$.

MulHom.subsemigroupMapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the subsemigroup map of f and #2 (from the name)

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Let $\mathrm{M'}$ be a subsemigroup of $M$. Then the subsemigroup map of $f$ and $\mathrm{M'}$ is a multiplicative homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , \mathrm{M'})}{x_{3}})}$.

Subsemigroup.comapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the preimage of f and S (from the docstring)

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Let $S$ be a subsemigroup of $N$. Then the preimage of $f$ and $S$ is a subsemigroup of $M$.

Subsemigroup.equivMapOfInjectivedefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

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

English

Let $S$ be a subsemigroup of $M$. Let $f$ be a multiplicative homomorphism of $M$ and $N$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $S$ and $f$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , S)}{x_{3}})}$.

Subsemigroup.gciMapComapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Subsemigroup.giMapComapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

no wording

English

Subsemigroup.inclusiondefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the inclusion of h (from the name)

English

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

Subsemigroup.mapdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the map of f and S (from the name)

English

Let $f$ be a multiplicative homomorphism of $M$ and $N$. Let $S$ be a subsemigroup of $M$. Then the map of $f$ and $S$ is a subsemigroup of $N$.

Subsemigroup.proddefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a subsemigroup of $M$. Let $t$ be a subsemigroup of $N$. Then the product of $s$ and $t$ is a subsemigroup of $\mathrm{Prod}$ applied to $M$ and $N$.

Subsemigroup.prodEquivdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

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

English

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

Subsemigroup.toAddSubsemigroupdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the additive subsemigroup (from the name)

English

The additive subsemigroup is an order isomorphism of the set of subsemigroups of $M$ and the set of additive subsemigroups of $\mathrm{Additive}$ applied to $M$.

Subsemigroup.toAddSubsemigroup'defMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the additive subsemigroup (from the name)

English

The additive subsemigroup is an order isomorphism of the set of subsemigroups of the set of multiplicatives of $A$ and the set of additive subsemigroups of $A$ defined as the inverse of the subsemigroup.

Subsemigroup.topEquivdefMathlib.Algebra.Group.Subsemigroup.Operations, function or constant

Wording

the top subsemigroup (from the docstring)

English

The top subsemigroup is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $M$.

Mathlib.Algebra.Group.TransferInstance

Equiv.addEquivdefMathlib.Algebra.Group.TransferInstance, function or constant

Wording

the additive equivalence of e (from the name)

English

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

Equiv.mulEquivdefMathlib.Algebra.Group.TransferInstance, function or constant

Wording

the multiplicative equivalence of e (from the name)

English

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

LibraryNote.instance_transfer_via_equivalencedefMathlib.Algebra.Group.TransferInstance, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_instance\_transfer\_via\_equivalence}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Mathlib.Algebra.Group.Translate

translatedefMathlib.Algebra.Group.Translate, function or constant

Wording

no wording

English

Let $a$ and $x_{2}$ be elements of $G$. Let $f$ be a function from elements of $G$ to elements of $x$. Then $\mathrm{translate}$ applied to $a$, $f$ and $x_{2}$ is an element of $x$ defined as $f$ applied to $x_{2} - a$.

Mathlib.Algebra.Group.TypeTags.Basic

AdditivedefMathlib.Algebra.Group.TypeTags.Basic, type

Wording

no wording

English

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

Additive.ofMuldefMathlib.Algebra.Group.TypeTags.Basic, function or constant

Wording

no wording

English

$\operatorname{ofMul}$ is an element of $\EquivMACRoAE {x}{\mathrm{Additive} (x)}$.

Additive.toMuldefMathlib.Algebra.Group.TypeTags.Basic, function or constant

Wording

the product (from the name)

English

The product is an element of $\EquivMACRoAE {\mathrm{Additive} (x)}{x}$ defined as the inverse of $\operatorname{ofMul}$.

MultiplicativedefMathlib.Algebra.Group.TypeTags.Basic, type

Wording

multiplicative of x (from the name)

English

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

Multiplicative.ofAdddefMathlib.Algebra.Group.TypeTags.Basic, function or constant

Wording

the multiplicative (from the name)

English

The multiplicative is an equivalence from $x$ to the set of multiplicatives of $x$.

Multiplicative.toAdddefMathlib.Algebra.Group.TypeTags.Basic, function or constant

Wording

the sum (from the name)

English

The sum is an equivalence from the set of multiplicatives of $x$ to $x$ defined as the inverse of the multiplicative.

Mathlib.Algebra.Group.TypeTags.Hom

AddMonoidHom.toMultiplicativedefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the multiplicative (from the name)

English

The multiplicative is an equivalence from the set of additive monoid homomorphisms of $x$ and $x_{1}$ to the set of monoid homomorphisms of the set of multiplicatives of $x$ and the set of multiplicatives of $x_{1}$.

AddMonoidHom.toMultiplicativeLeftdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the left multiplicative (from the name)

English

The left multiplicative is an equivalence from the set of additive monoid homomorphisms of $x$ and $\mathrm{Additive}$ applied to $x_{1}$ to the set of monoid homomorphisms of the set of multiplicatives of $x$ and $x_{1}$.

AddMonoidHom.toMultiplicativeLeftAddEquivdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the multiplicative left additive equivalence (from the name)

English

The multiplicative left additive equivalence is an additive equivalence of the set of additive monoid homomorphisms of $M$ and $\mathrm{Additive}$ applied to $N$ and $\mathrm{Additive}$ applied to the set of monoid homomorphisms of the set of multiplicatives of $M$ and $N$.

AddMonoidHom.toMultiplicativeRightdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the right multiplicative (from the name)

English

The right multiplicative is an equivalence from the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $x$ and $x_{1}$ to the set of monoid homomorphisms of $x$ and the set of multiplicatives of $x_{1}$.

AddMonoidHom.toMultiplicativeRightAddEquivdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the multiplicative right additive equivalence (from the name)

English

The multiplicative right additive equivalence is an additive equivalence of the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $M$ and $N$ and $\mathrm{Additive}$ applied to the set of monoid homomorphisms of $M$ and the set of multiplicatives of $N$.

MonoidHom.toAdditivedefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

no wording

English

$\operatorname{toAdditive}$ is an equivalence from the set of monoid homomorphisms of $x$ and $x_{1}$ to the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $x$ and $\mathrm{Additive}$ applied to $x_{1}$.

MonoidHom.toAdditiveLeftdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

no wording

English

$\operatorname{toAdditiveLeft}$ is an equivalence from the set of monoid homomorphisms of $x$ and the set of multiplicatives of $x_{1}$ to the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $x$ and $x_{1}$ defined as the inverse of the right multiplicative.

MonoidHom.toAdditiveLeftMulEquivdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the additive left multiplicative equivalence (from the name)

English

The additive left multiplicative equivalence is a multiplicative equivalence of the set of monoid homomorphisms of $M$ and the set of multiplicatives of $N$ and the set of multiplicatives of the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $M$ and $N$.

MonoidHom.toAdditiveRightdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

no wording

English

$\operatorname{toAdditiveRight}$ is an equivalence from the set of monoid homomorphisms of the set of multiplicatives of $x$ and $x_{1}$ to the set of additive monoid homomorphisms of $x$ and $\mathrm{Additive}$ applied to $x_{1}$ defined as the inverse of the left multiplicative.

MonoidHom.toAdditiveRightMulEquivdefMathlib.Algebra.Group.TypeTags.Hom, function or constant

Wording

the additive right multiplicative equivalence (from the name)

English

The additive right multiplicative equivalence is a multiplicative equivalence of the set of monoid homomorphisms of the set of multiplicatives of $M$ and $N$ and the set of multiplicatives of the set of additive monoid homomorphisms of $M$ and $\mathrm{Additive}$ applied to $N$.

Mathlib.Algebra.Group.ULift

AddEquiv.uliftdefMathlib.Algebra.Group.ULift, function or constant

Wording

the lift (from the name)

English

The lift is an additive equivalence of $\mathrm{ULift}$ applied to $x$ and $x$.

MulEquiv.uliftdefMathlib.Algebra.Group.ULift, function or constant

Wording

the lift (from the name)

English

The lift is a multiplicative equivalence of $\mathrm{ULift}$ applied to $x$ and $x$.

Mathlib.Algebra.Group.UniqueProds.Basic

TwoUniqueProdsclassMathlib.Algebra.Group.UniqueProds.Basic, predicate

Wording

no wording

English

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

TwoUniqueSumsclassMathlib.Algebra.Group.UniqueProds.Basic, predicate

Wording

no wording

English

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

UniqueAdddefMathlib.Algebra.Group.UniqueProds.Basic, predicate

Wording

no wording

English

Let $A$ and $B$ be finite sets of $G$. Let $a_{0}$ and $b_{0}$ be elements of $G$. Then $\mathrm{UniqueAdd}$ holds for $A$, $B$, $a_{0}$ and $b_{0}$, if for all elements $a$ and $b$ of $G$, if $a$ is an element of $A$, then if $b$ is an element of $B$, then if $\EqtMACRoH {a + b}{a_{0} + b_{0}}$, then $\EqtMACRoH {a}{a_{0}}$ and $\EqtMACRoH {b}{b_{0}}$.

UniqueMuldefMathlib.Algebra.Group.UniqueProds.Basic, predicate

Wording

no wording

English

Let $A$ and $B$ be finite sets of $G$. Let $a_{0}$ and $b_{0}$ be elements of $G$. Then $\mathrm{UniqueMul}$ holds for $A$, $B$, $a_{0}$ and $b_{0}$, if for all elements $a$ and $b$ of $G$, if $a$ is an element of $A$, then if $b$ is an element of $B$, then if $\EqtMACRoH {a \times b}{a_{0} \times b_{0}}$, then $\EqtMACRoH {a}{a_{0}}$ and $\EqtMACRoH {b}{b_{0}}$.

UniqueProdsclassMathlib.Algebra.Group.UniqueProds.Basic, predicate

Wording

no wording

English

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

UniqueSumsclassMathlib.Algebra.Group.UniqueProds.Basic, predicate

Wording

no wording

English

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

Mathlib.Algebra.Group.Units.Defs

AddUnitsstructureMathlib.Algebra.Group.Units.Defs, type

Wording

additive unit of x (from the name)

English

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

AddUnits.copydefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the copy of val and neg (from the name)

English

Let $u$ be an additive unit of $x$. Let $\mathrm{val}$ and $\mathrm{neg}$ be elements of $x$ such that $\mathrm{val}$ is equal to the underlying value in the base of $u$ and $\mathrm{neg}$ is equal to the underlying value in the base of $\operatorname{neg}$ applied to $u$. Then the copy of $\mathrm{val}$ and $\mathrm{neg}$ is an additive unit of $x$.

AddUnits.mkOfAddEqZerodefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$ such that $\EqtMACRoH {a + b}{0}$. Then $\operatorname{mkOfAddEqZero}$ applied to $a$, $b$ and $\mathrm{hab}$ is an additive unit of $x$.

AddUnits.negdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the negation of self (from the name)

English

Let $\mathrm{self}$ be an additive unit of $x$. Then the negation of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

AddUnits.valdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the underlying value in the base of self (from the docstring)

English

Let $\mathrm{self}$ be an additive unit of $x$. Then the underlying value in the base of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

IsAddUnitdefMathlib.Algebra.Group.Units.Defs, predicate

Wording

a is a additive unit (from the name)

English

Let $a$ be an element of $M$. Then $a$ is an additive unit, if there exists an additive unit $u$ of $M$, such that the underlying value in the base of $u$ is equal to $a$.

IsAddUnit.addUnitdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the additive unit of h (from the name)

English

Assume that $a$ is an additive unit. Then the additive unit of $h$ is an additive unit of $M$.

IsAddUnit.addUnit'defMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the additive unit of h (from the name)

English

Assume that $a$ is an additive unit. Then the additive unit of $h$ is an additive unit of $x$ defined as $\operatorname{mk}$ applied to $a$, $\operatorname{neg}$ applied to $a$, $\mathrm{IsAddUnit\_\_add\_neg\_cancel}$ applied to $h$ and $\mathrm{IsAddUnit\_\_neg\_add\_cancel}$ applied to $h$.

IsUnitdefMathlib.Algebra.Group.Units.Defs, predicate

Wording

a is a unit (by hand)

English

Let $a$ be an element of $M$. Then $a$ is a unit, if there exists a unit $u$ of $M$, such that the underlying value in the base of $u$ is equal to $a$.

IsUnit.unitdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the unit of h (from the name)

English

Assume that $a$ is a unit. Then the unit of $h$ is a unit of $M$.

IsUnit.unit'defMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the unit of h (from the name)

English

Assume that $a$ is a unit. Then the unit of $h$ is a unit of $x$ defined as $\operatorname{mk}$ applied to $a$, $\operatorname{inv}$ applied to $a$, $\mathrm{IsUnit\_\_mul\_inv\_cancel}$ applied to $h$ and $\mathrm{IsUnit\_\_inv\_mul\_cancel}$ applied to $h$.

UnitsstructureMathlib.Algebra.Group.Units.Defs, type

Wording

unit of x (by hand)

English

Let $x$ be a set. Then $\UnitsMACRoAO {x}$ is a set.

Units.copydefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the copy of val and inv (from the name)

English

Let $u$ be a unit of $x$. Let $\mathrm{val}$ and $\mathrm{inv}$ be elements of $x$ such that $\mathrm{val}$ is equal to the underlying value in the base of $u$ and $\mathrm{inv}$ is equal to the underlying value in the base of $\operatorname{inv}$ applied to $u$. Then the copy of $\mathrm{val}$ and $\mathrm{inv}$ is a unit of $x$.

Units.invdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the inverse of self (from the name)

English

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

Units.mkOfMulEqOnedefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$ such that $\EqtMACRoH {a \times b}{1}$. Then $\operatorname{mkOfMulEqOne}$ applied to $a$, $b$ and $\mathrm{hab}$ is a unit of $x$.

Units.valdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

the underlying value in the base of self (from the docstring)

English

Let $\mathrm{self}$ be a unit of $x$. Then the underlying value in the base of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

divpdefMathlib.Algebra.Group.Units.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $u$ be a unit of $x$. Then $\mathrm{divp}$ applied to $a$ and $u$ is an element of $x$ defined as the product of $a$ and the underlying value in the base of $\operatorname{inv}$ applied to $u$.

Mathlib.Algebra.Group.Units.Equiv

AddEquiv.negdefMathlib.Algebra.Group.Units.Equiv, 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 $G$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{neg}$, $\operatorname{neg}$, $\mathrm{Equiv\_\_left\_inv}$ applied to the negation of $G$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the negation of $G$ and $\mathrm{neg\_add}$.

AddUnits.addLeftdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

no wording

English

Let $u$ be an additive unit of $M$. Then $\operatorname{addLeft}$ applied to $u$ is a permutation of $M$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to the sum of the underlying value in the base of $u$ and $x_{1}$, the function that maps $x_{2}$ to the sum of the underlying value in the base of $\operatorname{neg}$ applied to $u$ and $x_{2}$, $\mathrm{AddUnits\_\_neg\_add\_cancel\_left}$ applied to $u$ and $\mathrm{AddUnits\_\_add\_neg\_cancel\_left}$ applied to $u$.

AddUnits.addRightdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

no wording

English

Let $u$ be an additive unit of $M$. Then $\operatorname{addRight}$ applied to $u$ is a permutation of $M$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to the sum of $x_{1}$ and the underlying value in the base of $u$, the function that maps $x_{2}$ to the sum of $x_{2}$ and the underlying value in the base of $\operatorname{neg}$ applied to $u$, the function that maps $x_{3}$ to $\mathrm{AddUnits\_\_add\_neg\_cancel\_right}$ applied to $x_{3}$ and $u$ and the function that maps $x_{4}$ to $\mathrm{AddUnits\_\_neg\_add\_cancel\_right}$ applied to $x_{4}$ and $u$.

Equiv.addLeftdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

no wording

English

Let $a$ be an element of $G$. Then $\operatorname{addLeft}$ applied to $a$ is a permutation of $G$ defined as $\operatorname{addLeft}$ applied to $\operatorname{toAddUnits}$ applied to $a$.

Equiv.addRightdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

no wording

English

Let $a$ be an element of $G$. Then $\operatorname{addRight}$ applied to $a$ is a permutation of $G$ defined as $\operatorname{addRight}$ applied to $\operatorname{toAddUnits}$ applied to $a$.

Equiv.divLeftdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the left quotient of a (from the name)

English

Let $a$ be an element of $G$. Then the left quotient of $a$ is an equivalence from $G$ to $G$.

Equiv.divRightdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the right quotient of a (from the name)

English

Let $a$ be an element of $G$. Then the right quotient of $a$ is an equivalence from $G$ to $G$.

Equiv.mulLeftdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the left multiplicative of a (from the name)

English

Let $a$ be an element of $G$. Then the left multiplicative of $a$ is a permutation of $G$ defined as the left multiplicative of $\operatorname{toUnits}$ applied to $a$.

Equiv.mulRightdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the right multiplicative of a (from the name)

English

Let $a$ be an element of $G$. Then the right multiplicative of $a$ is a permutation of $G$ defined as the right multiplicative of $\operatorname{toUnits}$ applied to $a$.

Equiv.subLeftdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the left difference of a (from the name)

English

Let $a$ be an element of $G$. Then the left difference of $a$ is an equivalence from $G$ to $G$.

Equiv.subRightdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the right difference of a (from the name)

English

Let $a$ be an element of $G$. Then the right difference of $a$ is an equivalence from $G$ to $G$.

MulEquiv.invdefMathlib.Algebra.Group.Units.Equiv, 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 $G$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inv}$, $\operatorname{inv}$, $\mathrm{Equiv\_\_left\_inv}$ applied to the inverse of $G$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the inverse of $G$ and $\mathrm{mul\_inv}$.

Units.mapEquivdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the map equivalence of h (from the name)

English

Let $h$ be a multiplicative equivalence of $M$ and $N$. Then the map equivalence of $h$ is a multiplicative equivalence of $\UnitsMACRoAO {M}$ and $\UnitsMACRoAO {N}$.

Units.mulLeftdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the left multiplicative of u (from the name)

English

Let $u$ be a unit of $M$. Then the left multiplicative of $u$ is a permutation of $M$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to the product of the underlying value in the base of $u$ and $x_{1}$, the function that maps $x_{2}$ to the product of the underlying value in the base of $\operatorname{inv}$ applied to $u$ and $x_{2}$, $\mathrm{Units\_\_inv\_mul\_cancel\_left}$ applied to $u$ and $\mathrm{Units\_\_mul\_inv\_cancel\_left}$ applied to $u$.

Units.mulRightdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the right multiplicative of u (from the name)

English

Let $u$ be a unit of $M$. Then the right multiplicative of $u$ is a permutation of $M$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to the product of $x_{1}$ and the underlying value in the base of $u$, the function that maps $x_{2}$ to the product of $x_{2}$ and the underlying value in the base of $\operatorname{inv}$ applied to $u$, the function that maps $x_{3}$ to $\mathrm{Units\_\_mul\_inv\_cancel\_right}$ applied to $x_{3}$ and $u$ and the function that maps $x_{4}$ to $\mathrm{Units\_\_inv\_mul\_cancel\_right}$ applied to $x_{4}$ and $u$.

toAddUnitsdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the additive unit (from the name)

English

The additive unit is an additive equivalence of $G$ and the set of additive units of $G$.

toUnitsdefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the unit (from the name)

English

The unit is a multiplicative equivalence of $G$ and $\UnitsMACRoAO {G}$.

unitsEquivProdSubtypedefMathlib.Algebra.Group.Units.Equiv, function or constant

Wording

the unit equivalence product subtype of x (from the name)

English

Let $x$ be a set. Then the unit equivalence product subtype of $x$ is an equivalence from $\UnitsMACRoAO {x}$ to $\SubtypeSet {p}{\mathrm{and} (\EqtMACRoH {(\ProdfstMACRoZ {p}\times \ProdsndMACRoAA {p})}{1}, \EqtMACRoH {(\ProdsndMACRoAA {p}\times \ProdfstMACRoZ {p})}{1})}$.

Mathlib.Algebra.Group.Units.Hom

AddMonoidHom.toHomAddUnitsdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the homomorphism additive unit of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $G$ and $M$. Then the homomorphism additive unit of $f$ is an additive monoid homomorphism of $G$ and the set of additive units of $M$.

AddUnits.coeHomdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the coercion homomorphism of M (from the name)

English

Let $M$ be a set. Then the coercion homomorphism of $M$ is an additive monoid homomorphism of the set of additive units of $M$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{val}$ and $\mathrm{AddUnits\_\_val\_zero}$ and $\mathrm{AddUnits\_\_val\_add}$.

AddUnits.liftRightdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the right lift of f and g (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Let $g$ be a function from elements of $M$ to additive units of $N$ such that for all elements $x_{2}$ of $M$, the underlying value in the base of $g$ applied to $x_{2}$ is equal to $f$ applied to $x_{2}$. Then the right lift of $f$ and $g$ is an additive monoid homomorphism of $M$ and the set of additive units of $N$.

AddUnits.mapdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the map of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then the map of $f$ is an additive monoid homomorphism of the set of additive units of $M$ and the set of additive units of $N$.

IsAddUnit.liftRightdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the right lift 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}$ of $M$, $f$ applied to $x_{2}$ is an additive unit. Then the right lift of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of $M$ and the set of additive units of $N$.

IsLocalHomclassMathlib.Algebra.Group.Units.Hom, predicate

Wording

f is a local homomorphism (from the name)

English

Let $f$ be an element of $F$. Then we can say that $f$ is a local homomorphism.

IsUnit.liftRightdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the right lift 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}$ of $M$, $f$ applied to $x_{2}$ is a unit. Then the right lift of $f$ and $\mathrm{hf}$ is a monoid homomorphism of $M$ and $\UnitsMACRoAO {N}$.

MonoidHom.toHomUnitsdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the homomorphism unit of f (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $M$. Then the homomorphism unit of $f$ is a monoid homomorphism of $G$ and $\UnitsMACRoAO {M}$.

MonoidHom.toHomUnitsMulEquivdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the homomorphism unit multiplicative equivalence (from the name)

English

The homomorphism unit multiplicative equivalence is a multiplicative equivalence of the set of monoid homomorphisms of $G$ and $M$ and the set of monoid homomorphisms of $G$ and $\UnitsMACRoAO {M}$.

Units.coeHomdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the coercion homomorphism of M (from the name)

English

Let $M$ be a set. Then the coercion homomorphism of $M$ is a monoid homomorphism of $\UnitsMACRoAO {M}$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{val}$ and $\mathrm{Units\_\_val\_one}$ and $\mathrm{Units\_\_val\_mul}$.

Units.liftRightdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the right lift of f and g (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Let $g$ be a function from elements of $M$ to units of $N$ such that for all elements $x_{2}$ of $M$, the underlying value in the base of $g$ applied to $x_{2}$ is equal to $f$ applied to $x_{2}$. Then the right lift of $f$ and $g$ is a monoid homomorphism of $M$ and $\UnitsMACRoAO {N}$.

Units.mapdefMathlib.Algebra.Group.Units.Hom, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$. Then the map of $f$ is a monoid homomorphism of $\UnitsMACRoAO {M}$ and $\UnitsMACRoAO {N}$.

Mathlib.Algebra.Group.Units.Opposite

AddUnits.opEquivdefMathlib.Algebra.Group.Units.Opposite, function or constant

Wording

the opposite equivalence (from the name)

English

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

Units.opEquivdefMathlib.Algebra.Group.Units.Opposite, function or constant

Wording

the opposite equivalence (from the name)

English

The opposite equivalence is a multiplicative equivalence of the set of units of the set of multiplicative opposites of $M$ and the set of multiplicative opposites of $\UnitsMACRoAO {M}$.

Mathlib.Algebra.Group.WithOne.Basic

AddEquiv.withZeroCongrdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

no wording

English

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

MulEquiv.withOneCongrdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

no wording

English

Let $e$ be a multiplicative equivalence of $x$ and $x_{1}$. Then $\operatorname{withOneCongr}$ applied to $e$ is a multiplicative equivalence of $\mathrm{WithOne}$ applied to $x$ and $\mathrm{WithOne}$ applied to $x_{1}$.

WithOne.coeMulHomdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

the coercion multiplicative homomorphism (from the name)

English

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

WithOne.liftdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from the set of multiplicative homomorphisms of $x$ and $x_{1}$ to the set of monoid homomorphisms of $\mathrm{WithOne}$ applied to $x$ and $x_{1}$.

WithOne.mapMulHomdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

the map multiplicative homomorphism of f (from the name)

English

Let $f$ be a multiplicative homomorphism of $x$ and $x_{1}$. Then the map multiplicative homomorphism of $f$ is a monoid homomorphism of $\mathrm{WithOne}$ applied to $x$ and $\mathrm{WithOne}$ applied to $x_{1}$ defined as $\operatorname{lift}$ applied to the composition of the coercion multiplicative homomorphism and $f$.

WithZero.coeAddHomdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

the coercion additive homomorphism (from the name)

English

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

WithZero.liftdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from the set of additive homomorphisms of $x$ and $x_{1}$ to the set of additive monoid homomorphisms of $\mathrm{WithZero}$ applied to $x$ and $x_{1}$.

WithZero.mapAddHomdefMathlib.Algebra.Group.WithOne.Basic, function or constant

Wording

the map additive homomorphism of f (from the name)

English

Let $f$ be an additive homomorphism of $x$ and $x_{1}$. Then the map additive homomorphism of $f$ is an additive monoid homomorphism of $\mathrm{WithZero}$ applied to $x$ and $\mathrm{WithZero}$ applied to $x_{1}$ defined as $\operatorname{lift}$ applied to the composition of the coercion additive homomorphism and $f$.

Mathlib.Algebra.Group.WithOne.Defs

WithOnedefMathlib.Algebra.Group.WithOne.Defs, type

Wording

no wording

English

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

WithOne.coedefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

the coercion of x1 (from the name)

English

Let $x_{1}$ be an element of $x$. Then the coercion of $x_{1}$ is an element of $\mathrm{WithOne}$ applied to $x$ defined as $\operatorname{some}$ applied to $x_{1}$.

WithOne.recOneCoedefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

no wording

English

Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{coe}$ be a function from elements $a$ of $x$ to elements of $\mathrm{motive}$ applied to the coercion of $a$. Let $n$ be an element of $\mathrm{WithOne}$ applied to $x$. Then $\operatorname{recOneCoe}$ applied to $\mathrm{one}$, $a$, $\mathrm{coe}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$.

WithOne.unonedefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

no wording

English

Assume that $x_{1} \neq 1$. Then $\operatorname{unone}$ applied to $h$ is an element of $x$.

WithOne.unoneDdefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

no wording

English

Let $d$ be an element of $x$. Let $x_{1}$ be an element of $\mathrm{WithOne}$ applied to $x$. Then $\operatorname{unoneD}$ applied to $d$ and $x_{1}$ is an element of $x$ defined as $\operatorname{recOneCoe}$ applied to $d$, $\mathrm{id}$ and $x_{1}$.

WithZerodefMathlib.Algebra.Group.WithOne.Defs, type

Wording

no wording

English

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

WithZero.coedefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

the coercion of x1 (from the name)

English

Let $x_{1}$ be an element of $x$. Then the coercion of $x_{1}$ is an element of $\mathrm{WithZero}$ applied to $x$ defined as $\operatorname{some}$ applied to $x_{1}$.

WithZero.recZeroCoedefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{coe}$ be a function from elements $a$ of $x$ to elements of $\mathrm{motive}$ applied to the coercion of $a$. Let $n$ be an element of $\mathrm{WithZero}$ applied to $x$. Then $\operatorname{recZeroCoe}$ applied to $\mathrm{zero}$, $a$, $\mathrm{coe}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$.

WithZero.unzerodefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

no wording

English

Assume that $x_{1} \neq 0$. Then $\operatorname{unzero}$ applied to $h$ is an element of $x$.

WithZero.unzeroDdefMathlib.Algebra.Group.WithOne.Defs, function or constant

Wording

no wording

English

Let $d$ be an element of $x$. Let $x_{1}$ be an element of $\mathrm{WithZero}$ applied to $x$. Then $\operatorname{unzeroD}$ applied to $d$ and $x_{1}$ is an element of $x$ defined as $\operatorname{recZeroCoe}$ applied to $d$, $\mathrm{id}$ and $x_{1}$.

Mathlib.Algebra.Group.WithOne.Map

WithOne.mapdefMathlib.Algebra.Group.WithOne.Map, function or constant

Wording

the map of f and x2 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{WithOne}$ applied to $x$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{WithOne}$ applied to $x_{1}$ defined as $\operatorname{map}$ applied to $f$ and $x_{2}$.

WithOne.map₂defMathlib.Algebra.Group.WithOne.Map, function or constant

Wording

the map of x4 and x5 (from the name)

English

Let $x_{3}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\mathrm{WithOne}$ applied to $x$. Let $x_{5}$ be an element of $\mathrm{WithOne}$ applied to $x_{1}$. Then the map of $x_{4}$ and $x_{5}$ is an element of $\mathrm{WithOne}$ applied to $x_{2}$ defined as the map of $x_{4}$ and $x_{5}$.

WithZero.mapdefMathlib.Algebra.Group.WithOne.Map, function or constant

Wording

the map of f and x2 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{WithZero}$ applied to $x$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{WithZero}$ applied to $x_{1}$ defined as $\operatorname{map}$ applied to $f$ and $x_{2}$.

WithZero.map₂defMathlib.Algebra.Group.WithOne.Map, function or constant

Wording

the map of x4 and x5 (from the name)

English

Let $x_{3}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\mathrm{WithZero}$ applied to $x$. Let $x_{5}$ be an element of $\mathrm{WithZero}$ applied to $x_{1}$. Then the map of $x_{4}$ and $x_{5}$ is an element of $\mathrm{WithZero}$ applied to $x_{2}$ defined as the map of $x_{4}$ and $x_{5}$.

Mathlib.Algebra.GroupWithZero.Action.Basic

DistribMulAction.toAddAutdefMathlib.Algebra.GroupWithZero.Action.Basic, function or constant

Wording

the additive automorphism of G and A (from the name)

English

Let $G$ and $A$ be sets. Then the additive automorphism of $G$ and $A$ is a monoid homomorphism of $G$ and the set of multiplicatives of the set of additive automorphisms of $A$.

DistribMulAction.toAddEquivdefMathlib.Algebra.GroupWithZero.Action.Basic, function or constant

Wording

the additive equivalence of A and x3 (from the name)

English

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

smulMonoidWithZeroHomdefMathlib.Algebra.GroupWithZero.Action.Basic, function or constant

Wording

the scalar multiple monoid with zero homomorphism (from the name)

English

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

Mathlib.Algebra.GroupWithZero.Action.Center

Subgroup.centerUnitsEquivUnitsCenterdefMathlib.Algebra.GroupWithZero.Action.Center, function or constant

Wording

the center unit equivalence unit center of x (from the name)

English

Let $x$ be a set. Then the center unit equivalence unit center of $x$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\UnitsMACRoAO {x})}{x_{2}})}$ and $\UnitsMACRoAO {(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (x)}{x_{3}})})}$.

Mathlib.Algebra.GroupWithZero.Action.Defs

DistribMulActionclassMathlib.Algebra.GroupWithZero.Action.Defs, predicate

Wording

no wording

English

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

DistribMulAction.toAddMonoidEnddefMathlib.Algebra.GroupWithZero.Action.Defs, function or constant

Wording

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

English

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

DistribSMulclassMathlib.Algebra.GroupWithZero.Action.Defs, predicate

Wording

no wording

English

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

DistribSMul.toAddMonoidHomdefMathlib.Algebra.GroupWithZero.Action.Defs, function or constant

Wording

the additive monoid homomorphism of A and x2 (from the name)

English

Let $A$ be a set. Let $x_{2}$ be an element of $M$. Then the additive monoid homomorphism of $A$ and $x_{2}$ is an additive monoid homomorphism of $A$ and $A$.

MulActionWithZeroclassMathlib.Algebra.GroupWithZero.Action.Defs, predicate

Wording

no wording

English

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

SMulWithZeroclassMathlib.Algebra.GroupWithZero.Action.Defs, predicate

Wording

no wording

English

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

SMulZeroClassclassMathlib.Algebra.GroupWithZero.Action.Defs, predicate

Wording

no wording

English

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

SMulZeroClass.toZeroHomdefMathlib.Algebra.GroupWithZero.Action.Defs, function or constant

Wording

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

English

Let $A$ be a set. Let $x_{2}$ be an element of $M$. Then the zero homomorphism of $A$ and $x_{2}$ is a zero homomorphism of $A$ and $A$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $\HSMulhSMulMACRoAL {x_{2}}{x_{3}}$ and $\mathrm{SMulZeroClass\_\_smul\_zero}$ applied to $x_{2}$.

Mathlib.Algebra.GroupWithZero.Action.End

DistribMulAction.toAddEquiv₀defMathlib.Algebra.GroupWithZero.Action.End, function or constant

Wording

the additive equivalence of x5 (from the name)

English

Let $x_{1}$ be a set. Let $x_{5}$ be an element of $x$ such that $x_{5} \neq 0$. Then the additive equivalence of $x_{5}$ is an additive equivalence of $x_{1}$ and $x_{1}$.

Mathlib.Algebra.GroupWithZero.Action.Prod

DistribMulAction.prodEquivdefMathlib.Algebra.GroupWithZero.Action.Prod, function or constant

Wording

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

English

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

Mathlib.Algebra.GroupWithZero.Action.Units

Equiv.smulRightdefMathlib.Algebra.GroupWithZero.Action.Units, function or constant

Wording

the right scalar multiple of ha (from the name)

English

Assume that $a \neq 0$. Then the right scalar multiple of $\mathrm{ha}$ is an equivalence from $x_{1}$ to $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $b$ to $\HSMulhSMulMACRoAL {a}{b}$, the function that maps $b_{1}$ to $\HSMulhSMulMACRoAL {\operatorname{inv} (a)}{b_{1}}$, $\mathrm{inv\_smul\_smul\_u2080\_}$ applied to $\mathrm{ha}$ and $\mathrm{smul\_inv\_smul\_u2080\_}$ applied to $\mathrm{ha}$.