Definitions: Mathlib.GroupTheory, part 3 of 3

AddLocalization.mkOrderEmbeddingdefMathlib.GroupTheory.MonoidLocalization.Order, function or constant

Wording

the order embedding of b (from the name)

English

Let $b$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$. Then the order embedding of $b$ is an order embedding of $x$ and the set of additive localizations of $s$.

Localization.mkOrderEmbeddingdefMathlib.GroupTheory.MonoidLocalization.Order, function or constant

Wording

the order embedding of b (from the name)

English

Let $b$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$. Then the order embedding of $b$ is an order embedding of $x$ and the set of localizations of $s$.

Mathlib.GroupTheory.Nilpotent

AddGroup.IsNilpotentclassMathlib.GroupTheory.Nilpotent, predicate

Wording

G is nilpotent (from the name)

English

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

AddGroup.IsVirtuallyNilpotentdefMathlib.GroupTheory.Nilpotent, predicate

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{IsVirtuallyNilpotent}$ holds for $G$, if there exists an additive subgroup $N$ of $G$, such that $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {N}{x_{1}})}$ is nilpotent and $N$ is a finite index.

AddGroup.nilpotencyClassdefMathlib.GroupTheory.Nilpotent, function or constant

Wording

the nilpotency class of G (from the docstring)

English

Let $G$ be a set. Then the nilpotency class of $G$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that $G$ is nilpotent, the function that maps $\mathrm{hG}$ to $\operatorname{find}$ applied to $\operatorname{nilpotent}$ applied to $G$ and the function that maps $\mathrm{hG1}$ to $0$.

AddSubgroup.IsAscendingCentralSeriesdefMathlib.GroupTheory.Nilpotent, predicate

Wording

no wording

English

Let $H$ be a function from natural numbers to additive subgroups of $G$. Then $\operatorname{IsAscendingCentralSeries}$ holds for $H$, if $H$ applied to $0$ is equal to the bottom and for all elements $x_{1}$ of $G$, for all natural numbers $n$, if $\MembershipmemMACRoT {H (n + 1)}{x_{1}}$, then for all elements $g$ of $G$, the bracket of $x_{1}$ and $g$ is an element of $H$ applied to $n$.

AddSubgroup.upperCentralSeriesdefMathlib.GroupTheory.Nilpotent, function or constant

Wording

the upper central series of G and n (from the name)

English

Let $G$ be a set. Let $n$ be a natural number. Then the upper central series of $G$ and $n$ is an additive subgroup of $G$ defined as $\operatorname{fst}$ applied to $\operatorname{upperCentralSeriesAux}$ applied to $G$ and $n$.

AddSubgroup.upperCentralSeriesStepdefMathlib.GroupTheory.Nilpotent, function or constant

Wording

the upper central series step of N (from the name)

English

Let $N$ be an additive subgroup of $G$. Then the upper central series step of $N$ is an additive subgroup of $G$.

Group.IsNilpotentclassMathlib.GroupTheory.Nilpotent, predicate

Wording

G is nilpotent (from the name)

English

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

Group.IsVirtuallyNilpotentdefMathlib.GroupTheory.Nilpotent, predicate

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{IsVirtuallyNilpotent}$ holds for $G$, if there exists a subgroup $N$ of $G$, such that $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {N}{x_{1}})}$ is nilpotent and $N$ is a finite index.

Group.nilpotencyClassdefMathlib.GroupTheory.Nilpotent, function or constant

Wording

the nilpotency class of G (from the docstring)

English

Subgroup.IsAscendingCentralSeriesdefMathlib.GroupTheory.Nilpotent, predicate

Wording

no wording

English

Let $H$ be a function from natural numbers to subgroups of $G$. Then $\operatorname{IsAscendingCentralSeries}$ holds for $H$, if $H$ applied to $0$ is equal to the bottom and for all elements $x_{1}$ of $G$, for all natural numbers $n$, if $\MembershipmemMACRoT {H (n + 1)}{x_{1}}$, then for all elements $g$ of $G$, the bracket of $x_{1}$ and $g$ is an element of $H$ applied to $n$.

Subgroup.upperCentralSeriesdefMathlib.GroupTheory.Nilpotent, function or constant

Wording

the upper central series of G and n (from the name)

English

Let $G$ be a set. Let $n$ be a natural number. Then the upper central series of $G$ and $n$ is a subgroup of $G$ defined as $\operatorname{fst}$ applied to $\operatorname{upperCentralSeriesAux}$ applied to $G$ and $n$.

Subgroup.upperCentralSeriesStepdefMathlib.GroupTheory.Nilpotent, function or constant

Wording

the upper central series step of N (from the name)

English

Let $N$ be a subgroup of $G$. Then the upper central series step of $N$ is a subgroup of $G$.

Mathlib.GroupTheory.Nilpotent.LowerCentralSeries

AddSubgroup.IsDescendingCentralSeriesdefMathlib.GroupTheory.Nilpotent.LowerCentralSeries, predicate

Wording

H is a descending central series (from the name)

English

Let $H$ be a function from natural numbers to additive subgroups of $G$. Then $H$ is a descending central series, if $H$ applied to $0$ is equal to the top and for all elements $x_{1}$ of $G$, for all natural numbers $n$, if $\MembershipmemMACRoT {H (n)}{x_{1}}$, then for all elements $g$ of $G$, the bracket of $x_{1}$ and $g$ is an element of $H$ applied to $n + 1$.

AddSubgroup.lowerCentralSeriesdefMathlib.GroupTheory.Nilpotent.LowerCentralSeries, function or constant

Wording

the lower central series of H and x1 (from the docstring)

English

Let $H$ be an additive subgroup of $G$. Let $x_{1}$ be a natural number. Then the lower central series of $H$ and $x_{1}$ is an additive subgroup of $G$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{AddSubgroup\_\_lowerCentralSeries\_\_\_f}$ applied to $H$.

Subgroup.IsDescendingCentralSeriesdefMathlib.GroupTheory.Nilpotent.LowerCentralSeries, predicate

Wording

H is a descending central series (from the name)

English

Let $H$ be a function from natural numbers to subgroups of $G$. Then $H$ is a descending central series, if $H$ applied to $0$ is equal to the top and for all elements $x_{1}$ of $G$, for all natural numbers $n$, if $\MembershipmemMACRoT {H (n)}{x_{1}}$, then for all elements $g$ of $G$, the bracket of $x_{1}$ and $g$ is an element of $H$ applied to $n + 1$.

Subgroup.lowerCentralSeriesdefMathlib.GroupTheory.Nilpotent.LowerCentralSeries, function or constant

Wording

the lower central series of H and x1 (from the docstring)

English

Let $H$ be a subgroup of $G$. Let $x_{1}$ be a natural number. Then the lower central series of $H$ and $x_{1}$ is a subgroup of $G$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Subgroup\_\_lowerCentralSeries\_\_\_f}$ applied to $H$.

Mathlib.GroupTheory.NoncommCoprod

AddHom.noncommCoproddefMathlib.GroupTheory.NoncommCoprod, function or constant

Wording

the noncommutative coproduct of f and g (from the name)

English

Let $f$ be an additive homomorphism of $M$ and $P$. Let $g$ be an additive homomorphism of $N$ and $P$ such that for all elements $m$ of $M$, for all elements $n$ of $N$, $\mathrm{AddCommute}$ holds for $f$ applied to $m$ and $g$ applied to $n$. Then the noncommutative coproduct of $f$ and $g$ is an additive homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$.

AddMonoidHom.noncommCoproddefMathlib.GroupTheory.NoncommCoprod, function or constant

Wording

the noncommutative coproduct of f and g (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $P$. Let $g$ be an additive monoid homomorphism of $N$ and $P$ such that for all elements $m$ of $M$, for all elements $n$ of $N$, $\mathrm{AddCommute}$ holds for $f$ applied to $m$ and $g$ applied to $n$. Then the noncommutative coproduct of $f$ and $g$ is an additive monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$.

MonoidHom.noncommCoproddefMathlib.GroupTheory.NoncommCoprod, function or constant

Wording

the noncommutative coproduct of f and g (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $P$. Let $g$ be a monoid homomorphism of $N$ and $P$ such that for all elements $m$ of $M$, for all elements $n$ of $N$, $\mathrm{Commute}$ holds for $f$ applied to $m$ and $g$ applied to $n$. Then the noncommutative coproduct of $f$ and $g$ is a monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$.

MulHom.noncommCoproddefMathlib.GroupTheory.NoncommCoprod, function or constant

Wording

the noncommutative coproduct of f and g (from the name)

English

Let $f$ be a multiplicative homomorphism of $M$ and $P$. Let $g$ be a multiplicative homomorphism of $N$ and $P$ such that for all elements $m$ of $M$, for all elements $n$ of $N$, $\mathrm{Commute}$ holds for $f$ applied to $m$ and $g$ applied to $n$. Then the noncommutative coproduct of $f$ and $g$ is a multiplicative homomorphism of $\mathrm{Prod}$ applied to $M$ and $N$ and $P$.

Mathlib.GroupTheory.NoncommPiCoprod

AddMonoidHom.noncommPiCoproddefMathlib.GroupTheory.NoncommPiCoprod, function or constant

Wording

the noncommutative product coproduct of x4 and i2 (from the name)

English

Let $x_{4}$ be a function from elements $i_{2}$ of $x_{1}$ to additive monoid homomorphisms of $N$ applied to $i_{2}$ and $M$ such that the function that maps $i_{1}$ and $j$ to the proposition that for all elements $x_{5}$ of $N$ applied to $i_{1}$, for all elements $y$ of $N$ applied to $j$, $\mathrm{AddCommute}$ holds for $x_{4}$ applied to $i_{1}$ and $x_{5}$ and $x_{4}$ applied to $j$ and $y$ is pairwise. Then the noncommutative product coproduct of $i_{2}$ and $x_{4}$ is an additive monoid homomorphism of the set of functions from elements $i$ of $x_{1}$ to elements of $N$ applied to $i$ and $M$.

AddMonoidHom.noncommPiCoprodEquivdefMathlib.GroupTheory.NoncommPiCoprod, function or constant

Wording

the noncommutative product coproduct equivalence (from the name)

English

The noncommutative product coproduct equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {x_{5}}{\mathrm{Pairwise} (\lambda i . \lambda j . \mathrm{forall} (N (i), \lambda x_{6} . \mathrm{forall} (N (j), \lambda y . \mathrm{AddCommute} (x_{5} (i , x_{6}), x_{5} (j , y)))))})}{\mathrm{AddMonoidHom} (\mathrm{Elem} (x_{1})\rightarrow N (i_{1}), M)}$.

AddSubgroup.noncommPiCoproddefMathlib.GroupTheory.NoncommPiCoprod, function or constant

Wording

the noncommutative product coproduct of hcomm (from the name)

English

Assume that the function that maps $i_{1}$ and $j$ to the proposition that for all elements $x_{4}$ and $y$ of $G$, if $\MembershipmemMACRoT {H (i_{1})}{x_{4}}$, then if $\MembershipmemMACRoT {H (j)}{y}$, then $\mathrm{AddCommute}$ holds for $x_{4}$ and $y$ is pairwise. Then the noncommutative product coproduct of $\mathrm{hcomm}$ is an additive monoid homomorphism of the set of functions from elements $i$ of $x_{1}$ to elements of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H (i)}{x_{3}})}$ and $G$ defined as the noncommutative product coproduct of the function that maps $i$ to the subtype of $H$ applied to $i$ and $\mathrm{AddSubgroup\_\_addCommute\_subtype\_of\_addCommute}$ applied to $\mathrm{hcomm}$.

MonoidHom.noncommPiCoproddefMathlib.GroupTheory.NoncommPiCoprod, function or constant

Wording

the noncommutative product coproduct of x4 and i2 (from the name)

English

Let $x_{4}$ be a function from elements $i_{2}$ of $x_{1}$ to monoid homomorphisms of $N$ applied to $i_{2}$ and $M$ such that the function that maps $i_{1}$ and $j$ to the proposition that for all elements $x_{5}$ of $N$ applied to $i_{1}$, for all elements $y$ of $N$ applied to $j$, $\mathrm{Commute}$ holds for $x_{4}$ applied to $i_{1}$ and $x_{5}$ and $x_{4}$ applied to $j$ and $y$ is pairwise. Then the noncommutative product coproduct of $i_{2}$ and $x_{4}$ is a monoid homomorphism of the set of functions from elements $i$ of $x_{1}$ to elements of $N$ applied to $i$ and $M$.

MonoidHom.noncommPiCoprodEquivdefMathlib.GroupTheory.NoncommPiCoprod, function or constant

Wording

the noncommutative product coproduct equivalence (from the name)

English

The noncommutative product coproduct equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {x_{5}}{\mathrm{Pairwise} (\lambda i . \lambda j . \mathrm{forall} (N (i), \lambda x_{6} . \mathrm{forall} (N (j), \lambda y . \mathrm{Commute} (x_{5} (i , x_{6}), x_{5} (j , y)))))})}{\mathrm{MonoidHom} (\mathrm{Elem} (x_{1})\rightarrow N (i_{1}), M)}$.

Subgroup.noncommPiCoproddefMathlib.GroupTheory.NoncommPiCoprod, function or constant

Wording

the noncommutative product coproduct of hcomm (from the name)

English

Assume that the function that maps $i_{1}$ and $j$ to the proposition that for all elements $x_{4}$ and $y$ of $G$, if $\MembershipmemMACRoT {H (i_{1})}{x_{4}}$, then if $\MembershipmemMACRoT {H (j)}{y}$, then $\mathrm{Commute}$ holds for $x_{4}$ and $y$ is pairwise. Then the noncommutative product coproduct of $\mathrm{hcomm}$ is a monoid homomorphism of the set of functions from elements $i$ of $x_{1}$ to elements of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H (i)}{x_{3}})}$ and $G$ defined as the noncommutative product coproduct of the function that maps $i$ to the subtype of $H$ applied to $i$ and $\mathrm{Subgroup\_\_commute\_subtype\_of\_commute}$ applied to $\mathrm{hcomm}$.

Mathlib.GroupTheory.Order.Min

AddMonoid.minOrderdefMathlib.GroupTheory.Order.Min, function or constant

Wording

the minimum order of x (from the docstring)

English

Let $x$ be a set. Then the minimum order of $x$ is a natural number defined as the infimum of the function that maps $a$ to the infimum of the function that maps $\mathrm{\_ha}$ to the infimum of the function that maps $\mathrm{\_ha'}$ to the additive order of $a$.

Monoid.minOrderdefMathlib.GroupTheory.Order.Min, function or constant

Wording

the minimum order of x (from the docstring)

English

Mathlib.GroupTheory.OrderOfElement

IsOfFinAddOrderdefMathlib.GroupTheory.OrderOfElement, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $G$. Then $\mathrm{IsOfFinAddOrder}$ holds for $x_{1}$, if $\MembershipmemMACRoT {\operatorname{periodicPts} (\lambda x_{2} . x_{1} + x_{2})}{0}$.

IsOfFinAddOrder.addUnitdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the additive unit of hx (from the name)

English

Assume that $\mathrm{IsOfFinAddOrder}$ holds for $x_{1}$. Then the additive unit of $\mathrm{hx}$ is an additive unit of $M$.

IsOfFinOrderdefMathlib.GroupTheory.OrderOfElement, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $G$. Then $\mathrm{IsOfFinOrder}$ holds for $x_{1}$, if $\MembershipmemMACRoT {\operatorname{periodicPts} (\lambda x_{2} . x_{1} \times x_{2})}{1}$.

IsOfFinOrder.unitdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the unit of hx (from the name)

English

Assume that $\mathrm{IsOfFinOrder}$ holds for $x_{1}$. Then the unit of $\mathrm{hx}$ is a unit of $M$.

addOrderOfdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the additive order of x1 (from the name)

English

Let $x_{1}$ be an element of $G$. Then the additive order of $x_{1}$ is a natural number defined as the minimal period of the function that maps $x_{2}$ to $x_{1} + x_{2}$ and $0$.

addSubgroupOfIdempotentdefMathlib.GroupTheory.OrderOfElement, 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 $\EqtMACRoH {S + S}{S}$. Then the additive subgroup of $S$ is an additive subgroup of $G$.

addSubmonoidOfIdempotentdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the additive submonoid of S (from the name)

English

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

finEquivMultiplesdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the finite equivalence multiple of hx (from the name)

English

Assume that $\mathrm{IsOfFinAddOrder}$ holds for $x_{1}$. Then the finite equivalence multiple of $\mathrm{hx}$ is an element of $\EquivMACRoAE {\mathrm{Fin} (\mathrm{addOrderOf} (x_{1}))}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{multiples} (x_{1})}{x_{2}})})}$.

finEquivPowersdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the finite equivalence power of hx (from the name)

English

Assume that $\mathrm{IsOfFinOrder}$ holds for $x_{1}$. Then the finite equivalence power of $\mathrm{hx}$ is an element of $\EquivMACRoAE {\mathrm{Fin} (\mathrm{orderOf} (x_{1}))}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{powers} (x_{1})}{x_{2}})})}$.

finEquivZMultiplesdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the finite equivalence multiple of hx (from the name)

English

Assume that $\mathrm{IsOfFinAddOrder}$ holds for $x_{1}$. Then the finite equivalence multiple of $\mathrm{hx}$ is an equivalence from $\mathrm{Fin}$ applied to the additive order of $x_{1}$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (x_{1})}{x_{2}})}$ defined as the composition of the finite equivalence multiple of $\mathrm{hx}$ and the equivalence of $\mathrm{IsOfFinAddOrder\_\_multiples\_eq\_zmultiples}$ applied to $\mathrm{hx}$.

finEquivZPowersdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the finite equivalence power of hx (from the name)

English

Assume that $\mathrm{IsOfFinOrder}$ holds for $x_{1}$. Then the finite equivalence power of $\mathrm{hx}$ is an equivalence from $\mathrm{Fin}$ applied to the order of $x_{1}$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{zpowers} (x_{1})}{x_{2}})}$ defined as the composition of the finite equivalence power of $\mathrm{hx}$ and the equivalence of $\mathrm{IsOfFinOrder\_\_powers\_eq\_zpowers}$ applied to $\mathrm{hx}$.

multiplesEquivMultiplesdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the multiple equivalence multiple of h1 (from the name)

English

Assume that $\mathrm{addOrderOf} (x_{1})= \mathrm{addOrderOf} (y)$. Then the multiple equivalence multiple of $h_{1}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{multiples} (x_{1})}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{multiples} (y)}{x_{3}})})}$ defined as the composition of the inverse of the finite equivalence multiple of $\mathrm{isOfFinAddOrder\_of\_finite}$ applied to $x_{1}$ and the composition of the finite congruence of $h_{1}$ and the finite equivalence multiple of $\mathrm{isOfFinAddOrder\_of\_finite}$ applied to $y$.

nsmulCoprimedefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the natural multiple coprime of h (from the name)

English

Assume that the cardinality of $G$ and $n$ are coprime. Then the natural multiple coprime of $h$ is an equivalence from $G$ to $G$.

orderOfdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the order of x1 (from the name)

English

Let $x_{1}$ be an element of $G$. Then the order of $x_{1}$ is a natural number defined as the minimal period of the function that maps $x_{2}$ to $x_{1} \times x_{2}$ and $1$.

powCardSubgroupdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the power cardinality subgroup of S and hS (from the name)

English

Let $S$ be a nonempty element of $\wp G$. Then the power cardinality subgroup of $S$ and $\mathrm{hS}$ is a subgroup of $G$.

powCoprimedefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the power coprime of h (from the name)

English

Assume that the cardinality of $G$ and $n$ are coprime. Then the power coprime of $h$ is an equivalence from $G$ to $G$.

powersEquivPowersdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the power equivalence power of h1 (from the name)

English

Assume that $\mathrm{orderOf} (x_{1})= \mathrm{orderOf} (y)$. Then the power equivalence power of $h_{1}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{powers} (x_{1})}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{powers} (y)}{x_{3}})})}$ defined as the composition of the inverse of the finite equivalence power of $\mathrm{isOfFinOrder\_of\_finite}$ applied to $x_{1}$ and the composition of the finite congruence of $h_{1}$ and the finite equivalence power of $\mathrm{isOfFinOrder\_of\_finite}$ applied to $y$.

smulCardAddSubgroupdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the scalar multiple cardinality additive subgroup of S and hS (from the name)

English

Let $S$ be a nonempty element of $\wp G$. Then the scalar multiple cardinality additive subgroup of $S$ and $\mathrm{hS}$ is an additive subgroup of $G$.

subgroupOfIdempotentdefMathlib.GroupTheory.OrderOfElement, 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 $\EqtMACRoH {S \times S}{S}$. Then the subgroup of $S$ is a subgroup of $G$.

submonoidOfIdempotentdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

the submonoid of S (from the name)

English

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

zmultiplesEquivZMultiplesdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

no wording

English

Assume that the additive order of $x_{1}$ is equal to the additive order of $y$. Then $\mathrm{zmultiplesEquivZMultiples}$ applied to $h_{1}$ is an equivalence from $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (x_{1})}{x_{2}})}$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (y)}{x_{3}})}$.

zpowersEquivZPowersdefMathlib.GroupTheory.OrderOfElement, function or constant

Wording

no wording

English

Assume that the order of $x_{1}$ is equal to the order of $y$. Then $\mathrm{zpowersEquivZPowers}$ applied to $h_{1}$ is an equivalence from $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{zpowers} (x_{1})}{x_{2}})}$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{zpowers} (y)}{x_{3}})}$.

Mathlib.GroupTheory.OreLocalization.Basic

AddOreLocalizationdefMathlib.GroupTheory.OreLocalization.Basic, type

Wording

no wording

English

Let $S$ be an additive submonoid of $R$. Let $X$ be a set. Then an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$ is an element of the function that maps $S$ and $X$ to $\mathrm{Quotient}$ applied to $\operatorname{oreEqv}$ applied to $S$ and $X$.

AddOreLocalization.hvadddefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $c$ be an element of $R$. Let $x_{4}$ be an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$. Then $\operatorname{hvadd}$ applied to $c$ and $x_{4}$ is an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$.

AddOreLocalization.liftExpanddefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the lift expand of P and x3 (from the name)

English

Let $P$ be a function from elements of $X$ and elements of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$ to elements of $C$ such that for all elements $r$ of $X$, for all elements $t$ of $R$, for all elements $s$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, for all elements $\mathrm{ht}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{(t + s)}$, $P$ applied to $r$ and $s$ is equal to $P$ applied to the sum of $t$ and $r$ and $t + s$. Let $x_{3}$ be an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$. Then the lift expand of $P$ and $x_{3}$ is an element of $C$.

AddOreLocalization.lift₂ExpanddefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the lift expand of x3 and x4 (from the name)

English

Let $P$ be a function from elements of $X$ and elements of $\SubtypeSet {x_{18}}{(\MembershipmemMACRoT {S}{x_{18}})}$ and elements of $X$ and elements of $\SubtypeSet {x_{17}}{(\MembershipmemMACRoT {S}{x_{17}})}$ to elements of $C$ such that for all elements $x_{5}$ of $X$, for all elements $x_{6}$ of $R$, for all elements $x_{7}$ of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {S}{x_{12}})}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{(x_{6} + x_{7})}$, for all elements $x_{8}$ of $X$, for all elements $x_{9}$ of $R$, for all elements $x_{10}$ of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {S}{x_{11}})}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{(x_{9} + x_{10})}$, $P$ applied to $x_{5}$, $x_{7}$, $x_{8}$ and $x_{10}$ is equal to $P$ applied to the sum of $x_{6}$ and $x_{5}$, $x_{6} + x_{7}$, the sum of $x_{9}$ and $x_{8}$ and $x_{9} + x_{10}$. Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$. Then the lift expand of $x_{3}$ and $x_{4}$ is an element of $C$.

AddOreLocalization.nsmuldefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the natural multiple of x2 and x3 (from the name)

English

Let $x_{2}$ be a natural number. Let $x_{3}$ be an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $R$. Then the natural multiple of $x_{2}$ and $x_{3}$ is an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $R$ defined as $\mathrm{nsmulRec}$ applied to $x_{2}$ and $x_{3}$.

AddOreLocalization.numeratorAddUnitdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the numerator additive unit of s (from the name)

English

Let $s$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then the numerator additive unit of $s$ is an additive unit of $\mathrm{AddOreLocalization}$ applied to $S$ and $R$.

AddOreLocalization.numeratorHomdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the numerator homomorphism (from the name)

English

The numerator homomorphism is an additive monoid homomorphism of $R$ and $\mathrm{AddOreLocalization}$ applied to $S$ and $R$.

AddOreLocalization.oreSubdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $r$ be an element of $X$. Let $s$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{oreSub}$ applied to $r$ and $s$ is an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$ defined as $\operatorname{mk'}$ applied to $\ProdmkMACRoU {r}{s}$.

AddOreLocalization.oreSubAddChar'defMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $R$. Let $x_{4}$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$. Let $x_{5}$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$. Then $\operatorname{oreSubAddChar'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r'}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s'}$ to the proposition that $\EqtMACRoH {\mathrm{s'} + x_{2}}{\mathrm{r'} + x_{5}}$ and $\EqtMACRoH {\operatorname{oreSub} (x_{2} , x_{4})+ \operatorname{oreSub} (x_{3} , x_{5})}{\operatorname{oreSub} (\mathrm{r'} + x_{3} , \mathrm{s'} + x_{4})}$.

AddOreLocalization.oreSubVAddChar'defMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be an element of $R$. Let $x_{4}$ be an element of $X$. Let $x_{5}$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$. Let $x_{6}$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$. Then $\operatorname{oreSubVAddChar'}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r'}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s'}$ to the proposition that $\EqtMACRoH {\mathrm{s'} + x_{3}}{\mathrm{r'} + x_{6}}$ and the sum of $\operatorname{oreSub}$ applied to $x_{3}$ and $x_{5}$ and $\operatorname{oreSub}$ applied to $x_{4}$ and $x_{6}$ is equal to $\operatorname{oreSub}$ applied to the sum of $\mathrm{r'}$ and $x_{4}$ and $\mathrm{s'} + x_{5}$.

AddOreLocalization.universalAddHomdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the universal additive homomorphism of f and fS (from the name)

English

Let $f$ be an additive monoid homomorphism of $R$ and $T$. Let $\mathrm{fS}$ be an additive monoid homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and the set of additive units of $T$ such that for all elements $s$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, $f$ applied to $s$ is equal to the underlying value in the base of $\mathrm{fS}$ applied to $s$. Then the universal additive homomorphism of $f$ and $\mathrm{fS}$ is an additive monoid homomorphism of $\mathrm{AddOreLocalization}$ applied to $S$ and $R$ and $T$.

AddOreLocalization.vadddefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the vector sum of y and x3 (from the name)

English

Let $y$ be an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $R$. Let $x_{3}$ be an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$. Then the vector sum of $y$ and $x_{3}$ is an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$.

AddOreLocalization.zerodefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the zero (from the name)

English

The zero is an element of $\mathrm{AddOreLocalization}$ applied to $S$ and $X$ defined as $\operatorname{oreSub}$ applied to $0$ and $0$.

OreLocalizationdefMathlib.GroupTheory.OreLocalization.Basic, type

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $X$ be a set. Then an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$ is an element of the function that maps $S$ and $X$ to $\mathrm{Quotient}$ applied to $\operatorname{oreEqv}$ applied to $S$ and $X$.

OreLocalization.hsmuldefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $c$ be an element of $R$. Let $x_{4}$ be an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$. Then $\operatorname{hsmul}$ applied to $c$ and $x_{4}$ is an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$.

OreLocalization.liftExpanddefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the lift expand of P and x3 (from the name)

English

Let $P$ be a function from elements of $X$ and elements of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$ to elements of $C$ such that for all elements $r$ of $X$, for all elements $t$ of $R$, for all elements $s$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, for all elements $\mathrm{ht}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{(t \times s)}$, $\EqtMACRoH {P (r , s)}{P (\HSMulhSMulMACRoAL {t}{r}, t \times s)}$. Let $x_{3}$ be an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$. Then the lift expand of $P$ and $x_{3}$ is an element of $C$.

OreLocalization.lift₂ExpanddefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the lift expand of x3 and x4 (from the name)

English

Let $P$ be a function from elements of $X$ and elements of $\SubtypeSet {x_{18}}{(\MembershipmemMACRoT {S}{x_{18}})}$ and elements of $X$ and elements of $\SubtypeSet {x_{17}}{(\MembershipmemMACRoT {S}{x_{17}})}$ to elements of $C$ such that for all elements $x_{5}$ of $X$, for all elements $x_{6}$ of $R$, for all elements $x_{7}$ of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {S}{x_{12}})}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{(x_{6} \times x_{7})}$, for all elements $x_{8}$ of $X$, for all elements $x_{9}$ of $R$, for all elements $x_{10}$ of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {S}{x_{11}})}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{(x_{9} \times x_{10})}$, $\EqtMACRoH {P (x_{5} , x_{7} , x_{8} , x_{10})}{P (\HSMulhSMulMACRoAL {x_{6}}{x_{5}}, x_{6} \times x_{7} , \HSMulhSMulMACRoAL {x_{9}}{x_{8}}, x_{9} \times x_{10})}$. Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{OreLocalization}$ applied to $S$ and $X$. Then the lift expand of $x_{3}$ and $x_{4}$ is an element of $C$.

OreLocalization.npowdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the natural power of x2 and x3 (from the name)

English

Let $x_{2}$ be a natural number. Let $x_{3}$ be an element of $\mathrm{OreLocalization}$ applied to $S$ and $R$. Then the natural power of $x_{2}$ and $x_{3}$ is an element of $\mathrm{OreLocalization}$ applied to $S$ and $R$ defined as $\mathrm{npowRec}$ applied to $x_{2}$ and $x_{3}$.

OreLocalization.numeratorHomdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the numerator homomorphism (from the name)

English

The numerator homomorphism is a monoid homomorphism of $R$ and $\mathrm{OreLocalization}$ applied to $S$ and $R$.

OreLocalization.numeratorUnitdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the numerator unit of s (from the name)

English

Let $s$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then the numerator unit of $s$ is a unit of $\mathrm{OreLocalization}$ applied to $S$ and $R$.

OreLocalization.onedefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the one (from the name)

English

The one is an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$ defined as $\operatorname{oreDiv}$ applied to $1$ and $1$.

OreLocalization.oreDivdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $r$ be an element of $X$. Let $s$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{oreDiv}$ applied to $r$ and $s$ is an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$ defined as $\operatorname{mk'}$ applied to $\ProdmkMACRoU {r}{s}$.

OreLocalization.oreDivMulChar'defMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $R$. Let $x_{4}$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$. Let $x_{5}$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$. Then $\operatorname{oreDivMulChar'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r'}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s'}$ to the proposition that $\EqtMACRoH {\mathrm{s'} \times x_{2}}{\mathrm{r'} \times x_{5}}$ and $\EqtMACRoH {\operatorname{oreDiv} (x_{2} , x_{4})\times \operatorname{oreDiv} (x_{3} , x_{5})}{\operatorname{oreDiv} (\mathrm{r'} \times x_{3} , \mathrm{s'} \times x_{4})}$.

OreLocalization.oreDivSMulChar'defMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be an element of $R$. Let $x_{4}$ be an element of $X$. Let $x_{5}$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$. Let $x_{6}$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$. Then $\operatorname{oreDivSMulChar'}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r'}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s'}$ to the proposition that $\EqtMACRoH {\mathrm{s'} \times x_{3}}{\mathrm{r'} \times x_{6}}$ and $\EqtMACRoH {\HSMulhSMulMACRoAL {\operatorname{oreDiv} (x_{3} , x_{5})}{\operatorname{oreDiv} (x_{4} , x_{6})}}{\operatorname{oreDiv} (\HSMulhSMulMACRoAL {\mathrm{r'}}{x_{4}}, \mathrm{s'} \times x_{5})}$.

OreLocalization.smuldefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the scalar multiple of y and x3 (from the name)

English

Let $y$ be an element of $\mathrm{OreLocalization}$ applied to $S$ and $R$. Let $x_{3}$ be an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$. Then the scalar multiple of $y$ and $x_{3}$ is an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$.

OreLocalization.universalMulHomdefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the universal multiplicative homomorphism of f and fS (from the name)

English

Let $f$ be a monoid homomorphism of $R$ and $T$. Let $\mathrm{fS}$ be a monoid homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and $\UnitsMACRoAO {T}$ such that for all elements $s$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, $f$ applied to $s$ is equal to the underlying value in the base of $\mathrm{fS}$ applied to $s$. Then the universal multiplicative homomorphism of $f$ and $\mathrm{fS}$ is a monoid homomorphism of $\mathrm{OreLocalization}$ applied to $S$ and $R$ and $T$.

OreLocalization.zerodefMathlib.GroupTheory.OreLocalization.Basic, function or constant

Wording

the zero (from the name)

English

The zero is an element of $\mathrm{OreLocalization}$ applied to $S$ and $X$ defined as $\operatorname{oreDiv}$ applied to $0$ and $1$.

Mathlib.GroupTheory.OreLocalization.OreSet

AddOreLocalization.AddOreSetclassMathlib.GroupTheory.OreLocalization.OreSet, predicate

Wording

no wording

English

Let $S$ be an additive submonoid of $R$. Then we can say that $\operatorname{AddOreSet}$ holds for $S$.

AddOreLocalization.AddOreSet.oreMindefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $x_{2}$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{oreMin}$ applied to $x_{1}$ and $x_{2}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

AddOreLocalization.AddOreSet.oreSubtradefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $x_{2}$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$. Then $\operatorname{oreSubtra}$ applied to $x_{1}$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

AddOreLocalization.addOreConditiondefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $s$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then $\operatorname{addOreCondition}$ applied to $r$ and $s$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r'}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s'}$ to $\EqtMACRoH {(\mathrm{s'} + r)}{(\mathrm{r'} + s)}$ defined as $\operatorname{mk}$ applied to $\operatorname{oreMin}$ applied to $r$ and $s$ and $\operatorname{mk}$ applied to $\operatorname{oreSubtra}$ applied to $r$ and $s$ and $\mathrm{AddOreLocalization\_\_add\_ore\_eq}$ applied to $r$ and $s$.

AddOreLocalization.oreMindefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $s$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then $\operatorname{oreMin}$ applied to $r$ and $s$ is an element of $R$ defined as $\operatorname{oreMin}$ applied to $r$ and $s$.

AddOreLocalization.oreSubtradefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $s$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{oreSubtra}$ applied to $r$ and $s$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ defined as $\operatorname{oreSubtra}$ applied to $r$ and $s$.

OreLocalization.OreSetclassMathlib.GroupTheory.OreLocalization.OreSet, predicate

Wording

no wording

English

Let $S$ be a submonoid of $R$. Then we can say that $\operatorname{OreSet}$ holds for $S$.

OreLocalization.OreSet.oreDenomdefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $x_{2}$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$. Then $\operatorname{oreDenom}$ applied to $x_{1}$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

OreLocalization.OreSet.oreNumdefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $x_{2}$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{oreNum}$ applied to $x_{1}$ and $x_{2}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

OreLocalization.oreConditiondefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $s$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then $\operatorname{oreCondition}$ applied to $r$ and $s$ is an element of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{r'}$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{s'}$ to $\EqtMACRoH {(\mathrm{s'} \times r)}{(\mathrm{r'} \times s)}$ defined as $\operatorname{mk}$ applied to $\operatorname{oreNum}$ applied to $r$ and $s$ and $\operatorname{mk}$ applied to $\operatorname{oreDenom}$ applied to $r$ and $s$ and $\mathrm{OreLocalization\_\_ore\_eq}$ applied to $r$ and $s$.

OreLocalization.oreDenomdefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $s$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{oreDenom}$ applied to $r$ and $s$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ defined as $\operatorname{oreDenom}$ applied to $r$ and $s$.

OreLocalization.oreNumdefMathlib.GroupTheory.OreLocalization.OreSet, function or constant

Wording

no wording

English

Let $r$ be an element of $R$. Let $s$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then $\operatorname{oreNum}$ applied to $r$ and $s$ is an element of $R$ defined as $\operatorname{oreNum}$ applied to $r$ and $s$.

Mathlib.GroupTheory.PGroup

IsAddPGroupdefMathlib.GroupTheory.PGroup, predicate

Wording

p is a additive group (from the name)

English

Let $p$ be a natural number. Let $G$ be a set. Then $p$ is an additive group, if for all elements $g$ of $G$, there exists a natural number $k$, such that $\EqtMACRoH {\HSMulhSMulMACRoAL {(p ^ {k})}{g}}{0}$.

IsAddPGroup.nsmulEquivdefMathlib.GroupTheory.PGroup, function or constant

Wording

the natural multiple equivalence of hG and hn (from the name)

English

Assume that $p$ is an additive group. Assume that $p$ and $n$ are coprime. Then the natural multiple equivalence of $\mathrm{hG}$ and $\mathrm{hn}$ is an equivalence from $G$ to $G$.

IsAddPGroup.nsmulEquiv'defMathlib.GroupTheory.PGroup, function or constant

Wording

the natural multiple equivalence of hG and hn (from the name)

English

Assume that $p$ is an additive group. Assume that $p$ does not divide $n$. Then the natural multiple equivalence of $\mathrm{hG}$ and $\mathrm{hn}$ is an equivalence from $G$ to $G$.

IsPGroupdefMathlib.GroupTheory.PGroup, predicate

Wording

p is a group (from the name)

English

Let $p$ be a natural number. Let $G$ be a set. Then $p$ is a group, if for all elements $g$ of $G$, there exists a natural number $k$, such that $\EqtMACRoH {g ^ {p ^ {k}}}{1}$.

IsPGroup.powEquivdefMathlib.GroupTheory.PGroup, function or constant

Wording

the power equivalence of hG and hn (from the name)

English

Assume that $p$ is a group. Assume that $p$ and $n$ are coprime. Then the power equivalence of $\mathrm{hG}$ and $\mathrm{hn}$ is an equivalence from $G$ to $G$.

IsPGroup.powEquiv'defMathlib.GroupTheory.PGroup, function or constant

Wording

the power equivalence of hG and hn (from the name)

English

Assume that $p$ is a group. Assume that $p$ does not divide $n$. Then the power equivalence of $\mathrm{hG}$ and $\mathrm{hn}$ is an equivalence from $G$ to $G$.

Mathlib.GroupTheory.Perm.Centralizer

Equiv.Perm.BasisstructureMathlib.GroupTheory.Perm.Centralizer, type

Wording

basis of g (from the name)

English

Let $g$ be a permutation of $x$. Then the bases of $g$ are a basic type.

Equiv.Perm.Basis.ofPermHomdefMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

the basis of a (from the name)

English

Let $a$ be a basis of $g$. Then the basis of $a$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{Equiv\_\_Perm\_\_OnCycleFactors\_\_range\_toPermHom'} (g)}{x_{3}})}$ and the set of permutations of $x$.

Equiv.Perm.Basis.ofPermHomFundefMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

the basis of x3 and x4 (from the name)

English

Let $a$ be a basis of $g$. Let $x_{3}$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{Equiv\_\_Perm\_\_OnCycleFactors\_\_range\_toPermHom'} (g)}{x_{5}})}$. Let $x_{4}$ be an element of $x$. Then the basis of $x_{3}$ and $x_{4}$ is an element of $x$.

Equiv.Perm.Basis.toCentralizerdefMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

the centralizer of a (from the name)

English

Let $a$ be a basis of $g$. Then the centralizer of $a$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{Equiv\_\_Perm\_\_OnCycleFactors\_\_range\_toPermHom'} (g)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{centralizer} (\operatorname{singleton} (g))}{x_{4}})}$.

Equiv.Perm.Basis.toFundefMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

the basis of self and x3 (from the name)

English

Let $\mathrm{self}$ be a basis of $g$. Let $x_{3}$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{cycleFactorsFinset} (g)}{x_{4}})}$. Then the basis of $\mathrm{self}$ and $x_{3}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

Equiv.Perm.OnCycleFactors.kerParamdefMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

no wording

English

Let $g$ be a permutation of $x$. Then $\operatorname{kerParam}$ applied to $g$ is a monoid homomorphism of $\mathrm{Prod}$ applied to the set of permutations of the set of elements of the fixed point of $\operatorname{coe}$ applied to $g$ and the set of functions from elements $c$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{cycleFactorsFinset} (g)}{x_{4}})}$ to elements of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{zpowers} (c)}{x_{3}})}$ and the set of permutations of $x$ defined as the noncommutative coproduct of the permutation and the noncommutative product coproduct of $\mathrm{Equiv\_\_Perm\_\_pairwise\_commute\_of\_mem\_zpowers}$ applied to $g$.

Equiv.Perm.OnCycleFactors.range_toPermHom'defMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

the range of g (from the docstring)

English

Let $g$ be a permutation of $x$. Then the range of $g$ is a subgroup of the set of permutations of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{cycleFactorsFinset} (g)}{x_{3}})}$.

Equiv.Perm.OnCycleFactors.toPermHomdefMathlib.GroupTheory.Perm.Centralizer, function or constant

Wording

the permutation homomorphism of g (from the name)

English

Let $g$ be a permutation of $x$. Then the permutation homomorphism of $g$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{centralizer} (\operatorname{singleton} (g))}{x_{3}})}$ and the set of permutations of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{cycleFactorsFinset} (g)}{x_{4}})}$ defined as the permutation homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{centralizer} (\operatorname{singleton} (g))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{cycleFactorsFinset} (g)}{x_{4}})}$.

Mathlib.GroupTheory.Perm.Cycle.Basic

Equiv.Perm.IsCycledefMathlib.GroupTheory.Perm.Cycle.Basic, predicate

Wording

f is a cycle (from the name)

English

Let $f$ be a permutation of $x$. Then $f$ is a cycle, if there exists an element $x_{1}$ of $x$, such that $f (x_{1})\neq x_{1}$ and for all elements $y$ of $x$, if $f (y)\neq y$, then $\operatorname{SameCycle}$ holds for $f$, $x_{1}$ and $y$.

Equiv.Perm.IsCycle.zpowersEquivSupportdefMathlib.GroupTheory.Perm.Cycle.Basic, function or constant

Wording

no wording

English

Assume that $x_{3}$ is a cycle. Then $\operatorname{zpowersEquivSupport}$ applied to $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zpowers} (x_{3})}{x_{4}})})}{(\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{support} (x_{3})}{x_{5}})})}$.

Equiv.Perm.IsCycleOndefMathlib.GroupTheory.Perm.Cycle.Basic, predicate

Wording

no wording

English

Let $f$ be a permutation of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{IsCycleOn}$ holds for $f$ and $s$, if $\operatorname{BijOn}$ holds for $\operatorname{coe}$ applied to $f$, $s$ and $s$ and for all elements $x_{1}$ of $x$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $x$, if $y$ is an element of $s$, then $\operatorname{SameCycle}$ holds for $f$, $x_{1}$ and $y$.

Equiv.Perm.SameCycledefMathlib.GroupTheory.Perm.Cycle.Basic, predicate

Wording

no wording

English

Let $f$ be a permutation of $x$. Let $x_{1}$ and $y$ be elements of $x$. Then $\operatorname{SameCycle}$ holds for $f$, $x_{1}$ and $y$, if there exists an integer $i$, such that $\EqtMACRoH {\operatorname{hPow} (f , i , x_{1})}{y}$.

Equiv.Perm.subtypePermOfSupportdefMathlib.GroupTheory.Perm.Cycle.Basic, function or constant

Wording

the subtype permutation of c (from the name)

English

Let $c$ be a permutation of $x$. Then the subtype permutation of $c$ is a permutation of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{support} (c)}{x_{3}})}$ defined as the subtype permutation of $c$ and the function that maps $x_{3}$ to $\mathrm{Equiv\_\_Perm\_\_apply\_mem\_support}$.

Equiv.Perm.subtypePerm_of_support_ledefMathlib.GroupTheory.Perm.Cycle.Basic, function or constant

Wording

the subtype permutation of c and hcs (from the name)

English

Let $c$ be a permutation of $x$ such that the support of $c$ is less than or equal to $s$. Then the subtype permutation of $c$ and $\mathrm{hcs}$ is a permutation of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ defined as the subtype permutation of $c$ and $\mathrm{Equiv\_\_Perm\_\_isInvariant\_of\_support\_le}$ applied to $\mathrm{hcs}$.

Mathlib.GroupTheory.Perm.Cycle.Concrete

Cycle.formPermdefMathlib.GroupTheory.Perm.Cycle.Concrete, function or constant

Wording

the form permutation of s and h (from the name)

English

Let $s$ be a cycle of $x$ such that $\operatorname{Nodup}$ holds for $s$. Then the form permutation of $s$ and $h$ is a permutation of $x$.

Equiv.Perm.isoCycledefMathlib.GroupTheory.Perm.Cycle.Concrete, function or constant

Wording

the isomorphism cycle (from the name)

English

The isomorphism cycle is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\operatorname{IsCycle} (f)})}{(\SubtypeSet {s}{\mathrm{and} (\operatorname{Nodup} (s), \operatorname{Nontrivial} (s))})}$.

Equiv.Perm.isoCycle'defMathlib.GroupTheory.Perm.Cycle.Concrete, function or constant

Wording

the isomorphism cycle (from the name)

English

The isomorphism cycle is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\operatorname{IsCycle} (f)})}{(\SubtypeSet {s}{\mathrm{and} (\operatorname{Nodup} (s), \operatorname{Nontrivial} (s))})}$.

Equiv.Perm.toCycledefMathlib.GroupTheory.Perm.Cycle.Concrete, function or constant

Wording

the cycle of f and hf (from the name)

English

Let $f$ be a permutation of $x$ such that $f$ is a cycle. Then the cycle of $f$ and $\mathrm{hf}$ is a cycle of $x$.

Equiv.Perm.toListdefMathlib.GroupTheory.Perm.Cycle.Concrete, function or constant

Wording

the list of p and x3 (from the name)

English

Let $p$ be a permutation of $x$. Let $x_{3}$ be an element of $x$. Then the list of $p$ and $x_{3}$ is a list of elements of $x$ defined as $\operatorname{iterate}$ applied to $\operatorname{coe}$ applied to $p$, $x_{3}$ and the cardinality of the support of the cycle of $p$ and $x_{3}$.

Mathlib.GroupTheory.Perm.Cycle.Factors

Equiv.Perm.cycleFactorsdefMathlib.GroupTheory.Perm.Cycle.Factors, function or constant

Wording

the cycle factor of f (from the name)

English

Let $f$ be a permutation of $x$. Then the cycle factor of $f$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{prod} (l)}{f}, \mathrm{and} (\mathrm{forall} (\operatorname{Perm} (x), \lambda g . \mathrm{if} (\MembershipmemMACRoT {l}{g}, \operatorname{IsCycle} (g))), \operatorname{Pairwise} (\operatorname{Disjoint} , l)))}$.

Equiv.Perm.cycleFactorsFinsetdefMathlib.GroupTheory.Perm.Cycle.Factors, function or constant

Wording

the cycle factor finite set of f (from the name)

English

Let $f$ be a permutation of $x$. Then the cycle factor finite set of $f$ is a finite set of the set of permutations of $x$.

Equiv.Perm.cycleOfdefMathlib.GroupTheory.Perm.Cycle.Factors, function or constant

Wording

the cycle of f and x2 (from the name)

English

Let $f$ be a permutation of $x$. Let $x_{2}$ be an element of $x$. Then the cycle of $f$ and $x_{2}$ is a permutation of $x$ defined as $\operatorname{ofSubtype}$ applied to the subtype permutation of $f$ and the function that maps $x_{4}$ to $\mathrm{Equiv\_\_Perm\_\_sameCycle\_apply\_right}$.

Equiv.Perm.truncCycleFactorsdefMathlib.GroupTheory.Perm.Cycle.Factors, function or constant

Wording

the truncation cycle factor of f (from the name)

English

Let $f$ be a permutation of $x$. Then the truncation cycle factor of $f$ is a truncation of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{prod} (l)}{f}, \mathrm{and} (\mathrm{forall} (\operatorname{Perm} (x), \lambda g . \mathrm{if} (\MembershipmemMACRoT {l}{g}, \operatorname{IsCycle} (g))), \operatorname{Pairwise} (\operatorname{Disjoint} , l)))}$.

Mathlib.GroupTheory.Perm.Cycle.Type

Equiv.Perm.IsThreeCycledefMathlib.GroupTheory.Perm.Cycle.Type, predicate

Wording

no wording

English

Let $x_{3}$ be a permutation of $x$. Then $\operatorname{IsThreeCycle}$ holds for $x_{3}$, if the cycle type of $x_{3}$ is equal to $\operatorname{singleton}$ applied to $3$.

Equiv.Perm.VectorsProdEqOne.equivVectordefMathlib.GroupTheory.Perm.Cycle.Type, function or constant

Wording

the equivalence vector of G and n (from the name)

English

Let $G$ be a set. Let $n$ be a natural number. Then the equivalence vector of $G$ and $n$ is an equivalence from the set of elements of $\operatorname{vectorsProdEqOne}$ applied to $G$ and $n$ to the set of vectors of $G$ and $n - 1$.

Equiv.Perm.VectorsProdEqOne.rotatedefMathlib.GroupTheory.Perm.Cycle.Type, function or constant

Wording

no wording

English

Let $v$ be an element of $\operatorname{vectorsProdEqOne}$ applied to $G$ and $n$. Let $k$ be a natural number. Then $\operatorname{rotate}$ applied to $v$ and $k$ is an element of $\operatorname{vectorsProdEqOne}$ applied to $G$ and $n$ defined as $\operatorname{rotate}$ applied to $v$ and $k$.

Equiv.Perm.VectorsProdEqOne.vectorEquivdefMathlib.GroupTheory.Perm.Cycle.Type, function or constant

Wording

the vector equivalence of G and n (from the name)

English

Let $G$ be a set. Let $n$ be a natural number. Then the vector equivalence of $G$ and $n$ is an equivalence from the set of vectors of $G$ and $n$ to the set of elements of $\operatorname{vectorsProdEqOne}$ applied to $G$ and $n + 1$.

Equiv.Perm.cycleTypedefMathlib.GroupTheory.Perm.Cycle.Type, function or constant

Wording

the cycle type of x3 (from the docstring)

English

Let $x_{3}$ be a permutation of $x$. Then the cycle type of $x_{3}$ is a multiset of $\Natural$ defined as the map of $\operatorname{comp}$ applied to $\FinsetcardMACRoM$ and $\operatorname{support}$ and the value of the cycle factor finite set of $x_{3}$.

Equiv.Perm.partitiondefMathlib.GroupTheory.Perm.Cycle.Type, function or constant

Wording

the partition corresponding to a permutation of x3 (from the docstring)

English

Let $x_{3}$ be a permutation of $x$. Then the partition corresponding to a permutation of $x_{3}$ is a partition of the cardinality of $x$.

Equiv.Perm.vectorsProdEqOnedefMathlib.GroupTheory.Perm.Cycle.Type, function or constant

Wording

no wording

English

Let $G$ be a set. Let $n$ be a natural number. Then $\operatorname{vectorsProdEqOne}$ applied to $G$ and $n$ is an element of the power set of the set of vectors of $G$ and $n$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that $\operatorname{prod}$ applied to the list of $v$ is equal to $1$.

Mathlib.GroupTheory.Perm.DomMulAct

DomMulAct.stabilizerEquiv_invFundefMathlib.GroupTheory.Perm.DomMulAct, function or constant

Wording

the stabilizer equivalence inverse function of g and i (from the name)

English

Let $g$ be a function from elements $i$ of $x_{1}$ to permutations of $\SubtypeSet {a_{1}}{(\EqtMACRoH {f (a_{1})}{i})}$. Let $a$ be an element of $x$. Then the stabilizer equivalence inverse function of $i$ and $g$ is an element of $x$ defined as the function that maps $a$ to $i$ applied to $f$ applied to $g$, $g$ and $a$.

DomMulAct.stabilizerMulEquivdefMathlib.GroupTheory.Perm.DomMulAct, function or constant

Wording

the stabilizer multiplicative equivalence of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the stabilizer multiplicative equivalence of $f$ is a multiplicative equivalence of the set of multiplicative opposites of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (\mathrm{DomMulAct} (\operatorname{Perm} (x)), f)}{x_{2}})}$ and the set of functions from elements $i$ of $x_{1}$ to permutations of $\SubtypeSet {a}{(\EqtMACRoH {f (a)}{i})}$.

Mathlib.GroupTheory.Perm.Fin

Equiv.Perm.decomposeFindefMathlib.GroupTheory.Perm.Fin, function or constant

Wording

no wording

English

$\operatorname{decomposeFin}$ is an equivalence from the set of permutations of $\mathrm{Fin}$ applied to the successor of $n$ to $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to the successor of $n$ and the set of permutations of $\mathrm{Fin}$ applied to $n$ defined as the composition of the composition of the permutation congruence of the finite successor equivalence of $n$ and $\operatorname{decomposeOption}$ and the product congruence of the inverse of the finite successor equivalence of $n$ and the identity of the set of permutations of $\mathrm{Fin}$ applied to $n$.

Equiv.Perm.decomposeFin'defMathlib.GroupTheory.Perm.Fin, function or constant

Wording

no wording

English

$\operatorname{decomposeFin'}$ is an equivalence from the set of permutations of $\mathrm{Fin}$ applied to $n + 2$ to $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $n + 2$ and the set of permutations of $\mathrm{Fin}$ applied to $n + 1$ defined as the inverse of the equivalence of $\operatorname{uncurry}$ applied to $\operatorname{decomposeFin'Symm}$ and $\mathrm{Equiv\_\_Perm\_\_decomposeFin'Symm\_uncurry\_bijective}$ applied to $n$.

Equiv.Perm.decomposeFin'SymmdefMathlib.GroupTheory.Perm.Fin, function or constant

Wording

no wording

English

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Let $x$ be a permutation of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{decomposeFin'Symm}$ applied to $i$ and $x$ is a permutation of $\mathrm{Fin}$ applied to $n + 2$.

Fin.cycleIccdefMathlib.GroupTheory.Perm.Fin, function or constant

Wording

the cycle closed interval of i and j (from the name)

English

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n$. Then the cycle closed interval of $i$ and $j$ is a permutation of $\mathrm{Fin}$ applied to $n$.

Fin.cycleRangedefMathlib.GroupTheory.Perm.Fin, function or constant

Wording

the cycle range of i (from the name)

English

Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the cycle range of $i$ is a permutation of $\mathrm{Fin}$ applied to $n$.

Mathlib.GroupTheory.Perm.Finite

Equiv.Perm.subtypePermOfFintypedefMathlib.GroupTheory.Perm.Finite, function or constant

Wording

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

English

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

Mathlib.GroupTheory.Perm.List

List.formPermdefMathlib.GroupTheory.Perm.List, function or constant

Wording

the form permutation of l (from the name)

English

Let $l$ be a list of elements of $x$. Then the form permutation of $l$ is a permutation of $x$ defined as $\operatorname{prod}$ applied to $\operatorname{zipWith}$ applied to $\operatorname{swap}$, $l$ and $\operatorname{tail}$ applied to $l$.

Mathlib.GroupTheory.Perm.Option

Equiv.Perm.decomposeOptiondefMathlib.GroupTheory.Perm.Option, function or constant

Wording

no wording

English

$\operatorname{decomposeOption}$ is an equivalence from the set of permutations of $\mathrm{Option}$ applied to $x$ to $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $x$ and the set of permutations of $x$.

Mathlib.GroupTheory.Perm.Sign

Equiv.Perm.finPairsLTdefMathlib.GroupTheory.Perm.Sign, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{finPairsLT}$ applied to $n$ is a finite set of $\Sigma$ applied to the function that maps $x$ to $\mathrm{Fin}$ applied to $n$.

Equiv.Perm.ofSigndefMathlib.GroupTheory.Perm.Sign, function or constant

Wording

the permutation of s (from the name)

English

Let $s$ be a unit of $\Integer$. Then the permutation of $s$ is a finite set of the set of permutations of $x$ defined as $\FinsetFilter {x_{3}}{(\EqtMACRoH {\operatorname{sign} (x_{3})}{s})}{\FinsetunivMACRoAC}$.

Equiv.Perm.signdefMathlib.GroupTheory.Perm.Sign, function or constant

Wording

the sign (from the name)

English

The sign is a monoid homomorphism of the set of permutations of $x$ and $\UnitsMACRoAO {\Integer}$.

Equiv.Perm.signAux2defMathlib.GroupTheory.Perm.Sign, function or constant

Wording

the sign of x2 and x3 (from the name)

English

Let $x_{2}$ be a list of elements of $x$. Let $x_{3}$ be a permutation of $x$. Then the sign of $x_{2}$ and $x_{3}$ is a unit of $\Integer$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Equiv\_\_Perm\_\_signAux2\_\_\_f}$ and $x_{3}$.

Equiv.Perm.signAux3defMathlib.GroupTheory.Perm.Sign, function or constant

Wording

the sign of f and h1 (from the name)

English

Let $f$ be a permutation of $x$. Assume that for all elements $x_{2}$ of $x$, $x_{2}$ is an element of $s$. Then the sign of $f$ and $h_{1}$ is a unit of $\Integer$.

Equiv.Perm.swapFactorsdefMathlib.GroupTheory.Perm.Sign, function or constant

Wording

the swap factor of f (from the name)

English

Let $f$ be a permutation of $x$. Then the swap factor of $f$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{prod} (l)}{f}, \mathrm{forall} (\operatorname{Perm} (x), \lambda g . \mathrm{if} (\MembershipmemMACRoT {l}{g}, \operatorname{IsSwap} (g))))}$.

Equiv.Perm.truncSwapFactorsdefMathlib.GroupTheory.Perm.Sign, function or constant

Wording

the truncation swap factor of f (from the name)

English

Let $f$ be a permutation of $x$. Then the truncation swap factor of $f$ is a truncation of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{prod} (l)}{f}, \mathrm{forall} (\operatorname{Perm} (x), \lambda g . \mathrm{if} (\MembershipmemMACRoT {l}{g}, \operatorname{IsSwap} (g))))}$.

Mathlib.GroupTheory.Perm.Subgroup

Equiv.Perm.subgroupOfMulActiondefMathlib.GroupTheory.Perm.Subgroup, function or constant

Wording

the subgroup of G and H (from the name)

English

Let $G$ and $H$ be sets. Then the subgroup of $G$ and $H$ is a multiplicative equivalence of $G$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toPermHom} (G , H))}{x_{2}})}$.

Mathlib.GroupTheory.Perm.Support

Equiv.Perm.DisjointdefMathlib.GroupTheory.Perm.Support, predicate

Wording

f is disjoint to g (from the name)

English

Let $f$ and $g$ be permutations of $x$. Then $f$ is disjoint to $g$, if for all elements $x_{1}$ of $x$, $\EqtMACRoH {f (x_{1})}{x_{1}}$ or $\EqtMACRoH {g (x_{1})}{x_{1}}$.

Equiv.Perm.IsSwapdefMathlib.GroupTheory.Perm.Support, predicate

Wording

f is a swap (from the name)

English

Let $f$ be a permutation of $x$. Then $f$ is a swap, if there exist elements $x_{2}$ and $y$ of $x$, such that $x_{2} \neq y$ and $f$ is equal to the swap of $x_{2}$ and $y$.

Equiv.Perm.supportdefMathlib.GroupTheory.Perm.Support, function or constant

Wording

the support of f (from the name)

English

Let $f$ be a permutation of $x$. Then the support of $f$ is a finite set of $x$ defined as $\FinsetFilter {x_{3}}{\mathrm{Neq} (f (x_{3}), x_{3})}{\FinsetunivMACRoAC}$.

Mathlib.GroupTheory.Perm.ViaEmbedding

Equiv.Perm.viaEmbeddingdefMathlib.GroupTheory.Perm.ViaEmbedding, function or constant

Wording

no wording

English

Let $e$ be a permutation of $x$. Let $x_{2}$ be an embedding of $x$ and $x_{1}$. Then $\operatorname{viaEmbedding}$ applied to $e$ and $x_{2}$ is a permutation of $x_{1}$ defined as $\operatorname{extendDomain}$ applied to $e$ and the equivalence of $\operatorname{toFun}$ applied to $x_{2}$ and $\operatorname{inj'}$ applied to $x_{2}$.

Equiv.Perm.viaEmbeddingHomdefMathlib.GroupTheory.Perm.ViaEmbedding, function or constant

Wording

no wording

English

Let $x_{2}$ be an embedding of $x$ and $x_{1}$. Then $\operatorname{viaEmbeddingHom}$ applied to $x_{2}$ is a monoid homomorphism of the set of permutations of $x$ and the set of permutations of $x_{1}$ defined as $\operatorname{extendDomainHom}$ applied to the equivalence of $\operatorname{toFun}$ applied to $x_{2}$ and $\operatorname{inj'}$ applied to $x_{2}$.

Mathlib.GroupTheory.Presentation

Group.PresentationstructureMathlib.GroupTheory.Presentation, type

Wording

presentation of G and x (from the name)

English

Let $G$ and $x$ be sets. Then the presentations of $G$ and $x$ are a basic type.

Group.Presentation.ofFreeGroupHomdefMathlib.GroupTheory.Presentation, function or constant

Wording

the presentation of x2 and rel (from the name)

English

Let $x_{2}$ be a monoid homomorphism of the set of free groups of $x$ and $G$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{2}$. Let $\mathrm{rel}$ be an element of the power set of the set of free groups of $x$ such that the multiplicative kernel of $x_{2}$ is equal to the normal closure of $\mathrm{rel}$. Then the presentation of $x_{2}$ and $\mathrm{rel}$ is a presentation of $G$ and $x$.

Group.Presentation.presentedGroupEquivdefMathlib.GroupTheory.Presentation, function or constant

Wording

the presented group equivalence of P (from the name)

English

Let $P$ be a presentation of $G$ and $x$. Then the presented group equivalence of $P$ is a multiplicative equivalence of the set of presented groups of the relation of $P$ and $G$.

Group.Presentation.reldefMathlib.GroupTheory.Presentation, function or constant

Wording

the relation of self (from the name)

English

Let $\mathrm{self}$ be a presentation of $G$ and $x$. Then the relation of $\mathrm{self}$ is an element of the power set of the set of free groups of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.GroupTheory.PresentedGroup

PresentedGroupdefMathlib.GroupTheory.PresentedGroup, type

Wording

presented group of rels (from the name)

English

Let $\mathrm{rels}$ be an element of the power set of the set of free groups of $x$. Then a presented group of $\mathrm{rels}$ is an element of the function that maps $\mathrm{rels}$ to the set of quotients of the set of free groups of $x$ and the normal closure of $\mathrm{rels}$.

PresentedGroup.coprodPresentationsdefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

the coproduct presentation of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of the power set of the set of free groups of $x$. Let $x_{3}$ be an element of the power set of the set of free groups of $x_{1}$. Then the coproduct presentation of $x_{2}$ and $x_{3}$ is a multiplicative equivalence of the set of presented groups of the union of the image of $\operatorname{coe}$ applied to the map of $\operatorname{inl}$ and $x_{2}$ and the image of $\operatorname{coe}$ applied to the map of $\operatorname{inr}$ and $x_{3}$ and the set of coproducts of the set of presented groups of $x_{2}$ and the set of presented groups of $x_{3}$.

PresentedGroup.equivPresentedGroupdefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

the equivalence presented group of rels and e (from the name)

English

Let $\mathrm{rels}$ be an element of the power set of the set of free groups of $x$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the equivalence presented group of $\mathrm{rels}$ and $e$ is a multiplicative equivalence of the set of presented groups of $\mathrm{rels}$ and the set of presented groups of the image of $\operatorname{coe}$ applied to the free group congruence of $e$ and $\mathrm{rels}$.

PresentedGroup.mapdefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

the map of f and hst (from the name)

English

Let $f$ be a monoid homomorphism of the set of free groups of $x$ and the set of free groups of $x_{1}$ such that $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to $f$, $s$ and $t$. Then the map of $f$ and $\mathrm{hst}$ is a monoid homomorphism of the set of presented groups of $s$ and the set of presented groups of $t$.

PresentedGroup.mkdefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

no wording

English

Let $\mathrm{rels}$ be an element of the power set of the set of free groups of $x$. Then $\operatorname{mk}$ applied to $\mathrm{rels}$ is a monoid homomorphism of the set of free groups of $x$ and the set of presented groups of $\mathrm{rels}$.

PresentedGroup.ofdefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a presented group of $\mathrm{rels}$ defined as $\operatorname{mk}$ applied to $\mathrm{rels}$ and $\operatorname{of}$ applied to $x_{1}$.

PresentedGroup.toCoproddefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

the coproduct of x3 and x4 (from the name)

English

Let $x_{2}$ be an element of the power set of the set of free groups of $x$. Let $x_{3}$ be an element of the power set of the set of free groups of $x_{1}$. Let $x_{4}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then the coproduct of $x_{3}$ and $x_{4}$ is a coproduct of the set of presented groups of $x_{2}$ and the set of presented groups of $x_{3}$ defined as $\operatorname{elim}$ applied to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the left injection and $\operatorname{of}$, $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the right injection and $\operatorname{of}$ and $x_{4}$.

PresentedGroup.toGroupdefMathlib.GroupTheory.PresentedGroup, function or constant

Wording

the group of h (from the name)

English

Assume that for all free groups $r$ of $x$, if $r$ is an element of $\mathrm{rels}$, then $\operatorname{coe}$ applied to the lift, $f$ and $r$ is equal to $1$. Then the group of $h$ is a monoid homomorphism of the set of presented groups of $\mathrm{rels}$ and $G$ defined as the lift of the normal closure of $\mathrm{rels}$ and $\operatorname{lift}$ applied to $f$.

Mathlib.GroupTheory.PushoutI

Monoid.PushoutIdefMathlib.GroupTheory.PushoutI, type

Wording

pushout of x3 (from the name)

English

Let $x_{3}$ be a function from elements $i$ of $x$ to monoid homomorphisms of $H$ and $G$ applied to $i$. Then a pushout of $i$ is an element of the function that maps $x_{3}$ and $x_{3}$ to the set of quotients of the congruence relation of $i$.

Monoid.PushoutI.NormalWordstructureMathlib.GroupTheory.PushoutI, type

Wording

normal word of d (from the name)

English

Let $d$ be an element of $\operatorname{Transversal}$ applied to $x_{3}$. Then the normal words of $d$ are a basic type.

Monoid.PushoutI.NormalWord.PairstructureMathlib.GroupTheory.PushoutI, type

Wording

pair of d and i (from the name)

English

Let $d$ be an element of $\operatorname{Transversal}$ applied to $x_{3}$. Let $i$ be an element of $x$. Then the pairs of $d$ and $i$ are a basic type.

Monoid.PushoutI.NormalWord.TransversalstructureMathlib.GroupTheory.PushoutI, type

Wording

no wording

English

Let $x_{3}$ be a function from elements $i$ of $x$ to monoid homomorphisms of $H$ and $G$ applied to $i$. Then the elements of $\operatorname{Transversal}$ applied to $i$ and $x_{3}$ are a basic type.

Monoid.PushoutI.NormalWord.Transversal.setdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the set of self and i (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{Transversal}$ applied to $x_{3}$. Let $i$ be an element of $x$. Then the set of $\mathrm{self}$ and $i$ is an element of $\wp G (i)$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

Monoid.PushoutI.NormalWord.consdefMathlib.GroupTheory.PushoutI, function or constant

Wording

no wording

English

Let $g$ be an element of $G$ applied to $i$. Let $w$ be a normal word of $d$ such that the first component index of $\operatorname{toWord}$ applied to $w$ is distinct from $\operatorname{some}$ applied to $i$. Assume that $g$ is not an element of the range of $x_{3}$ applied to $i$. Then $\operatorname{cons}$ applied to $g$, $w$, $\mathrm{hmw}$ and $\mathrm{hgr}$ is a normal word of $d$.

Monoid.PushoutI.NormalWord.consRecOndefMathlib.GroupTheory.PushoutI, function or constant

Wording

no wording

English

Let $w$ be a normal word of $d$. Let $\mathrm{empty}$ be an element of $\mathrm{motive}$ applied to $\operatorname{empty}$. Let $\mathrm{cons}$ be a function from elements $i_{1}$ of $x$ and elements $g$ of $G$ applied to $i_{1}$ and normal words $w_{2}$ of $d$ and elements $\mathrm{hmw}$ of $\mathrm{Proof}$ applied to the proposition that the first component index of $\operatorname{toWord}$ applied to $w_{2}$ is distinct from $\operatorname{some}$ applied to $i_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that $g$ is an element of the set of $d$ and $i_{1}$ and elements $\mathrm{hgr}$ of $\mathrm{Proof}$ applied to the proposition that $g$ is not an element of the range of $x_{3}$ applied to $i_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that the head of $w_{2}$ is equal to $1$ and elements of $\mathrm{motive}$ applied to $w_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $g$, $w_{2}$, $\mathrm{hmw}$ and $\mathrm{hgr}$. Let $\mathrm{base}$ be a function from elements $h$ of $H$ and normal words $w_{1}$ of $d$ and elements of $\mathrm{Proof}$ applied to the proposition that the head of $w_{1}$ is equal to $1$ and elements of $\mathrm{motive}$ applied to $w_{1}$ to elements of $\mathrm{motive}$ applied to $\HSMulhSMulMACRoAL {\operatorname{base} (x_{3} , h)}{w_{1}}$. Then $\operatorname{consRecOn}$ applied to $w$, $\mathrm{empty}$, $i_{1}$, $g$, $w_{2}$, $\mathrm{hmw}$, $\mathrm{hgr}$, $\mathrm{cons}$, $h$, $w_{1}$ and $\mathrm{base}$ is an element of $\mathrm{motive}$ applied to $w$.

Monoid.PushoutI.NormalWord.emptydefMathlib.GroupTheory.PushoutI, function or constant

Wording

no wording

English

$\operatorname{empty}$ is a normal word of $d$.

Monoid.PushoutI.NormalWord.equivdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence from the set of pushouts of $x_{3}$ to the set of normal words of $d$.

Monoid.PushoutI.NormalWord.equivPairdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the equivalence pair of i (from the name)

English

Let $i$ be an element of $x$. Then the equivalence pair of $i$ is an equivalence from the set of normal words of $d$ to the set of pairs of $d$ and $i$.

Monoid.PushoutI.NormalWord.headdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the head of self (from the name)

English

Let $\mathrm{self}$ be a normal word of $d$. Then the head of $\mathrm{self}$ is an element of $H$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Monoid.PushoutI.NormalWord.proddefMathlib.GroupTheory.PushoutI, function or constant

Wording

the product of w (from the name)

English

Let $w$ be a normal word of $d$. Then the product of $w$ is a pushout of $x_{3}$ defined as the product of $\operatorname{base}$ applied to $x_{3}$ and the head of $w$ and $\operatorname{ofCoprodI}$ applied to the product of $\operatorname{toWord}$ applied to $w$.

Monoid.PushoutI.NormalWord.rconsdefMathlib.GroupTheory.PushoutI, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Let $p$ be a pair of $d$ and $i$. Then $\operatorname{rcons}$ applied to $i$ and $p$ is a normal word of $d$.

Monoid.PushoutI.ReduceddefMathlib.GroupTheory.PushoutI, predicate

Wording

no wording

English

Let $x_{3}$ be a function from elements $i$ of $x$ to monoid homomorphisms of $H$ and $G$ applied to $i$. Let $w$ be a word of $G$. Then $\operatorname{Reduced}$ holds for $i$, $x_{3}$ and $w$, if for all elements $g$ of $\Sigma$ applied to the function that maps $i$ to $G$ applied to $i$, if $g$ is an element of the list of $x_{3}$, then $\operatorname{snd}$ applied to $g$ is not an element of the range of $i$ applied to $\operatorname{fst}$ applied to $g$.

Monoid.PushoutI.basedefMathlib.GroupTheory.PushoutI, function or constant

Wording

the map from the base monoid into the pushout of x3 (from the docstring)

English

Let $x_{3}$ be a function from elements $i$ of $x$ to monoid homomorphisms of $H$ and $G$ applied to $i$. Then the map from the base monoid into the pushout of $i$ is a monoid homomorphism of $H$ and the set of pushouts of $x_{3}$ defined as the function that maps $x_{3}$ to the composition of $\operatorname{mk'}$ applied to the congruence relation of $i$ and the right injection.

Monoid.PushoutI.condefMathlib.GroupTheory.PushoutI, function or constant

Wording

the congruence relation of x3 (from the name)

English

Let $x_{3}$ be a function from elements $i$ of $x$ to monoid homomorphisms of $H$ and $G$ applied to $i$. Then the congruence relation of $i$ is a congruence relation of the set of coproducts of the set of coproducts of $G$ and $H$ defined as the function that maps $x_{3}$ to the congruence relation generator of the function that maps $x_{4}$ and $y$ to the proposition that there exists an element $i$ of $x$, such that there exists an element $\mathrm{x'}$ of $H$, such that $\EqtMACRoH {x_{4}}{\operatorname{inl} (\operatorname{of} (i (i , \mathrm{x'})))}$ and $\EqtMACRoH {y}{\operatorname{inr} (\mathrm{x'})}$.

Monoid.PushoutI.homEquivdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the homomorphism equivalence (from the name)

English

The homomorphism equivalence is an element of $\EquivMACRoAE {\mathrm{MonoidHom} (\operatorname{PushoutI} (x_{4}), K)}{(\SubtypeSet {f}{\mathrm{forall} (x , \lambda i . \EqtMACRoH {\operatorname{comp} (\ProdfstMACRoZ {f}, x_{4} (i))}{\ProdsndMACRoAA {f}})})}$.

Monoid.PushoutI.liftdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the lift of f and i1 (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x$ to monoid homomorphisms of $G$ applied to $i_{1}$ and $K$. Let $k$ be a monoid homomorphism of $H$ and $K$ such that for all elements $i$ of $x$, the composition of $f$ applied to $i$ and $x_{4}$ applied to $i$ is equal to $k$. Then the lift of $i_{1}$ and $f$ is a monoid homomorphism of the set of pushouts of $x_{4}$ and $K$.

Monoid.PushoutI.ofdefMathlib.GroupTheory.PushoutI, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $i$ is a monoid homomorphism of $G$ applied to $i$ and the set of pushouts of $x_{3}$ defined as the composition of $\operatorname{mk'}$ applied to the congruence relation of $x_{3}$ and the composition of the left injection and $\operatorname{of}$.

Monoid.PushoutI.ofCoprodIdefMathlib.GroupTheory.PushoutI, function or constant

Wording

the map from the coproduct into the pushout (from the docstring)

English

The map from the coproduct into the pushout is a monoid homomorphism of the set of coproducts of $G$ and the set of pushouts of $x_{3}$ defined as $\operatorname{lift}$ applied to $\operatorname{of}$.

Mathlib.GroupTheory.QuotientGroup.Basic

AddMonoidHom.domRestrictHomKerEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

no wording

English

Let $A$ be a set. Let $H$ be an additive subgroup of $G$. Then $\operatorname{domRestrictHomKerEquiv}$ applied to $A$ and $H$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{domRestrictHom} (H , A))}{x_{2}})}$ and the set of additive monoid homomorphisms of the set of quotients of $G$ and $H$ and $A$.

MonoidHom.domRestrictHomKerEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

no wording

English

Let $A$ be a set. Let $H$ be a subgroup of $G$. Then $\operatorname{domRestrictHomKerEquiv}$ applied to $A$ and $H$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{domRestrictHom} (H , A))}{x_{2}})}$ and the set of monoid homomorphisms of the set of quotients of $G$ and $H$ and $A$.

QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHomdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

no wording

English

Let $A$ be a function from elements of $x$ to sets. Let $n$ be a natural number. Then $\operatorname{addEquivPiModRangeNSMulAddMonoidHom}$ applied to $A$ and $n$ is an additive equivalence of the set of quotients of the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$ and the range of the natural multiple additive monoid homomorphism of $n$ and the set of functions from elements $i_{1}$ of $x$ to quotients of $A$ applied to $i_{1}$ and the range of the natural multiple additive monoid homomorphism of $n$.

QuotientAddGroup.comapMk'OrderIsodefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the preimage order isomorphism of N (from the name)

English

Let $N$ be an additive subgroup of $G$. Then the preimage order isomorphism of $N$ is an order isomorphism of the set of additive subgroups of the set of quotients of $G$ and $N$ and the set of elements of $\operatorname{Ici}$ applied to $N$.

QuotientAddGroup.equivQuotientAddSubgroupOfOfEqdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the equivalence quotient additive subgroup of h and #2 (from the name)

English

Assume that $\EqtMACRoH {\mathrm{A'}}{\mathrm{B'}}$. Assume that $\EqtMACRoH {A}{B}$. Then the equivalence quotient additive subgroup of $\mathrm{h'}$ and $h$ is an additive equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and the additive subgroup of $\mathrm{A'}$ and $A$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {B}{x_{2}})}$ and the additive subgroup of $\mathrm{B'}$ and $B$.

QuotientAddGroup.equivQuotientZSMulOfEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

no wording

English

Let $e$ be an additive equivalence of $A$ and $B$. Let $n$ be an integer. Then $\operatorname{equivQuotientZSMulOfEquiv}$ applied to $e$ and $n$ is an additive equivalence of the set of quotients of $A$ and the range of the integer multiple additive group homomorphism of $n$ and the set of quotients of $B$ and the range of the integer multiple additive group homomorphism of $n$.

QuotientAddGroup.homQuotientZSMulOfHomdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of $A$ and $B$. Let $n$ be an integer. Then $\operatorname{homQuotientZSMulOfHom}$ applied to $f$ and $n$ is an additive monoid homomorphism of the set of quotients of $A$ and the range of the integer multiple additive group homomorphism of $n$ and the set of quotients of $B$ and the range of the integer multiple additive group homomorphism of $n$.

QuotientAddGroup.kerLiftdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the induced map from the quotient by the kernel to the codomain of x2 (from the docstring)

English

Let $x_{2}$ be an additive monoid homomorphism of $G$ and $H$. Then the induced map from the quotient by the kernel to the codomain of $x_{2}$ is an additive monoid homomorphism of the set of quotients of $G$ and the additive kernel of $x_{2}$ and $H$.

QuotientAddGroup.prodAddEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the product additive equivalence of A and B (from the name)

English

Let $A$ be an additive subgroup of $G$. Let $B$ be an additive subgroup of $H$. Then the product additive equivalence of $A$ and $B$ is an additive equivalence of the set of quotients of $\mathrm{Prod}$ applied to $G$ and $H$ and the product of $A$ and $B$ and $\mathrm{Prod}$ applied to the set of quotients of $G$ and $A$ and the set of quotients of $H$ and $B$.

QuotientAddGroup.prodEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the product equivalence of A and B (from the name)

English

Let $A$ be an additive subgroup of $G$. Let $B$ be an additive subgroup of $H$. Then the product equivalence of $A$ and $B$ is an equivalence from the set of quotients of $\mathrm{Prod}$ applied to $G$ and $H$ and the product of $A$ and $B$ to $\mathrm{Prod}$ applied to the set of quotients of $G$ and $A$ and the set of quotients of $H$ and $B$.

QuotientAddGroup.quotientAddEquivOfEqdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient additive equivalence of h2 (from the name)

English

Assume that $\EqtMACRoH {M}{N}$. Then the quotient additive equivalence of $h_{2}$ is an additive equivalence of the set of quotients of $G$ and $M$ and the set of quotients of $G$ and $N$.

QuotientAddGroup.quotientBotdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient bottom (from the name)

English

The quotient bottom is an additive equivalence of the set of quotients of $G$ and the bottom and $G$.

QuotientAddGroup.quotientInfEquivSumNormalQuotientdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient infimum equivalence sum normal quotient of H and N (from the name)

English

Let $H$ and $N$ be additive subgroups of $G$. Then the quotient infimum equivalence sum normal quotient of $H$ and $N$ is an additive equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the additive subgroup of $N$ and $H$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {H}{N})}{x_{2}})}$ and the additive subgroup of $N$ and $\MaxmaxMACRoAF {H}{N}$ defined as the quotient infimum equivalence sum normalizer quotient of $H$ and $N$.

QuotientAddGroup.quotientInfEquivSumNormalizerQuotientdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient infimum equivalence sum normalizer quotient of H and N (from the name)

English

Let $H$ and $N$ be additive subgroups of $G$ such that $H$ is less than or equal to the normalizer of $N$. Then the quotient infimum equivalence sum normalizer quotient of $H$ and $N$ is an additive equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the additive subgroup of $N$ and $H$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {H}{N})}{x_{2}})}$ and the additive subgroup of $N$ and $\MaxmaxMACRoAF {H}{N}$.

QuotientAddGroup.quotientKerEquivOfRightInversedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient kernel equivalence of x2 and x3 (from the name)

English

Let $x_{2}$ be an additive monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a function from elements of $H$ to elements of $G$ such that $\operatorname{RightInverse}$ holds for $x_{3}$ and $\operatorname{coe}$ applied to $x_{2}$. Then the quotient kernel equivalence of $x_{2}$ and $x_{3}$ is an additive equivalence of the set of quotients of $G$ and the additive kernel of $x_{2}$ and $H$.

QuotientAddGroup.quotientKerEquivOfSurjectivedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient kernel equivalence of x2 and h (from the name)

English

Let $x_{2}$ be an additive monoid homomorphism of $G$ and $H$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{2}$. Then the quotient kernel equivalence of $x_{2}$ and $h$ is an additive equivalence of the set of quotients of $G$ and the additive kernel of $x_{2}$ and $H$.

QuotientAddGroup.quotientKerEquivRangedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient kernel equivalence range of x2 (from the name)

English

Let $x_{2}$ be an additive monoid homomorphism of $G$ and $H$. Then the quotient kernel equivalence range of $x_{2}$ is an additive equivalence of the set of quotients of $G$ and the additive kernel of $x_{2}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{range} (x_{2})}{x_{3}})}$.

QuotientAddGroup.quotientMapAddSubgroupOfOfLedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient map additive subgroup of h and #2 (from the name)

English

Assume that $\mathrm{A'} \leq \mathrm{B'}$. Assume that $A \leq B$. Then the quotient map additive subgroup of $\mathrm{h'}$ and $h$ is an additive monoid homomorphism of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and the additive subgroup of $\mathrm{A'}$ and $A$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {B}{x_{2}})}$ and the additive subgroup of $\mathrm{B'}$ and $B$.

QuotientAddGroup.quotientQuotientEquivQuotientdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient quotient equivalence quotient of N and M (from the name)

English

Let $N$ and $M$ be additive subgroups of $G$ such that $N \leq M$. Then the quotient quotient equivalence quotient of $N$ and $M$ is an additive equivalence of the set of quotients of the set of quotients of $G$ and $N$ and the map of $\operatorname{mk'}$ applied to $N$ and $M$ and the set of quotients of $G$ and $M$.

QuotientAddGroup.rangeKerLiftdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the induced map from the quotient by the kernel to the range of x2 (from the docstring)

English

Let $x_{2}$ be an additive monoid homomorphism of $G$ and $H$. Then the induced map from the quotient by the kernel to the range of $x_{2}$ is an additive monoid homomorphism of the set of quotients of $G$ and the additive kernel of $x_{2}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{range} (x_{2})}{x_{3}})}$.

QuotientGroup.comapMk'OrderIsodefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the preimage order isomorphism of N (from the name)

English

Let $N$ be a subgroup of $G$. Then the preimage order isomorphism of $N$ is an order isomorphism of the set of subgroups of the set of quotients of $G$ and $N$ and the set of elements of $\operatorname{Ici}$ applied to $N$.

QuotientGroup.equivQuotientSubgroupOfOfEqdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the equivalence quotient subgroup of h and #2 (from the name)

English

Assume that $\EqtMACRoH {\mathrm{A'}}{\mathrm{B'}}$. Assume that $\EqtMACRoH {A}{B}$. Then the equivalence quotient subgroup of $\mathrm{h'}$ and $h$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and the subgroup of $\mathrm{A'}$ and $A$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {B}{x_{2}})}$ and the subgroup of $\mathrm{B'}$ and $B$.

QuotientGroup.equivQuotientZPowOfEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the equivalence quotient power of e and n (from the name)

English

Let $e$ be a multiplicative equivalence of $A$ and $B$. Let $n$ be an integer. Then the equivalence quotient power of $e$ and $n$ is a multiplicative equivalence of the set of quotients of $A$ and the range of the integer power group homomorphism of $n$ and the set of quotients of $B$ and the range of the integer power group homomorphism of $n$.

QuotientGroup.homQuotientZPowOfHomdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the homomorphism quotient power of f and n (from the name)

English

Let $f$ be a monoid homomorphism of $A$ and $B$. Let $n$ be an integer. Then the homomorphism quotient power of $f$ and $n$ is a monoid homomorphism of the set of quotients of $A$ and the range of the integer power group homomorphism of $n$ and the set of quotients of $B$ and the range of the integer power group homomorphism of $n$.

QuotientGroup.kerLiftdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the induced map from the quotient by the kernel to the codomain of x2 (from the docstring)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and $H$. Then the induced map from the quotient by the kernel to the codomain of $x_{2}$ is a monoid homomorphism of the set of quotients of $G$ and the multiplicative kernel of $x_{2}$ and $H$.

QuotientGroup.mulEquivPiModRangePowMonoidHomdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

no wording

English

Let $A$ be a function from elements of $x$ to sets. Let $n$ be a natural number. Then $\operatorname{mulEquivPiModRangePowMonoidHom}$ applied to $A$ and $n$ is a multiplicative equivalence of the set of quotients of the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$ and the range of the power monoid homomorphism of $n$ and the set of functions from elements $i_{1}$ of $x$ to quotients of $A$ applied to $i_{1}$ and the range of the power monoid homomorphism of $n$.

QuotientGroup.prodEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the product equivalence of A and B (from the name)

English

Let $A$ be a subgroup of $G$. Let $B$ be a subgroup of $H$. Then the product equivalence of $A$ and $B$ is an equivalence from the set of quotients of $\mathrm{Prod}$ applied to $G$ and $H$ and the product of $A$ and $B$ to $\mathrm{Prod}$ applied to the set of quotients of $G$ and $A$ and the set of quotients of $H$ and $B$.

QuotientGroup.prodMulEquivdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the product multiplicative equivalence of A and B (from the name)

English

Let $A$ be a subgroup of $G$. Let $B$ be a subgroup of $H$. Then the product multiplicative equivalence of $A$ and $B$ is a multiplicative equivalence of the set of quotients of $\mathrm{Prod}$ applied to $G$ and $H$ and the product of $A$ and $B$ and $\mathrm{Prod}$ applied to the set of quotients of $G$ and $A$ and the set of quotients of $H$ and $B$.

QuotientGroup.quotientBotdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient bottom (from the name)

English

The quotient bottom is a multiplicative equivalence of the set of quotients of $G$ and the bottom and $G$.

QuotientGroup.quotientInfEquivProdNormalQuotientdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient infimum equivalence product normal quotient of H and N (from the name)

English

Let $H$ and $N$ be subgroups of $G$. Then the quotient infimum equivalence product normal quotient of $H$ and $N$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the subgroup of $N$ and $H$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {H}{N})}{x_{2}})}$ and the subgroup of $N$ and $\MaxmaxMACRoAF {H}{N}$ defined as the quotient infimum equivalence product normalizer quotient of $H$ and $N$.

QuotientGroup.quotientInfEquivProdNormalizerQuotientdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient infimum equivalence product normalizer quotient of H and N (from the name)

English

Let $H$ and $N$ be subgroups of $G$ such that $H$ is less than or equal to the normalizer of $N$. Then the quotient infimum equivalence product normalizer quotient of $H$ and $N$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the subgroup of $N$ and $H$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {H}{N})}{x_{2}})}$ and the subgroup of $N$ and $\MaxmaxMACRoAF {H}{N}$.

QuotientGroup.quotientKerEquivOfRightInversedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient kernel equivalence of x2 and x3 (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a function from elements of $H$ to elements of $G$ such that $\operatorname{RightInverse}$ holds for $x_{3}$ and $\operatorname{coe}$ applied to $x_{2}$. Then the quotient kernel equivalence of $x_{2}$ and $x_{3}$ is a multiplicative equivalence of the set of quotients of $G$ and the multiplicative kernel of $x_{2}$ and $H$.

QuotientGroup.quotientKerEquivOfSurjectivedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient kernel equivalence of x2 and h (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and $H$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{2}$. Then the quotient kernel equivalence of $x_{2}$ and $h$ is a multiplicative equivalence of the set of quotients of $G$ and the multiplicative kernel of $x_{2}$ and $H$.

QuotientGroup.quotientKerEquivRangedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient kernel equivalence range of x2 (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and $H$. Then the quotient kernel equivalence range of $x_{2}$ is a multiplicative equivalence of the set of quotients of $G$ and the multiplicative kernel of $x_{2}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{range} (x_{2})}{x_{3}})}$.

QuotientGroup.quotientMapSubgroupOfOfLedefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient map subgroup of h and #2 (from the name)

English

Assume that $\mathrm{A'} \leq \mathrm{B'}$. Assume that $A \leq B$. Then the quotient map subgroup of $\mathrm{h'}$ and $h$ is a monoid homomorphism of the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {A}{x_{1}})}$ and the subgroup of $\mathrm{A'}$ and $A$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {B}{x_{2}})}$ and the subgroup of $\mathrm{B'}$ and $B$.

QuotientGroup.quotientMulEquivOfEqdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient multiplicative equivalence of h2 (from the name)

English

Assume that $\EqtMACRoH {M}{N}$. Then the quotient multiplicative equivalence of $h_{2}$ is a multiplicative equivalence of the set of quotients of $G$ and $M$ and the set of quotients of $G$ and $N$.

QuotientGroup.quotientQuotientEquivQuotientdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the quotient quotient equivalence quotient of N and M (from the name)

English

Let $N$ and $M$ be subgroups of $G$ such that $N \leq M$. Then the quotient quotient equivalence quotient of $N$ and $M$ is a multiplicative equivalence of the set of quotients of the set of quotients of $G$ and $N$ and the map of $\operatorname{mk'}$ applied to $N$ and $M$ and the set of quotients of $G$ and $M$.

QuotientGroup.rangeKerLiftdefMathlib.GroupTheory.QuotientGroup.Basic, function or constant

Wording

the induced map from the quotient by the kernel to the range of x2 (from the docstring)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and $H$. Then the induced map from the quotient by the kernel to the range of $x_{2}$ is a monoid homomorphism of the set of quotients of $G$ and the multiplicative kernel of $x_{2}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{range} (x_{2})}{x_{3}})}$.

Mathlib.GroupTheory.QuotientGroup.Defs

AddCon.addSubgroupdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the additive subgroup of c (from the name)

English

Let $c$ be an additive congruence relation of $G$. Then the additive subgroup of $c$ is an additive subgroup of $G$.

AddSubgroup.orderIsoAddCondefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the order isomorphism additive congruence relation (from the name)

English

The order isomorphism additive congruence relation is an order isomorphism of $\SubtypeSet {N}{\operatorname{Normal} (N)}$ and the set of additive congruence relations of $G$.

Con.subgroupdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the subgroup defined by the class of c (from the docstring)

English

Let $c$ be a congruence relation of $G$. Then the subgroup defined by the class of $c$ is a subgroup of $G$.

QuotientAddGroup.condefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the additive congruence relation generated by a normal additive subgroup of N (from the docstring)

English

Let $N$ be an additive subgroup of $G$. Then the additive congruence relation generated by a normal additive subgroup of $N$ is an additive congruence relation of $G$.

QuotientAddGroup.congrdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the congruence of he and #3 (from the name)

English

Let $\mathrm{G'}$ be an additive subgroup of $G$. Let $\mathrm{H'}$ be an additive subgroup of $H$. Let $e$ be an additive equivalence of $G$ and $H$ such that the map of the additive monoid homomorphism of $e$ and $\mathrm{G'}$ is equal to $\mathrm{H'}$. Then the congruence of $\mathrm{H'}$ and $e$ is an additive equivalence of the set of quotients of $G$ and $\mathrm{G'}$ and the set of quotients of $H$ and $\mathrm{H'}$.

QuotientAddGroup.liftdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the lift of N and x2 (from the name)

English

Let $N$ be an additive subgroup of $G$. Let $x_{2}$ be an additive monoid homomorphism of $G$ and $M$ such that $N$ is less than or equal to the additive kernel of $x_{2}$. Then the lift of $N$ and $x_{2}$ is an additive monoid homomorphism of the set of quotients of $G$ and $N$ and $M$.

QuotientAddGroup.liftEquivdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the lift equivalence of N (from the name)

English

Let $N$ be an additive subgroup of $G$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{2}$. Assume that $N$ is equal to the additive kernel of $x_{2}$. Then the lift equivalence of $N$ is an additive equivalence of the set of quotients of $G$ and $N$ and $H$.

QuotientAddGroup.mapdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the map of M and f (from the name)

English

Let $N$ be an additive subgroup of $G$. Let $M$ be an additive subgroup of $H$. Let $f$ be an additive monoid homomorphism of $G$ and $H$ such that $N$ is less than or equal to the preimage of $f$ and $M$. Then the map of $M$ and $f$ is an additive monoid homomorphism of the set of quotients of $G$ and $N$ and the set of quotients of $H$ and $M$.

QuotientAddGroup.mk'defMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

no wording

English

Let $N$ be an additive subgroup of $G$. Then $\operatorname{mk'}$ applied to $N$ is an additive monoid homomorphism of $G$ and the set of quotients of $G$ and $N$.

QuotientGroup.condefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the congruence relation generated by a normal subgroup of N (from the docstring)

English

Let $N$ be a subgroup of $G$. Then the congruence relation generated by a normal subgroup of $N$ is a congruence relation of $G$.

QuotientGroup.congrdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the congruence of he and #3 (from the name)

English

Let $\mathrm{G'}$ be a subgroup of $G$. Let $\mathrm{H'}$ be a subgroup of $H$. Let $e$ be a multiplicative equivalence of $G$ and $H$ such that the map of the monoid homomorphism of $e$ and $\mathrm{G'}$ is equal to $\mathrm{H'}$. Then the congruence of $\mathrm{H'}$ and $e$ is a multiplicative equivalence of the set of quotients of $G$ and $\mathrm{G'}$ and the set of quotients of $H$ and $\mathrm{H'}$.

QuotientGroup.liftdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the lift of N and x2 (from the name)

English

Let $N$ be a subgroup of $G$. Let $x_{2}$ be a monoid homomorphism of $G$ and $M$ such that $N$ is less than or equal to the multiplicative kernel of $x_{2}$. Then the lift of $N$ and $x_{2}$ is a monoid homomorphism of the set of quotients of $G$ and $N$ and $M$.

QuotientGroup.liftEquivdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the lift equivalence of N (from the name)

English

Let $N$ be a subgroup of $G$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{2}$. Assume that $N$ is equal to the multiplicative kernel of $x_{2}$. Then the lift equivalence of $N$ is a multiplicative equivalence of the set of quotients of $G$ and $N$ and $H$.

QuotientGroup.mapdefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the map of M and f (from the name)

English

Let $N$ be a subgroup of $G$. Let $M$ be a subgroup of $H$. Let $f$ be a monoid homomorphism of $G$ and $H$ such that $N$ is less than or equal to the preimage of $f$ and $M$. Then the map of $M$ and $f$ is a monoid homomorphism of the set of quotients of $G$ and $N$ and the set of quotients of $H$ and $M$.

QuotientGroup.mk'defMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

no wording

English

Let $N$ be a subgroup of $G$. Then $\operatorname{mk'}$ applied to $N$ is a monoid homomorphism of $G$ and the set of quotients of $G$ and $N$.

Subgroup.orderIsoCondefMathlib.GroupTheory.QuotientGroup.Defs, function or constant

Wording

the order isomorphism congruence relation (from the name)

English

The order isomorphism congruence relation is an order isomorphism of $\SubtypeSet {N}{\operatorname{Normal} (N)}$ and the set of congruence relations of $G$.

Mathlib.GroupTheory.Rank

AddGroup.rankdefMathlib.GroupTheory.Rank, function or constant

Wording

the rank of G (from the name)

English

Let $G$ be a set. Then the rank of $G$ is a natural number.

Group.rankdefMathlib.GroupTheory.Rank, function or constant

Wording

the rank of G (from the name)

English

Let $G$ be a set. Then the rank of $G$ is a natural number.

Mathlib.GroupTheory.RegularWreathProduct

IteratedWreathProductdefMathlib.GroupTheory.RegularWreathProduct, type

Wording

iterated wreath product of G and n (from the name)

English

Let $G$ be a set. Let $n$ be a natural number. Then an iterated wreath product of $G$ and $n$ is an element of the function that maps $G$ and $n$ to $\operatorname{brecOn}$ applied to $n$ and $\mathrm{IteratedWreathProduct\_\_\_f}$ applied to $G$.

RegularWreathProductstructureMathlib.GroupTheory.RegularWreathProduct, type

Wording

regular wreath product of D and Q (from the name)

English

Let $D$ and $Q$ be sets. Then the regular wreath products of $D$ and $Q$ are a basic type.

RegularWreathProduct.congrdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the congruence of f and g (from the name)

English

Let $f$ be a multiplicative equivalence of $x$ and $x_{2}$. Let $g$ be a multiplicative equivalence of $x_{1}$ and $x_{3}$. Then the congruence of $f$ and $g$ is a multiplicative equivalence of the set of regular wreath products of $x$ and $x_{1}$ and the set of regular wreath products of $x_{2}$ and $x_{3}$.

RegularWreathProduct.equivProddefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the equivalence map for the representation of D and Q (from the docstring)

English

Let $D$ and $Q$ be sets. Then the equivalence map for the representation of $D$ and $Q$ is an equivalence from the set of regular wreath products of $D$ and $Q$ to $\mathrm{Prod}$ applied to the set of functions from elements of $Q$ to elements of $D$ and $Q$.

RegularWreathProduct.inldefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the left injection (from the name)

English

The left injection is a monoid homomorphism of $Q$ and the set of regular wreath products of $D$ and $Q$.

RegularWreathProduct.leftdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the left of self and x (from the name)

English

Let $\mathrm{self}$ be a regular wreath product of $D$ and $Q$. Let $x$ be an element of $Q$. Then the left of $\mathrm{self}$ and $x$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

RegularWreathProduct.rightdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the right of self (from the name)

English

Let $\mathrm{self}$ be a regular wreath product of $D$ and $Q$. Then the right of $\mathrm{self}$ is an element of $Q$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

RegularWreathProduct.rightHomdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the right homomorphism (from the name)

English

The right homomorphism is a monoid homomorphism of the set of regular wreath products of $D$ and $Q$ and $Q$.

RegularWreathProduct.toPermdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the permutation of Q and x2 (from the name)

English

Let $D$, $Q$ and $x_{2}$ be sets. Then the permutation of $Q$ and $x_{2}$ is a monoid homomorphism of the set of regular wreath products of $D$ and $Q$ and the set of permutations of $\mathrm{Prod}$ applied to $x_{2}$ and $Q$ defined as the permutation homomorphism of the set of regular wreath products of $D$ and $Q$ and $\mathrm{Prod}$ applied to $x_{2}$ and $Q$.

Sylow.mulEquivIteratedWreathProductdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the multiplicative equivalence iterated wreath product of n and P (from the name)

English

Let $p$ and $n$ be natural numbers. Let $x$ and $G$ be sets such that the cardinality of $x$ is equal to $p ^ {n}$ and the cardinality of $G$ is equal to $p$. Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and the set of permutations of $x$. Then the multiplicative equivalence iterated wreath product of $n$ and $P$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (P)}{x_{2}})}$ and the set of iterated wreath products of $G$ and $n$.

iteratedWreathToPermHomdefMathlib.GroupTheory.RegularWreathProduct, function or constant

Wording

the iterated wreath to permutation homomorphism of G and n (from the name)

English

Let $G$ be a set. Let $n$ be a natural number. Then the iterated wreath to permutation homomorphism of $G$ and $n$ is a monoid homomorphism of the set of iterated wreath products of $G$ and $n$ and the set of permutations of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{iteratedWreathToPermHom\_\_\_f}$ applied to $G$.

Mathlib.GroupTheory.ResiduallyFinite

AddGroup.ResiduallyFiniteclassMathlib.GroupTheory.ResiduallyFinite, predicate

Wording

G is residually finite (from the name)

English

generation took over the time limit

Group.ResiduallyFiniteclassMathlib.GroupTheory.ResiduallyFinite, predicate

Wording

G is residually finite (from the name)

English

generation took over the time limit

Mathlib.GroupTheory.Schreier

Subgroup.cardCommutatorBounddefMathlib.GroupTheory.Schreier, function or constant

Wording

the cardinality commutator bound of n (from the name)

English

Let $n$ be a natural number. Then the cardinality commutator bound of $n$ is a natural number defined as $(n ^ {2 \times n})^ {(n ^ {(2 \times n + 1)}+ 1)}$.

Mathlib.GroupTheory.SchurZassenhaus

Subgroup.QuotientDiffdefMathlib.GroupTheory.SchurZassenhaus, type

Wording

quotient difference of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the quotient differences of $H$ are a basic type.

Mathlib.GroupTheory.SemidirectProduct

SemidirectProductstructureMathlib.GroupTheory.SemidirectProduct, type

Wording

semidirect product of G and x2 (from the name)

English

Let $N$ and $G$ be sets. Let $x_{2}$ be a monoid homomorphism of $G$ and the set of multiplicative automorphisms of $N$. Then the semidirect products of $G$ and $x_{2}$ are a basic type.

SemidirectProduct.congrdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the congruence of fn and fg (from the name)

English

Let $\mathrm{fn}$ be a multiplicative equivalence of $x$ and $x_{2}$. Let $\mathrm{fg}$ be a multiplicative equivalence of $x_{1}$ and $x_{3}$ such that for all elements $g$ of $x_{1}$, the composition of $x_{8}$ applied to $g$ and $\mathrm{fn}$ is equal to the composition of $\mathrm{fn}$ and $x_{9}$ applied to $\mathrm{fg}$ applied to $g$. Then the congruence of $\mathrm{fn}$ and $\mathrm{fg}$ is a multiplicative equivalence of the set of semidirect products of $x_{1}$ and $x_{8}$ and the set of semidirect products of $x_{3}$ and $x_{9}$.

SemidirectProduct.congr'defMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the congruence of fn and fg (from the name)

English

Let $\mathrm{fn}$ be a multiplicative equivalence of $x$ and $x_{2}$. Let $\mathrm{fg}$ be a multiplicative equivalence of $x_{1}$ and $x_{3}$. Then the congruence of $\mathrm{fn}$ and $\mathrm{fg}$ is a multiplicative equivalence of the set of semidirect products of $x_{1}$ and $x_{8}$ and the set of semidirect products of $x_{3}$ and the composition of the monoid homomorphism of the congruence of $\mathrm{fn}$ and the composition of $x_{8}$ and the monoid homomorphism of the inverse of $\mathrm{fg}$.

SemidirectProduct.equivProddefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the bijection between the semidirect product and the product (from the docstring)

English

The bijection between the semidirect product and the product is an equivalence from the set of semidirect products of $G$ and $x_{2}$ to $\mathrm{Prod}$ applied to $N$ and $G$.

SemidirectProduct.inldefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the left injection (from the name)

English

The left injection is a monoid homomorphism of $N$ and the set of semidirect products of $G$ and $x_{2}$.

SemidirectProduct.inrdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the right injection (from the name)

English

The right injection is a monoid homomorphism of $G$ and the set of semidirect products of $G$ and $x_{2}$.

SemidirectProduct.leftdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the left of self (from the name)

English

Let $\mathrm{self}$ be a semidirect product of $G$ and $x_{2}$. Then the left of $\mathrm{self}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

SemidirectProduct.liftdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the lift of fn and fg (from the name)

English

Let $\mathrm{fn}$ be a monoid homomorphism of $N$ and $H$. Let $\mathrm{fg}$ be a monoid homomorphism of $G$ and $H$ such that for all elements $g$ of $G$, the composition of $\mathrm{fn}$ and the monoid homomorphism of $x_{3}$ applied to $g$ is equal to the composition of the monoid homomorphism of $\operatorname{conj}$ applied to $\mathrm{fg}$ applied to $g$ and $\mathrm{fn}$. Then the lift of $\mathrm{fn}$ and $\mathrm{fg}$ is a monoid homomorphism of the set of semidirect products of $G$ and $x_{3}$ and $H$.

SemidirectProduct.mapdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the map of fn and fg (from the name)

English

Let $\mathrm{fn}$ be a monoid homomorphism of $x$ and $x_{2}$. Let $\mathrm{fg}$ be a monoid homomorphism of $x_{1}$ and $x_{3}$ such that for all elements $g$ of $x_{1}$, the composition of $\mathrm{fn}$ and the monoid homomorphism of $x_{8}$ applied to $g$ is equal to the composition of the monoid homomorphism of $x_{9}$ applied to $\mathrm{fg}$ applied to $g$ and $\mathrm{fn}$. Then the map of $\mathrm{fn}$ and $\mathrm{fg}$ is a monoid homomorphism of the set of semidirect products of $x_{1}$ and $x_{8}$ and the set of semidirect products of $x_{3}$ and $x_{9}$.

SemidirectProduct.monoidHomSubgroupdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the monoid homomorphism subgroup of h (from the name)

English

Assume that $K$ is less than or equal to the normalizer of $H$. Then the monoid homomorphism subgroup of $h$ is a monoid homomorphism of the set of semidirect products of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {K}{x_{2}})}$ and the composition of the homomorphism of $H$ and the inclusion homomorphism of $h$ and $G$.

SemidirectProduct.mulEquivProddefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the multiplicative equivalence product (from the name)

English

The multiplicative equivalence product is a multiplicative equivalence of the set of semidirect products of $G$ and $1$ and $\mathrm{Prod}$ applied to $N$ and $G$.

SemidirectProduct.mulEquivSubgroupdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the multiplicative equivalence subgroup of h1 (from the name)

English

Assume that $\operatorname{IsComplement'}$ holds for $H$ and $K$. Then the multiplicative equivalence subgroup of $h_{1}$ is a multiplicative equivalence of the set of semidirect products of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {K}{x_{2}})}$ and the composition of the homomorphism of $H$ and the inclusion homomorphism of $\operatorname{rec}$ applied to $\mathrm{le\_top}$ and $\operatorname{symm}$ applied to $\mathrm{Subgroup\_\_normalizer\_eq\_top}$ applied to $H$ and $G$.

SemidirectProduct.rightdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the right of self (from the name)

English

Let $\mathrm{self}$ be a semidirect product of $G$ and $x_{2}$. Then the right of $\mathrm{self}$ is an element of $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

SemidirectProduct.rightHomdefMathlib.GroupTheory.SemidirectProduct, function or constant

Wording

the right homomorphism (from the name)

English

The right homomorphism is a monoid homomorphism of the set of semidirect products of $G$ and $x_{2}$ and $G$.

Mathlib.GroupTheory.Solvable

AddGroup.IsSolvableclassMathlib.GroupTheory.Solvable, predicate

Wording

G is solvable (from the name)

English

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

AddSubgroup.derivedSeriesdefMathlib.GroupTheory.Solvable, function or constant

Wording

the derived series of G and x1 (from the name)

English

Let $G$ be a set. Let $x_{1}$ be a natural number. Then the derived series of $G$ and $x_{1}$ is an additive subgroup of $G$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{AddSubgroup\_\_derivedSeries\_\_\_f}$ applied to $G$.

Group.IsSolvableclassMathlib.GroupTheory.Solvable, predicate

Wording

G is solvable (from the name)

English

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

Subgroup.derivedSeriesdefMathlib.GroupTheory.Solvable, function or constant

Wording

the derived series of G and x1 (from the name)

English

Let $G$ be a set. Let $x_{1}$ be a natural number. Then the derived series of $G$ and $x_{1}$ is a subgroup of $G$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Subgroup\_\_derivedSeries\_\_\_f}$ applied to $G$.

Mathlib.GroupTheory.SpecificGroups.Alternating

Equiv.altCongrHomdefMathlib.GroupTheory.SpecificGroups.Alternating, function or constant

Wording

no wording

English

Let $e$ be an element of $\EquivMACRoAE {x}{x_{3}}$. Then $\operatorname{altCongrHom}$ applied to $e$ is a multiplicative equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (x)}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (x_{3})}{x_{7}})}$.

alternatingGroupdefMathlib.GroupTheory.SpecificGroups.Alternating, function or constant

Wording

the alternating group of x (from the name)

English

Let $x$ be a set. Then the alternating group of $x$ is a subgroup of the set of permutations of $x$ defined as the multiplicative kernel of the sign.

alternatingGroup.ofSubtypedefMathlib.GroupTheory.SpecificGroups.Alternating, function or constant

Wording

the alternating group of s (from the name)

English

Let $s$ be a finite set of $x$. Then the alternating group of $s$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})})}{x_{3}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (x)}{x_{5}})}$.

Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

alternatingGroup.kleinFourdefMathlib.GroupTheory.SpecificGroups.Alternating.KleinFour, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{kleinFour}$ applied to $x$ is a subgroup of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (x)}{x_{3}})}$ defined as the closure of $\operatorname{ofPred}$ applied to the function that maps $g$ to $\EqtMACRoH {\operatorname{cycleType} (g)}{\operatorname{insert} (2 , \operatorname{singleton} (2))}$.

Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Equiv.Perm.iwasawaStructure_twodefMathlib.GroupTheory.SpecificGroups.Alternating.Simple, function or constant

Wording

no wording

English

$\mathrm{Equiv\_\_Perm\_\_iwasawaStructure\_two}$ is an element of $\operatorname{IwasawaStructure}$ applied to the set of permutations of $x$ and the set of elements of the powerset cardinality of $x$ and $2$.

alternatingGroup.iwasawaStructure_fourdefMathlib.GroupTheory.SpecificGroups.Alternating.Simple, function or constant

Wording

the Iwasawa structure of h5 (from the docstring)

English

Assume that $5 \leq \operatorname{card} (x)$. Then the Iwasawa structure of $h_{5}$ is an element of $\operatorname{IwasawaStructure}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (x)}{x_{3}})}$ and the set of elements of the powerset cardinality of $x$ and $4$.

alternatingGroup.iwasawaStructure_threedefMathlib.GroupTheory.SpecificGroups.Alternating.Simple, function or constant

Wording

no wording

English

$\mathrm{alternatingGroup\_\_iwasawaStructure\_three}$ is an element of $\operatorname{IwasawaStructure}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{alternatingGroup} (x)}{x_{3}})}$ and the set of elements of the powerset cardinality of $x$ and $3$.

Mathlib.GroupTheory.SpecificGroups.Cyclic

IsCyclic.mulAutMulEquivdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the automorphism group of G (from the docstring)

English

Let $G$ be a set. Then the automorphism group of $G$ is a multiplicative equivalence of the set of multiplicative automorphisms of $G$ and the set of units of $\mathrm{ZMod}$ applied to the cardinality of $G$ defined as the composition of the composition of the inverse of the congruence of the integer modulo cyclic multiplicative equivalence of $h$ and the multiplicative automorphism multiplicative of $\mathrm{ZMod}$ applied to the cardinality of $G$ and $\operatorname{toMultiplicative}$ applied to the automorphism group of the cardinality of $G$.

addEquivOfAddCyclicCardEqdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the additive equivalence of hcard (from the name)

English

Assume that the cardinality of $G$ is equal to the cardinality of $\mathrm{G'}$. Then the additive equivalence of $\mathrm{hcard}$ is an additive equivalence of $G$ and $\mathrm{G'}$.

addEquivOfAddOrderOfEqdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the additive equivalence of h and #3 (from the name)

English

Assume that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zmultiples} (g)}{x_{3}}$. Assume that for all elements $x_{2}$ of $\mathrm{G'}$, $\MembershipmemMACRoT {\operatorname{zmultiples} (\mathrm{g'})}{x_{2}}$. Assume that the additive order of $g$ is equal to the additive order of $\mathrm{g'}$. Then the additive equivalence of $\mathrm{hg'}$ and $h$ is an additive equivalence of $G$ and $\mathrm{G'}$.

addEquivOfPrimeCardEqdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the additive equivalence of hG and hH (from the name)

English

Assume that the cardinality of $G$ is equal to $p$. Assume that the cardinality of $\mathrm{G'}$ is equal to $p$. Then the additive equivalence of $\mathrm{hG}$ and $\mathrm{hH}$ is an additive equivalence of $G$ and $\mathrm{G'}$.

addMonoidHomOfForallMemZMultiplesdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the additive monoid homomorphism of hg and #2 (from the name)

English

Assume that for all elements $x_{2}$ of $G$, $\MembershipmemMACRoT {\operatorname{zmultiples} (g)}{x_{2}}$. Assume that the additive order of $\mathrm{g'}$ divides the additive order of $g$. Then the additive monoid homomorphism of $\mathrm{hg}$ and $\mathrm{hg'}$ is an additive monoid homomorphism of $G$ and $\mathrm{G'}$.

intCyclicAddEquivdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer cyclic additive equivalence (from the name)

English

The integer cyclic additive equivalence is an additive equivalence of $\Integer$ and $G$.

intCyclicMulEquivdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer cyclic multiplicative equivalence (from the name)

English

The integer cyclic multiplicative equivalence is a multiplicative equivalence of the set of multiplicatives of $\Integer$ and $G$.

intEquivOfZMultiplesEqTopdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer equivalence of g and hg (from the name)

English

Let $g$ be an element of $G$ such that $\operatorname{zmultiples}$ applied to $g$ is equal to the top. Then the integer equivalence of $g$ and $\mathrm{hg}$ is an additive equivalence of $\Integer$ and $G$ defined as the additive equivalence of $\operatorname{zmultiplesHom}$ applied to $G$ and $g$ and $\mathrm{zmultiplesHom\_bijective}$ applied to $\mathrm{hg}$.

intEquivOfZPowersEqTopdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer equivalence of g and hg (from the name)

English

Let $g$ be an element of $G$ such that $\operatorname{zpowers}$ applied to $g$ is equal to the top. Then the integer equivalence of $g$ and $\mathrm{hg}$ is a multiplicative equivalence of the set of multiplicatives of $\Integer$ and $G$ defined as the multiplicative equivalence of $\operatorname{zpowersHom}$ applied to $G$ and $g$ and $\mathrm{zpowersHom\_bijective}$ applied to $\mathrm{hg}$.

monoidHomOfForallMemZpowersdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the monoid homomorphism of hg and #2 (from the name)

English

Assume that for all elements $x_{2}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{2}}$. Assume that the order of $\mathrm{g'}$ divides the order of $g$. Then the monoid homomorphism of $\mathrm{hg}$ and $\mathrm{hg'}$ is a monoid homomorphism of $G$ and $\mathrm{G'}$.

mulEquivOfCyclicCardEqdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the multiplicative equivalence of hcard (from the name)

English

Assume that the cardinality of $G$ is equal to the cardinality of $\mathrm{G'}$. Then the multiplicative equivalence of $\mathrm{hcard}$ is a multiplicative equivalence of $G$ and $\mathrm{G'}$.

mulEquivOfOrderOfEqdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the multiplicative equivalence of h and #3 (from the name)

English

Assume that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Assume that for all elements $x_{2}$ of $\mathrm{G'}$, $\MembershipmemMACRoT {\operatorname{zpowers} (\mathrm{g'})}{x_{2}}$. Assume that the order of $g$ is equal to the order of $\mathrm{g'}$. Then the multiplicative equivalence of $\mathrm{hg'}$ and $h$ is a multiplicative equivalence of $G$ and $\mathrm{G'}$.

mulEquivOfPrimeCardEqdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the multiplicative equivalence of hG and hH (from the name)

English

Assume that the cardinality of $G$ is equal to $p$. Assume that the cardinality of $\mathrm{G'}$ is equal to $p$. Then the multiplicative equivalence of $\mathrm{hG}$ and $\mathrm{hH}$ is a multiplicative equivalence of $G$ and $\mathrm{G'}$.

zmodAddCyclicAddEquivdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer modulo additive cyclic additive equivalence of h (from the name)

English

Assume that $G$ is cyclic. Then the integer modulo additive cyclic additive equivalence of $h$ is an additive equivalence of $\mathrm{ZMod}$ applied to the cardinality of $G$ and $G$.

zmodAddEquivOfGeneratordefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer modulo additive equivalence of hg and hn (from the name)

English

Assume that for all elements $x_{1}$ of $G$, $\MembershipmemMACRoT {\operatorname{zmultiples} (g)}{x_{1}}$. Assume that the cardinality of $G$ is equal to $n$. Then the integer modulo additive equivalence of $\mathrm{hg}$ and $\mathrm{hn}$ is an additive equivalence of $\mathrm{ZMod}$ applied to $n$ and $G$.

zmodCyclicMulEquivdefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer modulo cyclic multiplicative equivalence of h (from the name)

English

Assume that $G$ is cyclic. Then the integer modulo cyclic multiplicative equivalence of $h$ is a multiplicative equivalence of the set of multiplicatives of $\mathrm{ZMod}$ applied to the cardinality of $G$ and $G$.

zmodMulEquivOfGeneratordefMathlib.GroupTheory.SpecificGroups.Cyclic, function or constant

Wording

the integer modulo multiplicative equivalence of hg and hn (from the name)

English

Assume that for all elements $x_{1}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{1}}$. Assume that the cardinality of $G$ is equal to $n$. Then the integer modulo multiplicative equivalence of $\mathrm{hg}$ and $\mathrm{hn}$ is a multiplicative equivalence of the set of multiplicatives of $\mathrm{ZMod}$ applied to $n$ and $G$ defined as $\operatorname{toMultiplicative}$ applied to the integer modulo additive equivalence of $\mathrm{hg}$ and $\mathrm{hn}$.

Mathlib.GroupTheory.SpecificGroups.Cyclic.Subgroup

MulDistribMulAction.toMonoidHomZModOfIsCyclicdefMathlib.GroupTheory.SpecificGroups.Cyclic.Subgroup, function or constant

Wording

no wording

English

Let $G$ and $M$ be sets such that the cardinality of $G$ is equal to $n$. Then $\operatorname{toMonoidHomZModOfIsCyclic}$ applied to $G$, $M$ and $\mathrm{hn}$ is a monoid homomorphism of $M$ and $\mathrm{ZMod}$ applied to $n$.

Mathlib.GroupTheory.SpecificGroups.Dihedral

DihedralGroupinductiveMathlib.GroupTheory.SpecificGroups.Dihedral, type

Wording

dihedral group of n (from the name)

English

Let $n$ be a natural number. Then the dihedral groups of $n$ are a basic type.

DihedralGroup.ctorElimTypedefMathlib.GroupTheory.SpecificGroups.Dihedral, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $\mathrm{ZMod}$ applied to $n$ to elements of $\mathrm{motive}$ applied to $\operatorname{r}$ applied to $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\mathrm{ZMod}$ applied to $n$ to elements of $\mathrm{motive}$ applied to $\operatorname{sr}$ applied to $x_{1}$.

DihedralGroup.equivSumdefMathlib.GroupTheory.SpecificGroups.Dihedral, function or constant

Wording

the equivalence sum (from the name)

English

The equivalence sum is an equivalence from the set of dihedral groups of $n$ to $\mathrm{Sum}$ applied to $\mathrm{ZMod}$ applied to $n$ and $\mathrm{ZMod}$ applied to $n$.

DihedralGroup.oddCommuteEquivdefMathlib.GroupTheory.SpecificGroups.Dihedral, function or constant

Wording

the odd commute equivalence of hn (from the name)

English

Assume that $n$ is odd. Then the odd commute equivalence of $\mathrm{hn}$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{\mathrm{Commute} (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {p})})}{\mathrm{Sum} (\mathrm{ZMod} (n), \mathrm{Sum} (\mathrm{ZMod} (n), \mathrm{Sum} (\mathrm{ZMod} (n), \mathrm{Prod} (\mathrm{ZMod} (n), \mathrm{ZMod} (n)))))}$.

DihedralGroup.rconstructorMathlib.GroupTheory.SpecificGroups.Dihedral, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{ZMod}$ applied to $n$. Then $\operatorname{r}$ applied to $x$ is a dihedral group of $n$.

DihedralGroup.srconstructorMathlib.GroupTheory.SpecificGroups.Dihedral, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{ZMod}$ applied to $n$. Then $\operatorname{sr}$ applied to $x$ is a dihedral group of $n$.

Mathlib.GroupTheory.SpecificGroups.KleinFour

IsAddKleinFourclassMathlib.GroupTheory.SpecificGroups.KleinFour, predicate

Wording

no wording

English

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

IsAddKleinFour.addEquivdefMathlib.GroupTheory.SpecificGroups.KleinFour, function or constant

Wording

the additive equivalence of e and he (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$ such that $\EqtMACRoH {e (0)}{0}$. Then the additive equivalence of $e$ and $\mathrm{he}$ is an additive equivalence of $x$ and $x_{1}$ defined as the additive equivalence of $e$.

IsAddKleinFour.addEquiv'defMathlib.GroupTheory.SpecificGroups.KleinFour, function or constant

Wording

the additive equivalence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$ such that $\EqtMACRoH {e (0)}{0}$. Assume that the exponent of $x_{1}$ is equal to $2$. Then the additive equivalence of $e$ is an additive equivalence of $x$ and $x_{1}$.

IsKleinFourclassMathlib.GroupTheory.SpecificGroups.KleinFour, predicate

Wording

no wording

English

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

IsKleinFour.mulEquivdefMathlib.GroupTheory.SpecificGroups.KleinFour, function or constant

Wording

the multiplicative equivalence of e and he (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$ such that $\EqtMACRoH {e (1)}{1}$. Then the multiplicative equivalence of $e$ and $\mathrm{he}$ is a multiplicative equivalence of $x$ and $x_{1}$ defined as the multiplicative equivalence of $e$.

IsKleinFour.mulEquiv'defMathlib.GroupTheory.SpecificGroups.KleinFour, function or constant

Wording

the multiplicative equivalence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$ such that $\EqtMACRoH {e (1)}{1}$. Assume that the exponent of $x_{1}$ is equal to $2$. Then the multiplicative equivalence of $e$ is a multiplicative equivalence of $x$ and $x_{1}$.

Mathlib.GroupTheory.SpecificGroups.Quaternion

QuaternionGroupinductiveMathlib.GroupTheory.SpecificGroups.Quaternion, type

Wording

quaternion group of n (from the name)

English

Let $n$ be a natural number. Then the quaternion groups of $n$ are a basic type.

QuaternionGroup.aconstructorMathlib.GroupTheory.SpecificGroups.Quaternion, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{ZMod}$ applied to $2 \times n$. Then $\operatorname{a}$ applied to $x$ is a quaternion group of $n$.

QuaternionGroup.ctorElimTypedefMathlib.GroupTheory.SpecificGroups.Quaternion, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $\mathrm{ZMod}$ applied to $2 \times n$ to elements of $\mathrm{motive}$ applied to $\operatorname{a}$ applied to $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\mathrm{ZMod}$ applied to $2 \times n$ to elements of $\mathrm{motive}$ applied to $\operatorname{xa}$ applied to $x_{1}$.

QuaternionGroup.quaternionGroupZeroEquivDihedralGroupZerodefMathlib.GroupTheory.SpecificGroups.Quaternion, function or constant

Wording

the quaternion group zero equivalence dihedral group zero (from the name)

English

The quaternion group zero equivalence dihedral group zero is a multiplicative equivalence of the set of quaternion groups of $0$ and the set of dihedral groups of $0$.

QuaternionGroup.xaconstructorMathlib.GroupTheory.SpecificGroups.Quaternion, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{ZMod}$ applied to $2 \times n$. Then $\operatorname{xa}$ applied to $x$ is a quaternion group of $n$.

Mathlib.GroupTheory.SpecificGroups.VirtuallyCyclic

AddGroup.IsVirtuallyAddCyclicclassMathlib.GroupTheory.SpecificGroups.VirtuallyCyclic, predicate

Wording

no wording

English

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

Group.IsVirtuallyCyclicclassMathlib.GroupTheory.SpecificGroups.VirtuallyCyclic, predicate

Wording

no wording

English

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

Mathlib.GroupTheory.SpecificGroups.ZGroup

IsZGroupclassMathlib.GroupTheory.SpecificGroups.ZGroup, predicate

Wording

G is a group (from the name)

English

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

Mathlib.GroupTheory.Subgroup.Center

AddSubgroup.centerdefMathlib.GroupTheory.Subgroup.Center, function or constant

Wording

the center of G (from the docstring)

English

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

AddSubgroup.centerCongrdefMathlib.GroupTheory.Subgroup.Center, function or constant

Wording

the center congruence of e (from the name)

English

Let $e$ be an additive equivalence of $G$ and $H$. Then the center congruence of $e$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (G)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (H)}{x_{3}})}$ defined as the center congruence of $e$.

AddSubgroup.centerToAddOppositedefMathlib.GroupTheory.Subgroup.Center, function or constant

Wording

the center of G (from the docstring)

English

Let $G$ be a set. Then the center of $G$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (G)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{AddOpposite} (G))}{x_{2}})}$ defined as the center.

Subgroup.centerdefMathlib.GroupTheory.Subgroup.Center, function or constant

Wording

the center of G (from the docstring)

English

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

Subgroup.centerCongrdefMathlib.GroupTheory.Subgroup.Center, function or constant

Wording

the center congruence of e (from the name)

English

Let $e$ be a multiplicative equivalence of $G$ and $H$. Then the center congruence of $e$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (G)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (H)}{x_{3}})}$ defined as the center congruence of $e$.

Subgroup.centerToMulOppositedefMathlib.GroupTheory.Subgroup.Center, function or constant

Wording

the center of G (from the docstring)

English

Let $G$ be a set. Then the center of $G$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (G)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{MulOpposite} (G))}{x_{2}})}$ defined as the center.

Mathlib.GroupTheory.Subgroup.Centralizer

AddSubgroup.centralizerdefMathlib.GroupTheory.Subgroup.Centralizer, function or constant

Wording

the centralizer of s (from the name)

English

Let $s$ be an element of $\wp G$. Then the centralizer of $s$ is an additive subgroup of $G$ defined as $\operatorname{mk}$ applied to the centralizer of $s$ and the function that maps $x_{1}$ to $\mathrm{Set\_\_neg\_mem\_addCentralizer}$.

Subgroup.centralizerdefMathlib.GroupTheory.Subgroup.Centralizer, function or constant

Wording

the centralizer of s (from the name)

English

Let $s$ be an element of $\wp G$. Then the centralizer of $s$ is a subgroup of $G$ defined as $\operatorname{mk}$ applied to the centralizer of $s$ and the function that maps $x_{1}$ to $\mathrm{Set\_\_inv\_mem\_centralizer}$.

Subgroup.normalizerMonoidHomdefMathlib.GroupTheory.Subgroup.Centralizer, function or constant

Wording

the homomorphism of H (from the docstring)

English

Let $H$ be a subgroup of $G$. Then the homomorphism of $H$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{normalizer} (H)}{x_{1}})}$ and the set of multiplicative automorphisms of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ defined as the multiplicative automorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{normalizer} (H)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$.

Mathlib.GroupTheory.Subgroup.Saturated

AddSubmonoid.NSMulSaturateddefMathlib.GroupTheory.Subgroup.Saturated, predicate

Wording

no wording

English

Let $H$ be an additive submonoid of $G$. Then $\operatorname{NSMulSaturated}$ holds for $H$, if for all natural numbers $n$, for all elements $g$ of $G$, if $\HSMulhSMulMACRoAL {n}{g}$ is an element of $H$, then $n = 0$ or $g$ is an element of $H$.

Submonoid.PowSaturateddefMathlib.GroupTheory.Subgroup.Saturated, predicate

Wording

no wording

English

Let $H$ be a submonoid of $G$. Then $\operatorname{PowSaturated}$ holds for $H$, if for all natural numbers $n$, for all elements $g$ of $G$, if $g ^ {n}$ is an element of $H$, then $n = 0$ or $g$ is an element of $H$.

Mathlib.GroupTheory.Subgroup.Simple

IsSimpleAddGroupclassMathlib.GroupTheory.Subgroup.Simple, predicate

Wording

A is a simple additive group (from the name)

English

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

IsSimpleGroupclassMathlib.GroupTheory.Subgroup.Simple, predicate

Wording

G is a simple group (from the name)

English

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

Mathlib.GroupTheory.Submonoid.Center

AddSubmonoid.centerdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center of M (from the docstring)

English

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

AddSubmonoid.centerCongrdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center congruence of e (from the name)

English

Let $e$ be an additive equivalence of $M$ and $N$. Then the center congruence of $e$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (M)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (N)}{x_{3}})}$ defined as the center congruence of $e$.

AddSubmonoid.centerToAddOppositedefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center (from the docstring)

English

The center is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (M)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{AddOpposite} (M))}{x_{2}})}$ defined as the center.

AddSubsemigroup.centerCongrdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center congruence of e (from the name)

English

AddSubsemigroup.centerToAddOppositedefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center (from the docstring)

English

Submonoid.centerdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center of M (from the docstring)

English

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

Submonoid.centerCongrdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center congruence of e (from the name)

English

Let $e$ be a multiplicative equivalence of $M$ and $N$. Then the center congruence of $e$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (M)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (N)}{x_{3}})}$ defined as the center congruence of $e$.

Submonoid.centerToMulOppositedefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center (from the docstring)

English

The center is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (M)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{MulOpposite} (M))}{x_{2}})}$ defined as the center.

Subsemigroup.centerCongrdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center congruence of e (from the name)

English

Subsemigroup.centerToMulOppositedefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the center (from the docstring)

English

addUnitsCenterToCenterAddUnitsdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the additive unit center to center additive unit of M (from the name)

English

Let $M$ be a set. Then the additive unit center to center additive unit of $M$ is an additive monoid homomorphism of the set of additive units of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (M)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{AddUnits} (M))}{x_{2}})}$.

unitsCenterToCenterUnitsdefMathlib.GroupTheory.Submonoid.Center, function or constant

Wording

the unit center to center unit of M (from the name)

English

Let $M$ be a set. Then the unit center to center unit of $M$ is a monoid homomorphism of $\UnitsMACRoAO {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (M)}{x_{1}})})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{center} (\UnitsMACRoAO {M})}{x_{2}})}$.

Mathlib.GroupTheory.Submonoid.Centralizer

AddSubmonoid.centralizerdefMathlib.GroupTheory.Submonoid.Centralizer, function or constant

Wording

the centralizer of S (from the docstring)

English

Let $S$ be an element of $\wp M$. Then the centralizer of $S$ is an additive submonoid of $M$.

Submonoid.centralizerdefMathlib.GroupTheory.Submonoid.Centralizer, function or constant

Wording

the centralizer of S (from the docstring)

English

Let $S$ be an element of $\wp M$. Then the centralizer of $S$ is a submonoid of $M$.

Mathlib.GroupTheory.Submonoid.Inverses

AddSubmonoid.fromCommLeftNegdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

no wording

English

Let $S$ be an additive submonoid of $M$. Then $\operatorname{fromCommLeftNeg}$ applied to $S$ is an additive monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{leftNeg} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

AddSubmonoid.fromLeftNegdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

no wording

English

Let $S$ be an additive submonoid of $M$. Let $x_{1}$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{leftNeg} (S)}{x_{3}})}$. Then $\operatorname{fromLeftNeg}$ applied to $S$ and $x_{1}$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

AddSubmonoid.leftNegdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

the left negation of S (from the name)

English

Let $S$ be an additive submonoid of $M$. Then the left negation of $S$ is an additive submonoid of $M$.

AddSubmonoid.leftNegEquivdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

the left negation equivalence of S and hS (from the name)

English

Let $S$ be an additive submonoid of $M$ such that $S \leq \operatorname{addSubmonoid} (M)$. Then the left negation equivalence of $S$ and $\mathrm{hS}$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{leftNeg} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

Submonoid.fromCommLeftInvdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $M$. Then $\operatorname{fromCommLeftInv}$ applied to $S$ is a monoid homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{leftInv} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

Submonoid.fromLeftInvdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $M$. Let $x_{1}$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{leftInv} (S)}{x_{3}})}$. Then $\operatorname{fromLeftInv}$ applied to $S$ and $x_{1}$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

Submonoid.leftInvdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

the left inverse of S (from the name)

English

Let $S$ be a submonoid of $M$. Then the left inverse of $S$ is a submonoid of $M$.

Submonoid.leftInvEquivdefMathlib.GroupTheory.Submonoid.Inverses, function or constant

Wording

the left inverse equivalence of S and hS (from the name)

English

Let $S$ be a submonoid of $M$ such that $S \leq \operatorname{submonoid} (M)$. Then the left inverse equivalence of $S$ and $\mathrm{hS}$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{leftInv} (S)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$.

Mathlib.GroupTheory.Subsemigroup.Center

AddSubsemigroup.centerdefMathlib.GroupTheory.Subsemigroup.Center, function or constant

Wording

the center of M (from the docstring)

English

Let $M$ be a set. Then the center of $M$ is an additive subsemigroup of $M$ defined as $\operatorname{mk}$ applied to the center of $M$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Set\_\_add\_mem\_addCenter}$.

Subsemigroup.centerdefMathlib.GroupTheory.Subsemigroup.Center, function or constant

Wording

the center of M (from the docstring)

English

Let $M$ be a set. Then the center of $M$ is a subsemigroup of $M$ defined as $\operatorname{mk}$ applied to the center of $M$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Set\_\_mul\_mem\_center}$.

Mathlib.GroupTheory.Subsemigroup.Centralizer

AddSubsemigroup.centralizerdefMathlib.GroupTheory.Subsemigroup.Centralizer, function or constant

Wording

the centralizer of S (from the docstring)

English

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

Subsemigroup.centralizerdefMathlib.GroupTheory.Subsemigroup.Centralizer, function or constant

Wording

the centralizer of S (from the docstring)

English

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

Mathlib.GroupTheory.Sylow

IsPGroup.toSylowdefMathlib.GroupTheory.Sylow, function or constant

Wording

no wording

English

Assume that $p$ is a group. Assume that $p$ does not divide the index of $P$. Then $\operatorname{toSylow}$ applied to $\mathrm{hP1}$ and $\mathrm{hP2}$ is an element of $\mathrm{Sylow}$ applied to $p$ and $G$.

SylowstructureMathlib.GroupTheory.Sylow, type

Wording

no wording

English

Let $p$ be a natural number. Let $G$ be a set. Then the elements of $\mathrm{Sylow}$ applied to $p$ and $G$ are a basic type.

Sylow.comapOfInjectivedefMathlib.GroupTheory.Sylow, function or constant

Wording

the preimage of P and x2 (from the name)

English

Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$. Let $x_{2}$ be a monoid homomorphism of $K$ and $G$ such that $\operatorname{coe}$ applied to $x_{2}$ is injective and $\operatorname{toSubgroup}$ applied to $P$ is less than or equal to the range of $x_{2}$. Then the preimage of $P$ and $x_{2}$ is an element of $\mathrm{Sylow}$ applied to $p$ and $K$ defined as the preimage of $P$ and $x_{2}$.

Sylow.comapOfKerIsPGroupdefMathlib.GroupTheory.Sylow, function or constant

Wording

the preimage of P and x2 (from the name)

English

Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$. Let $x_{2}$ be a monoid homomorphism of $K$ and $G$. Assume that $p$ is a group. Assume that $\operatorname{toSubgroup}$ applied to $P$ is less than or equal to the range of $x_{2}$. Then the preimage of $P$ and $x_{2}$ is an element of $\mathrm{Sylow}$ applied to $p$ and $K$.

Sylow.directProductOfNormaldefMathlib.GroupTheory.Sylow, function or constant

Wording

the direct product of hn (from the name)

English

Assume that for all elements $p_{1}$ of $\Natural$, if the proposition that $p_{1}$ is prime is a fact, then for all elements $P_{1}$ of $\mathrm{Sylow}$ applied to $p_{1}$ and $G$, $\operatorname{toSubgroup}$ applied to $P_{1}$ is normal. Then the direct product of $\mathrm{hn}$ is a multiplicative equivalence of the set of functions from elements $p$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{primeFactors} (\operatorname{card} (G))}{x_{2}})}$ and elements $P$ of $\mathrm{Sylow}$ applied to $p$ and $G$ to elements of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {P}{x_{1}})}$ and $G$.

Sylow.equivdefMathlib.GroupTheory.Sylow, function or constant

Wording

the equivalence of P and Q (from the name)

English

Let $P$ and $Q$ be elements of $\mathrm{Sylow}$ applied to $p$ and $G$. Then the equivalence of $P$ and $Q$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (P)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (Q)}{x_{2}})}$.

Sylow.equivProdPrimeFactorsdefMathlib.GroupTheory.Sylow, function or constant

Wording

the equivalence product prime factor of h (from the name)

English

Assume that $p \neq 0$. Then the equivalence product prime factor of $h$ is an element of $\EquivMACRoAE {\mathrm{Sylow} (p , G)}{\mathrm{Sylow} (\FinsetProd {\operatorname{primeFactors} (p)}{a}{\mathrm{id} (a)}, G)}$.

Sylow.equivQuotientNormalizerdefMathlib.GroupTheory.Sylow, function or constant

Wording

the equivalence quotient normalizer of P (from the name)

English

Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$. Then the equivalence quotient normalizer of $P$ is an equivalence from $\mathrm{Sylow}$ applied to $p$ and $G$ to the set of quotients of $G$ and the normalizer of $P$.

Sylow.equivSMuldefMathlib.GroupTheory.Sylow, function or constant

Wording

the equivalence product of P and g (from the name)

English

Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$. Let $g$ be an element of $G$. Then the equivalence product of $P$ and $g$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (P)}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (\HSMulhSMulMACRoAL {g}{P})}{x_{2}})}$ defined as the equivalence product of $\operatorname{conj}$ applied to $g$ and $\operatorname{toSubgroup}$ applied to $P$.

Sylow.fixedPointsMulLeftCosetsEquivQuotientdefMathlib.GroupTheory.Sylow, function or constant

Wording

the fixed point multiplicative left coset equivalence quotient of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the fixed point multiplicative left coset equivalence quotient of $H$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{fixedPoints} (\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}, \operatorname{Quotient} (G , H)))}{\operatorname{Quotient} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{normalizer} (H)}{x_{2}})}, \operatorname{comap} (\operatorname{subtype} (\operatorname{normalizer} (H)), H))}$.

Sylow.mapSurjectivedefMathlib.GroupTheory.Sylow, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$. Then $\operatorname{mapSurjective}$ applied to $\mathrm{hf}$ and $P$ is an element of $\mathrm{Sylow}$ applied to $p$ and $\mathrm{G'}$.

Sylow.ofCarddefMathlib.GroupTheory.Sylow, function or constant

Wording

no wording

English

Let $H$ be a subgroup of $G$ such that the cardinality of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ is equal to the exponentiation of $p$ to the multiplicity of $p$ in the cardinality of $G$. Then $\operatorname{ofCard}$ applied to $H$ and $\mathrm{card\_eq}$ is an element of $\mathrm{Sylow}$ applied to $p$ and $G$.

Sylow.subtypedefMathlib.GroupTheory.Sylow, function or constant

Wording

the subtype of P and h (from the name)

English

Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$ such that $\operatorname{toSubgroup} (P)\leq N$. Then the subtype of $P$ and $h$ is an element of $\mathrm{Sylow}$ applied to $p$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {N}{x_{1}})}$.

Mathlib.GroupTheory.Torsion

AddCommGroup.freeRankdefMathlib.GroupTheory.Torsion, function or constant

Wording

the free rank of G (from the docstring)

English

Let $G$ be a set. Then the free rank of $G$ is a natural number defined as the rank of the set of quotients of $G$ and the torsion additive subgroup of $G$.

AddCommGroup.primaryComponentdefMathlib.GroupTheory.Torsion, function or constant

Wording

the primary component of G and p (from the name)

English

Let $G$ be a set. Let $p$ be a natural number. Then the primary component of $G$ and $p$ is an additive subgroup of $G$.

AddCommGroup.torsiondefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion additive subgroup of G (from the docstring)

English

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

AddCommMonoid.Torsion.ofTorsiondefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion of G (from the name)

English

Let $G$ be a set. Then the torsion of $G$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addTorsion} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{addTorsion} (G)}{x_{2}})})}{x_{1}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{addTorsion} (G)}{x_{3}})}$ defined as the torsion additive equivalence of $\operatorname{isAddTorsion}$.

AddCommMonoid.addTorsiondefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion additive submonoid of G (from the docstring)

English

Let $G$ be a set. Then the torsion additive submonoid of $G$ is an additive submonoid of $G$.

AddCommMonoid.primaryComponentdefMathlib.GroupTheory.Torsion, function or constant

Wording

the primary component of G and p (from the name)

English

Let $G$ be a set. Let $p$ be a natural number. Then the primary component of $G$ and $p$ is an additive submonoid of $G$.

CommGroup.freeRankdefMathlib.GroupTheory.Torsion, function or constant

Wording

the free rank of G (from the docstring)

English

Let $G$ be a set. Then the free rank of $G$ is a natural number defined as the rank of the set of quotients of $G$ and the torsion subgroup of $G$.

CommGroup.primaryComponentdefMathlib.GroupTheory.Torsion, function or constant

Wording

the primary component of G and p (from the name)

English

Let $G$ be a set. Let $p$ be a natural number. Then the primary component of $G$ and $p$ is a subgroup of $G$.

CommGroup.torsiondefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion subgroup of G (from the docstring)

English

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

CommMonoid.Torsion.ofTorsiondefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion of G (from the name)

English

Let $G$ be a set. Then the torsion of $G$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{torsion} (G)}{x_{2}})})}{x_{1}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{torsion} (G)}{x_{3}})}$ defined as the torsion multiplicative equivalence of $\operatorname{isMulTorsion}$.

CommMonoid.primaryComponentdefMathlib.GroupTheory.Torsion, function or constant

Wording

the primary component of G and p (from the name)

English

Let $G$ be a set. Let $p$ be a natural number. Then the primary component of $G$ and $p$ is a submonoid of $G$.

CommMonoid.torsiondefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion submonoid of G (from the docstring)

English

Let $G$ be a set. Then the torsion submonoid of $G$ is a submonoid of $G$.

IsAddTorsiondefMathlib.GroupTheory.Torsion, predicate

Wording

G is a additive torsion (from the name)

English

Let $G$ be a set. Then $G$ is an additive torsion, if for all elements $g$ of $G$, $\mathrm{IsOfFinAddOrder}$ holds for $g$.

IsAddTorsion.torsionAddEquivdefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion additive equivalence of tG (from the name)

English

Assume that $G$ is an additive torsion. Then the torsion additive equivalence of $\mathrm{tG}$ is an additive equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{addTorsion} (G)}{x_{1}})}$ and $G$ defined as the composition of the additive submonoid congruence of $\mathrm{IsAddTorsion\_\_torsion\_eq\_top}$ applied to $\mathrm{tG}$ and the top.

IsMulTorsiondefMathlib.GroupTheory.Torsion, predicate

Wording

G is a multiplicative torsion (from the name)

English

Let $G$ be a set. Then $G$ is a multiplicative torsion, if for all elements $g$ of $G$, $\mathrm{IsOfFinOrder}$ holds for $g$.

IsMulTorsion.torsionMulEquivdefMathlib.GroupTheory.Torsion, function or constant

Wording

the torsion multiplicative equivalence of tG (from the name)

English

Assume that $G$ is a multiplicative torsion. Then the torsion multiplicative equivalence of $\mathrm{tG}$ is a multiplicative equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{torsion} (G)}{x_{1}})}$ and $G$ defined as the composition of the submonoid congruence of $\mathrm{IsMulTorsion\_\_torsion\_eq\_top}$ applied to $\mathrm{tG}$ and the top.

Mathlib.GroupTheory.Transfer

AddMonoidHom.transferdefMathlib.GroupTheory.Transfer, function or constant

Wording

the transfer of x2 (from the name)

English

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

AddSubgroup.leftTransversals.diffdefMathlib.GroupTheory.Transfer, function or constant

Wording

the difference of S and T (from the name)

English

Let $x_{2}$ be an additive monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $A$. Let $S$ and $T$ be elements of $\operatorname{LeftTransversal}$ applied to $H$. Then the difference of $S$ and $T$ is an element of $A$.

MonoidHom.transferdefMathlib.GroupTheory.Transfer, function or constant

Wording

the transfer of x2 (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $A$. Then the transfer of $x_{2}$ is a monoid homomorphism of $G$ and $A$.

MonoidHom.transferCenterPowdefMathlib.GroupTheory.Transfer, function or constant

Wording

the transfer homomorphism of G (from the docstring)

English

Let $G$ be a set. Then the transfer homomorphism of $G$ is a monoid homomorphism of $G$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{center} (G)}{x_{1}})}$.

MonoidHom.transferSylowdefMathlib.GroupTheory.Transfer, function or constant

Wording

no wording

English

Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$ such that the normalizer of $P$ is less than or equal to the centralizer of $P$. Then $\operatorname{transferSylow}$ applied to $P$ and $\mathrm{hP}$ is a monoid homomorphism of $G$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (P)}{x_{1}})}$ defined as the transfer of the identity map of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (P)}{x_{1}})}$.

Subgroup.leftTransversals.diffdefMathlib.GroupTheory.Transfer, function or constant

Wording

the difference of S and T (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $A$. Let $S$ and $T$ be elements of $\operatorname{LeftTransversal}$ applied to $H$. Then the difference of $S$ and $T$ is an element of $A$.

Subgroup.transferFunctiondefMathlib.GroupTheory.Transfer, function or constant

Wording

the transfer function of g and x1 (from the name)

English

Let $H$ be a subgroup of $G$. Let $g$ be an element of $G$. Let $x_{1}$ be a quotient of $G$ and $H$. Then the transfer function of $g$ and $x_{1}$ is an element of $G$ defined as the product of the exponentiation of $g$ to the cast of $\operatorname{snd}$ applied to $\operatorname{quotientEquivSigmaZMod}$ applied to $H$, $g$ and $x_{1}$ and $\operatorname{out}$ applied to $\operatorname{out}$ applied to $\operatorname{fst}$ applied to $\operatorname{quotientEquivSigmaZMod}$ applied to $H$, $g$ and $x_{1}$.

Subgroup.transferSetdefMathlib.GroupTheory.Transfer, function or constant

Wording

the transfer transversal as a set of H and g (from the docstring)

English

Let $H$ be a subgroup of $G$. Let $g$ be an element of $G$. Then the transfer transversal as a set of $H$ and $g$ is an element of $\wp G$ defined as the range of $\operatorname{transferFunction}$ applied to $g$.

Subgroup.transferTransversaldefMathlib.GroupTheory.Transfer, function or constant

Wording

no wording

English

Let $H$ be a subgroup of $G$. Let $g$ be an element of $G$. Then $\operatorname{transferTransversal}$ applied to $H$ and $g$ is an element of $\operatorname{LeftTransversal}$ applied to $H$ defined as the transfer transversal as a set of $H$ and $g$.