Definitions: Mathlib.GroupTheory, part 1 of 3

396 definitions of 35 modules, Mathlib.GroupTheory.Abelianization.Defs to Mathlib.GroupTheory.FreeGroup.IsFreeGroup. ‹ previous next ›

Mathlib.GroupTheory.Abelianization.Defs

AbelianizationdefMathlib.GroupTheory.Abelianization.Defs, type
Wording
abelianization of G (from the name)
English
Let $G$ be a set. Then an abelianization of $G$ is an element of the function that maps $G$ to the set of quotients of $G$ and the commutator subgroup of $G$.
Abelianization.equivOfCommdefMathlib.GroupTheory.Abelianization.Defs, function or constant
Wording
the equivalence (from the name)
English
The equivalence is a multiplicative equivalence of $H$ and the set of abelianizations of $H$.
Abelianization.liftdefMathlib.GroupTheory.Abelianization.Defs, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of monoid homomorphisms of $G$ and $A$ to the set of monoid homomorphisms of the set of abelianizations of $G$ and $A$.
Abelianization.mapdefMathlib.GroupTheory.Abelianization.Defs, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a monoid homomorphism of $G$ and $H$. Then the map of $f$ is a monoid homomorphism of the set of abelianizations of $G$ and the set of abelianizations of $H$ defined as $\operatorname{lift}$ applied to the composition of $\operatorname{of}$ and $f$.
Abelianization.ofdefMathlib.GroupTheory.Abelianization.Defs, function or constant
Wording
no wording
English
$\operatorname{of}$ is a monoid homomorphism of $G$ and the set of abelianizations of $G$.
MulEquiv.abelianizationCongrdefMathlib.GroupTheory.Abelianization.Defs, function or constant
Wording
the abelianization congruence of e (from the name)
English
Let $e$ be a multiplicative equivalence of $G$ and $H$. Then the abelianization congruence of $e$ is a multiplicative equivalence of the set of abelianizations of $G$ and the set of abelianizations of $H$.

Mathlib.GroupTheory.ArchimedeanDensely

LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_posdefMathlib.GroupTheory.ArchimedeanDensely, function or constant
Wording
the integer order additive monoid isomorphism of h2 (from the name)
English
Assume that $\mathrm{IsLeast}$ holds for $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{Lt} (0 , y)$ and $x_{2}$. Then the integer order additive monoid isomorphism of $h_{2}$ is an order additive monoid isomorphism of $G$ and $\Integer$.
LinearOrderedAddCommGroup.zmultiplesOrderAddMonoidIsodefMathlib.GroupTheory.ArchimedeanDensely, function or constant
Wording
no wording
English
Let $x_{4}$ be an element of $G$. Let $y$ be an element of $\mathrm{G'}$ such that $\EqtMACRoH {x_{4}}{0}$, if and only if $\EqtMACRoH {y}{0}$. Then $\operatorname{zmultiplesOrderAddMonoidIso}$ applied to $x_{4}$, $y$ and $\mathrm{hxy}$ is an order additive monoid isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (x_{4})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (y)}{x_{6}})}$.
LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_ltdefMathlib.GroupTheory.ArchimedeanDensely, function or constant
Wording
the multiplicative integer order monoid isomorphism of h2 (from the name)
English
Assume that $\mathrm{IsLeast}$ holds for $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{Lt} (1 , y)$ and $x_{2}$. Then the multiplicative integer order monoid isomorphism of $h_{2}$ is an order monoid isomorphism of $G$ and the set of multiplicatives of $\Integer$ defined as $\operatorname{toMultiplicativeRight}$ applied to the integer order additive monoid isomorphism of $h_{2}$.
LinearOrderedCommGroup.zpowersOrderMonoidIsodefMathlib.GroupTheory.ArchimedeanDensely, function or constant
Wording
no wording
English
Let $x_{4}$ be an element of $G$. Let $y$ be an element of $\mathrm{G'}$ such that $\EqtMACRoH {x_{4}}{1}$, if and only if $\EqtMACRoH {y}{1}$. Then $\operatorname{zpowersOrderMonoidIso}$ applied to $x_{4}$, $y$ and $\mathrm{hxy}$ is an order monoid isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{zpowers} (x_{4})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{zpowers} (y)}{x_{6}})}$.

Mathlib.GroupTheory.Commensurable

AddSubgroup.CommensurabledefMathlib.GroupTheory.Commensurable, predicate
Wording
no wording
English
Let $H$ and $K$ be additive subgroups of $G$. Then $\operatorname{Commensurable}$ holds for $H$ and $K$, if $\operatorname{IsFiniteRelIndex}$ holds for $H$ and $K$ and $\operatorname{IsFiniteRelIndex}$ holds for $K$ and $H$.
Subgroup.CommensurabledefMathlib.GroupTheory.Commensurable, predicate
Wording
no wording
English
Let $H$ and $K$ be subgroups of $G$. Then $\operatorname{Commensurable}$ holds for $H$ and $K$, if $\operatorname{IsFiniteRelIndex}$ holds for $H$ and $K$ and $\operatorname{IsFiniteRelIndex}$ holds for $K$ and $H$.
Subgroup.Commensurable.commensuratordefMathlib.GroupTheory.Commensurable, function or constant
Wording
no wording
English
Let $H$ be a subgroup of $G$. Then $\operatorname{commensurator}$ applied to $H$ is a subgroup of $G$.

Mathlib.GroupTheory.Commutator.Basic

addCommutatordefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the commutator subgroup of G (from the docstring)
English
Let $G$ be a set. Then the commutator subgroup of $G$ is an additive subgroup of $G$ defined as the bracket of the top and the top.
addCommutatorRepresentativesdefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the additive commutator representative of G (from the name)
English
Let $G$ be a set. Then the additive commutator representative of $G$ is an element of $\wp \mathrm{Prod} (G , G)$.
addCommutatorSetdefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the additive commutator set of G (from the name)
English
Let $G$ be a set. Then the additive commutator set of $G$ is an element of $\wp G$ defined as $\operatorname{ofPred}$ applied to the function that maps $g$ to the proposition that there exist elements $x_{1}$ and $x_{2}$ of $G$, such that the bracket of $x_{1}$ and $x_{2}$ is equal to $g$.
closureAddCommutatorRepresentativesdefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the closure additive commutator representative of G (from the name)
English
Let $G$ be a set. Then the closure additive commutator representative of $G$ is an additive subgroup of $G$ defined as the closure of the union of the image of $\ProdfstMACRoZ$ and the additive commutator representative of $G$ and the image of $\ProdsndMACRoAA$ and the additive commutator representative of $G$.
closureCommutatorRepresentativesdefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the closure commutator representative of G (from the name)
English
Let $G$ be a set. Then the closure commutator representative of $G$ is a subgroup of $G$ defined as the closure of the union of the image of $\ProdfstMACRoZ$ and the commutator representative of $G$ and the image of $\ProdsndMACRoAA$ and the commutator representative of $G$.
commutatordefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the commutator subgroup of G (from the docstring)
English
Let $G$ be a set. Then the commutator subgroup of $G$ is a subgroup of $G$ defined as the bracket of the top and the top.
commutatorRepresentativesdefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the commutator representative of G (from the name)
English
Let $G$ be a set. Then the commutator representative of $G$ is an element of $\wp \mathrm{Prod} (G , G)$.
commutatorSetdefMathlib.GroupTheory.Commutator.Basic, function or constant
Wording
the commutator set of G (from the name)
English
Let $G$ be a set. Then the commutator set of $G$ is an element of $\wp G$ defined as $\operatorname{ofPred}$ applied to the function that maps $g$ to the proposition that there exist elements $x_{1}$ and $x_{2}$ of $G$, such that the bracket of $x_{1}$ and $x_{2}$ is equal to $g$.

Mathlib.GroupTheory.CommutingProbability

DihedralGroup.ProductdefMathlib.GroupTheory.CommutingProbability, type
Wording
product of l (from the name)
English
Let $l$ be a list of natural numbers. Then the products of $l$ are a basic type.
DihedralGroup.reciprocalFactorsdefMathlib.GroupTheory.CommutingProbability, function or constant
Wording
the reciprocal factor of n (from the name)
English
Let $n$ be a natural number. Then the reciprocal factor of $n$ is a list of natural numbers.
commProbdefMathlib.GroupTheory.CommutingProbability, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\mathrm{commProb}$ applied to $M$ is a rational number defined as the quotient of the cardinality of $\SubtypeSet {p}{\mathrm{Commute} (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {p})}$ and the exponentiation of the cardinality of $M$ to $2$.

Mathlib.GroupTheory.Complement

AddSubgroup.IsComplementdefMathlib.GroupTheory.Complement, predicate
Wording
no wording
English
Let $S$ and $T$ be elements of $\wp G$. Then $\operatorname{IsComplement}$ holds for $S$ and $T$, if the function that maps $x_{1}$ to $\ProdfstMACRoZ {x_{1}}+ \ProdsndMACRoAA {x_{1}}$ is bijective.
AddSubgroup.IsComplement'defMathlib.GroupTheory.Complement, predicate
Wording
no wording
English
Let $H$ and $K$ be additive subgroups of $G$. Then $\operatorname{IsComplement'}$ holds for $H$ and $K$, if $\operatorname{IsComplement}$ holds for $H$ and $K$.
AddSubgroup.IsComplement.leftQuotientEquivdefMathlib.GroupTheory.Complement, function or constant
Wording
the left quotient equivalence of hS (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $S$ and $H$. Then the left quotient equivalence of $\mathrm{hS}$ is an equivalence from the set of quotients of $G$ and $H$ to the set of elements of $S$.
AddSubgroup.IsComplement.rightQuotientEquivdefMathlib.GroupTheory.Complement, function or constant
Wording
the right quotient equivalence of hT (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $H$ and $T$. Then the right quotient equivalence of $\mathrm{hT}$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{rightRel}$ applied to $H$ to the set of elements of $T$.
AddSubgroup.IsComplement.toLeftFundefMathlib.GroupTheory.Complement, function or constant
Wording
the left function of hS and x1 (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $S$ and $H$. Let $x_{1}$ be an element of $G$. Then the left function of $\mathrm{hS}$ and $x_{1}$ is an element of $S$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the left quotient equivalence of $\mathrm{hS}$, $\operatorname{mk''}$ and $x_{1}$.
AddSubgroup.IsComplement.toRightFundefMathlib.GroupTheory.Complement, function or constant
Wording
the right function of hT and x1 (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $H$ and $T$. Let $x_{1}$ be an element of $G$. Then the right function of $\mathrm{hT}$ and $x_{1}$ is an element of $T$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the right quotient equivalence of $\mathrm{hT}$, $\operatorname{mk''}$ and $x_{1}$.
AddSubgroup.LeftTransversaldefMathlib.GroupTheory.Complement, type
Wording
no wording
English
Let $H$ be an additive subgroup of $G$. Then an element of $\operatorname{LeftTransversal}$ applied to $H$ is an element of the function that maps $H$ to $\SubtypeSet {S}{\operatorname{IsComplement} (S , H)}$.
AddSubgroup.RightTransversaldefMathlib.GroupTheory.Complement, type
Wording
no wording
English
Let $H$ be an additive subgroup of $G$. Then an element of $\operatorname{RightTransversal}$ applied to $H$ is an element of the function that maps $H$ to $\SubtypeSet {T}{\operatorname{IsComplement} (H , T)}$.
Subgroup.IsComplementdefMathlib.GroupTheory.Complement, predicate
Wording
no wording
English
Let $S$ and $T$ be elements of $\wp G$. Then $\operatorname{IsComplement}$ holds for $S$ and $T$, if the function that maps $x_{1}$ to $\ProdfstMACRoZ {x_{1}}\times \ProdsndMACRoAA {x_{1}}$ is bijective.
Subgroup.IsComplement'defMathlib.GroupTheory.Complement, predicate
Wording
no wording
English
Let $H$ and $K$ be subgroups of $G$. Then $\operatorname{IsComplement'}$ holds for $H$ and $K$, if $\operatorname{IsComplement}$ holds for $H$ and $K$.
Subgroup.IsComplement'.QuotientMulEquivdefMathlib.GroupTheory.Complement, function or constant
Wording
the quotient multiplicative equivalence of h1 (from the name)
English
Assume that $\operatorname{IsComplement'}$ holds for $H$ and $K$. Then the quotient multiplicative equivalence of $h_{1}$ is a multiplicative equivalence of the set of quotients of $G$ and $K$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$.
Subgroup.IsComplement.equivdefMathlib.GroupTheory.Complement, function or constant
Wording
the equivalence of hST (from the docstring)
English
Assume that $\operatorname{IsComplement}$ holds for $S$ and $T$. Then the equivalence of $\mathrm{hST}$ is an equivalence from $G$ to $\mathrm{Prod}$ applied to the set of elements of $S$ and the set of elements of $T$ defined as the inverse of the equivalence of the function that maps $x_{1}$ to $\ProdfstMACRoZ {x_{1}}\times \ProdsndMACRoAA {x_{1}}$ and $\mathrm{hST}$.
Subgroup.IsComplement.leftQuotientEquivdefMathlib.GroupTheory.Complement, function or constant
Wording
the left quotient equivalence of hS (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $S$ and $H$. Then the left quotient equivalence of $\mathrm{hS}$ is an equivalence from the set of quotients of $G$ and $H$ to the set of elements of $S$.
Subgroup.IsComplement.rightQuotientEquivdefMathlib.GroupTheory.Complement, function or constant
Wording
the right quotient equivalence of hT (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $H$ and $T$. Then the right quotient equivalence of $\mathrm{hT}$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{rightRel}$ applied to $H$ to the set of elements of $T$.
Subgroup.IsComplement.toLeftFundefMathlib.GroupTheory.Complement, function or constant
Wording
the left function of hS and x1 (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $S$ and $H$. Let $x_{1}$ be an element of $G$. Then the left function of $\mathrm{hS}$ and $x_{1}$ is an element of $S$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the left quotient equivalence of $\mathrm{hS}$, $\operatorname{mk''}$ and $x_{1}$.
Subgroup.IsComplement.toRightFundefMathlib.GroupTheory.Complement, function or constant
Wording
the right function of hT and x1 (from the name)
English
Assume that $\operatorname{IsComplement}$ holds for $H$ and $T$. Let $x_{1}$ be an element of $G$. Then the right function of $\mathrm{hT}$ and $x_{1}$ is an element of $T$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the right quotient equivalence of $\mathrm{hT}$, $\operatorname{mk''}$ and $x_{1}$.
Subgroup.LeftTransversaldefMathlib.GroupTheory.Complement, type
Wording
no wording
English
Let $H$ be a subgroup of $G$. Then an element of $\operatorname{LeftTransversal}$ applied to $H$ is an element of the function that maps $H$ to $\SubtypeSet {S}{\operatorname{IsComplement} (S , H)}$.
Subgroup.RightTransversaldefMathlib.GroupTheory.Complement, type
Wording
no wording
English
Let $H$ be a subgroup of $G$. Then an element of $\operatorname{RightTransversal}$ applied to $H$ is an element of the function that maps $H$ to $\SubtypeSet {T}{\operatorname{IsComplement} (H , T)}$.

Mathlib.GroupTheory.Congruence.Basic

AddCon.addSubmonoiddefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the additive submonoid of c (from the name)
English
Let $c$ be an additive congruence relation of $M$. Then the additive submonoid of $c$ is an additive submonoid of $\mathrm{Prod}$ applied to $M$ and $M$.
AddCon.comapQuotientEquivdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the preimage quotient equivalence of c and f (from the name)
English
Let $c$ be an additive congruence relation of $M$. Let $f$ be an additive monoid homomorphism of $N$ and $M$. Then the preimage quotient equivalence of $c$ and $f$ is an additive equivalence of the set of quotients of the preimage of $\operatorname{coe}$ applied to $f$ and $c$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (\operatorname{comp} (\operatorname{mk'} (c), f))}{x_{2}})}$ defined as the composition of the congruence of the identity map of $N$ and $\mathrm{AddCon\_\_comap\_eq}$ and the quotient kernel equivalence range of the composition of $\operatorname{mk'}$ applied to $c$ and $f$.
AddCon.comapQuotientEquivOfSurjdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the preimage quotient equivalence of c and f (from the name)
English
Let $c$ be an additive congruence relation of $M$. Let $f$ be an additive monoid homomorphism of $N$ and $M$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the preimage quotient equivalence of $c$ and $f$ is an additive equivalence of the set of quotients of the preimage of $\operatorname{coe}$ applied to $f$ and $c$ and the set of quotients of $c$.
AddCon.congrdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the congruence of e and h (from the name)
English
Let $e$ be an additive equivalence of $M$ and $N$ such that $c$ is equal to the preimage of $\operatorname{coe}$ applied to $e$ and $d$. Then the congruence of $e$ and $h$ is an additive equivalence of the set of quotients of $c$ and the set of quotients of $d$.
AddCon.ofAddSubmonoiddefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the additive congruence relation of N and H (from the name)
English
Let $N$ be an additive submonoid of $\mathrm{Prod}$ applied to $M$ and $M$ such that the function that maps $x_{1}$ and $y$ to $\MembershipmemMACRoT {N}{(\ProdmkMACRoU {x_{1}}{y})}$ is an equivalence relation. Then the additive congruence relation of $N$ and $H$ is an additive congruence relation of $M$.
AddCon.pidefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the product of C (from the docstring)
English
Let $C$ be a function from elements $i_{1}$ of $x$ to additive congruence relations of $f$ applied to $i_{1}$. Then the product of $i_{1}$ is an additive congruence relation of the set of functions from elements $i$ of $x$ to elements of $f$ applied to $i$.
AddCon.proddefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the product of c and d (from the name)
English
Let $c$ be an additive congruence relation of $M$. Let $d$ be an additive congruence relation of $N$. Then the product of $c$ and $d$ is an additive congruence relation of $\mathrm{Prod}$ applied to $M$ and $N$.
AddCon.quotientKerEquivOfRightInversedefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient kernel equivalence of f and g (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $P$. Let $g$ be a function from elements of $P$ to elements of $M$ such that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $g$ is an additive equivalence of the set of quotients of the kernel of $f$ and $P$.
AddCon.quotientKerEquivOfSurjectivedefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient kernel equivalence of f and hf (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $P$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $\mathrm{hf}$ is an additive equivalence of the set of quotients of the kernel of $f$ and $P$.
AddCon.quotientKerEquivRangedefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient kernel equivalence range of f (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $P$. Then the quotient kernel equivalence range of $f$ is an additive equivalence of the set of quotients of the kernel of $f$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (f)}{x_{2}})}$.
AddCon.quotientQuotientEquivQuotientdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient quotient equivalence quotient of c and d (from the name)
English
Let $c$ and $d$ be additive congruence relations of $M$ such that $c \leq d$. Then the quotient quotient equivalence quotient of $c$ and $d$ is an additive equivalence of the set of quotients of the kernel of the map of $c$ and $d$ and the set of quotients of $d$.
Con.comapQuotientEquivdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the preimage quotient equivalence of c and f (from the name)
English
Let $c$ be a congruence relation of $M$. Let $f$ be a monoid homomorphism of $N$ and $M$. Then the preimage quotient equivalence of $c$ and $f$ is a multiplicative equivalence of the set of quotients of the preimage of $\operatorname{coe}$ applied to $f$ and $c$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (\operatorname{comp} (\operatorname{mk'} (c), f))}{x_{2}})}$ defined as the composition of the congruence of the identity map of $N$ and $\mathrm{Con\_\_comap\_eq}$ and the quotient kernel equivalence range of the composition of $\operatorname{mk'}$ applied to $c$ and $f$.
Con.comapQuotientEquivOfSurjdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the preimage quotient equivalence of c and f (from the name)
English
Let $c$ be a congruence relation of $M$. Let $f$ be a monoid homomorphism of $N$ and $M$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the preimage quotient equivalence of $c$ and $f$ is a multiplicative equivalence of the set of quotients of the preimage of $\operatorname{coe}$ applied to $f$ and $c$ and the set of quotients of $c$.
Con.congrdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the congruence of e and h (from the name)
English
Let $e$ be a multiplicative equivalence of $M$ and $N$ such that $c$ is equal to the preimage of $\operatorname{coe}$ applied to $e$ and $d$. Then the congruence of $e$ and $h$ is a multiplicative equivalence of the set of quotients of $c$ and the set of quotients of $d$.
Con.ofSubmonoiddefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the congruence relation of N and H (from the docstring)
English
Let $N$ be a submonoid of $\mathrm{Prod}$ applied to $M$ and $M$ such that the function that maps $x_{1}$ and $y$ to $\MembershipmemMACRoT {N}{(\ProdmkMACRoU {x_{1}}{y})}$ is an equivalence relation. Then the congruence relation of $N$ and $H$ is a congruence relation of $M$.
Con.pidefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the product of C (from the docstring)
English
Let $C$ be a function from elements $i_{1}$ of $x$ to congruence relations of $f$ applied to $i_{1}$. Then the product of $i_{1}$ is a congruence relation of the set of functions from elements $i$ of $x$ to elements of $f$ applied to $i$.
Con.proddefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the product of c and d (from the name)
English
Let $c$ be a congruence relation of $M$. Let $d$ be a congruence relation of $N$. Then the product of $c$ and $d$ is a congruence relation of $\mathrm{Prod}$ applied to $M$ and $N$.
Con.quotientKerEquivOfRightInversedefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient kernel equivalence of f and g (from the name)
English
Let $f$ be a monoid homomorphism of $M$ and $P$. Let $g$ be a function from elements of $P$ to elements of $M$ such that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $g$ is a multiplicative equivalence of the set of quotients of the kernel of $f$ and $P$.
Con.quotientKerEquivOfSurjectivedefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient kernel equivalence of f and hf (from the name)
English
Let $f$ be a monoid homomorphism of $M$ and $P$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $\mathrm{hf}$ is a multiplicative equivalence of the set of quotients of the kernel of $f$ and $P$.
Con.quotientKerEquivRangedefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient kernel equivalence range of f (from the name)
English
Let $f$ be a monoid homomorphism of $M$ and $P$. Then the quotient kernel equivalence range of $f$ is a multiplicative equivalence of the set of quotients of the kernel of $f$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{mrange} (f)}{x_{2}})}$.
Con.quotientQuotientEquivQuotientdefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the quotient quotient equivalence quotient of c and d (from the name)
English
Let $c$ and $d$ be congruence relations of $M$ such that $c \leq d$. Then the quotient quotient equivalence quotient of $c$ and $d$ is a multiplicative equivalence of the set of quotients of the kernel of the map of $c$ and $d$ and the set of quotients of $d$.
Con.submonoiddefMathlib.GroupTheory.Congruence.Basic, function or constant
Wording
the submonoid of c (from the docstring)
English
Let $c$ be a congruence relation of $M$. Then the submonoid of $c$ is a submonoid of $\mathrm{Prod}$ applied to $M$ and $M$.

Mathlib.GroupTheory.Congruence.Defs

AddConstructureMathlib.GroupTheory.Congruence.Defs, type
Wording
additive congruence relation of M (from the name)
English
Let $M$ be a set. Then the additive congruence relations of $M$ are a basic type.
AddCon.QuotientdefMathlib.GroupTheory.Congruence.Defs, type
Wording
quotient of c (from the name)
English
Let $c$ be an additive congruence relation of $M$. Then a quotient of $c$ is an element of the function that maps $c$ to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $c$.
AddCon.comapdefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the preimage of f and c (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\EqtMACRoH {f (x_{2} + y)}{f (x_{2})+ f (y)}$. Let $c$ be an additive congruence relation of $N$. Then the preimage of $f$ and $c$ is an additive congruence relation of $M$.
AddCon.gidefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{gi}$ applied to $M$ is a Galois insertion of $\mathrm{addConGen}$ and $\operatorname{coe}$.
AddCon.hrecOn₂defMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $a$ be a quotient of $\mathrm{cM}$. Let $b$ be a quotient of $\mathrm{cN}$. Let $f$ be a function from elements $x_{4}$ of $M$ and elements $y_{1}$ of $N$ to elements of $x_{2}$ applied to the morphism into the quotient by an additive congruence relation of $x_{4}$ and the morphism into the quotient by an additive congruence relation of $y_{1}$ such that for all elements $x_{3}$ of $M$, for all elements $y$ of $N$, for all elements $\mathrm{x'}$ of $M$, for all elements $\mathrm{y'}$ of $N$, if $\mathrm{cM}$ holds for $x_{3}$ and $\mathrm{x'}$, then if $\mathrm{cN}$ holds for $y$ and $\mathrm{y'}$, then $\mathrm{HEq}$ holds for $f$ applied to $x_{3}$ and $y$ and $f$ applied to $\mathrm{x'}$ and $\mathrm{y'}$. Then $\mathrm{AddCon\_\_hrecOn\_u2082\_}$ applied to $a$, $b$, $x_{4}$, $y_{1}$, $f$ and $h$ is an element of $x_{2}$ applied to $a$ and $b$ defined as the function that maps $f$ and $h$ to $\mathrm{Quotient\_\_hrecOn\_u2082\_'}$ applied to $a$, $b$, $x_{4}$, $y_{1}$, $f$ and $h$.
AddCon.liftOndefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $q$ be a quotient of $c$. Let $f$ be a function from elements of $M$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $M$, if $c$ holds for $a$ and $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn}$ applied to $q$, $f$ and $h$ is an element of $x_{1}$ defined as $\operatorname{liftOn'}$ applied to $q$, $f$ and $h$.
AddCon.liftOnAddUnitsdefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the lift on additive unit of u and f (from the name)
English
Let $u$ be an additive unit of the set of quotients of $c$. Let $f$ be a function from elements $x_{3}$ of $M$ and elements $y_{1}$ of $M$ and elements of $\mathrm{Proof}$ applied to $c$ applied to $x_{3} + y_{1}$ and $0$ and elements of $\mathrm{Proof}$ applied to $c$ applied to $y_{1} + x_{3}$ and $0$ to elements of $x$ such that for all elements $x_{2}$ and $y$ of $M$, for all elements $\mathrm{hxy}$ of $\mathrm{Proof}$ applied to $c$ applied to $x_{2} + y$ and $0$, for all elements $\mathrm{hyx}$ of $\mathrm{Proof}$ applied to $c$ applied to $y + x_{2}$ and $0$, for all elements $\mathrm{x'}$ and $\mathrm{y'}$ of $M$, for all elements $\mathrm{hxy'}$ of $\mathrm{Proof}$ applied to $c$ applied to $\mathrm{x'} + \mathrm{y'}$ and $0$, for all elements $\mathrm{hyx'}$ of $\mathrm{Proof}$ applied to $c$ applied to $\mathrm{y'} + \mathrm{x'}$ and $0$, if $c$ holds for $x_{2}$ and $\mathrm{x'}$, then if $c$ holds for $y$ and $\mathrm{y'}$, then $\EqtMACRoH {f (x_{2} , y , \mathrm{hxy} , \mathrm{hyx})}{f (\mathrm{x'} , \mathrm{y'} , \mathrm{hxy'} , \mathrm{hyx'})}$. Then the lift on additive unit of $u$ and $x_{3}$ is an element of $x$.
AddCon.liftOn₂defMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $q$ and $r$ be quotients of $c$. Let $f$ be a function from elements of $M$ and elements of $M$ to elements of $x_{1}$ such that for all elements $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ of $M$, if $c$ holds for $x_{2}$ and $x_{4}$, then if $c$ holds for $x_{3}$ and $x_{5}$, then $\EqtMACRoH {f (x_{2} , x_{3})}{f (x_{4} , x_{5})}$. Then $\mathrm{AddCon\_\_liftOn\_u2082\_}$ applied to $q$, $r$, $f$ and $h$ is an element of $x_{1}$ defined as $\mathrm{Quotient\_\_liftOn\_u2082\_'}$ applied to $q$, $r$, $f$ and $h$.
AddCon.toQuotientdefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the morphism into the quotient by an additive congruence relation of x1 (from the docstring)
English
Let $x_{1}$ be an element of $M$. Then the morphism into the quotient by an additive congruence relation of $x_{1}$ is a quotient of $c$ defined as $\operatorname{mk''}$ applied to $x_{1}$.
AddConGen.RelinductiveMathlib.GroupTheory.Congruence.Defs, predicate
Wording
no wording
English
Let $r$ be a function from elements of $M$ and elements of $M$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $M$. Then we can say that $\operatorname{Rel}$ holds for $r$, $x_{1}$ and $x_{2}$.
AddConGen.Rel.belowinductiveMathlib.GroupTheory.Congruence.Defs, predicate
Wording
no wording
English
Assume that $\operatorname{Rel}$ holds for $r$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
ConstructureMathlib.GroupTheory.Congruence.Defs, type
Wording
congruence relation of M (from the name)
English
Let $M$ be a set. Then the congruence relations of $M$ are a basic type.
Con.QuotientdefMathlib.GroupTheory.Congruence.Defs, type
Wording
quotient of c (from the name)
English
Let $c$ be a congruence relation of $M$. Then a quotient of $c$ is an element of the function that maps $c$ to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $c$.
Con.comapdefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the preimage of f and c (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$ such that for all elements $x_{2}$ and $y$ of $M$, $\EqtMACRoH {f (x_{2} \times y)}{f (x_{2})\times f (y)}$. Let $c$ be a congruence relation of $N$. Then the preimage of $f$ and $c$ is a congruence relation of $M$.
Con.gidefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{gi}$ applied to $M$ is a Galois insertion of $\mathrm{conGen}$ and $\operatorname{coe}$.
Con.hrecOn₂defMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $a$ be a quotient of $\mathrm{cM}$. Let $b$ be a quotient of $\mathrm{cN}$. Let $f$ be a function from elements $x_{4}$ of $M$ and elements $y_{1}$ of $N$ to elements of $x_{2}$ applied to the morphism into the quotient by a congruence relation of $x_{4}$ and the morphism into the quotient by a congruence relation of $y_{1}$ such that for all elements $x_{3}$ of $M$, for all elements $y$ of $N$, for all elements $\mathrm{x'}$ of $M$, for all elements $\mathrm{y'}$ of $N$, if $\mathrm{cM}$ holds for $x_{3}$ and $\mathrm{x'}$, then if $\mathrm{cN}$ holds for $y$ and $\mathrm{y'}$, then $\mathrm{HEq}$ holds for $f$ applied to $x_{3}$ and $y$ and $f$ applied to $\mathrm{x'}$ and $\mathrm{y'}$. Then $\mathrm{Con\_\_hrecOn\_u2082\_}$ applied to $a$, $b$, $x_{4}$, $y_{1}$, $f$ and $h$ is an element of $x_{2}$ applied to $a$ and $b$ defined as the function that maps $f$ and $h$ to $\mathrm{Quotient\_\_hrecOn\_u2082\_'}$ applied to $a$, $b$, $x_{4}$, $y_{1}$, $f$ and $h$.
Con.liftOndefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $q$ be a quotient of $c$. Let $f$ be a function from elements of $M$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $M$, if $c$ holds for $a$ and $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn}$ applied to $q$, $f$ and $h$ is an element of $x_{1}$ defined as $\operatorname{liftOn'}$ applied to $q$, $f$ and $h$.
Con.liftOnUnitsdefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the lift on unit of u and f (from the name)
English
Let $u$ be a unit of the set of quotients of $c$. Let $f$ be a function from elements $x_{3}$ of $M$ and elements $y_{1}$ of $M$ and elements of $\mathrm{Proof}$ applied to $c$ applied to $x_{3} \times y_{1}$ and $1$ and elements of $\mathrm{Proof}$ applied to $c$ applied to $y_{1} \times x_{3}$ and $1$ to elements of $x$ such that for all elements $x_{2}$ and $y$ of $M$, for all elements $\mathrm{hxy}$ of $\mathrm{Proof}$ applied to $c$ applied to $x_{2} \times y$ and $1$, for all elements $\mathrm{hyx}$ of $\mathrm{Proof}$ applied to $c$ applied to $y \times x_{2}$ and $1$, for all elements $\mathrm{x'}$ and $\mathrm{y'}$ of $M$, for all elements $\mathrm{hxy'}$ of $\mathrm{Proof}$ applied to $c$ applied to $\mathrm{x'} \times \mathrm{y'}$ and $1$, for all elements $\mathrm{hyx'}$ of $\mathrm{Proof}$ applied to $c$ applied to $\mathrm{y'} \times \mathrm{x'}$ and $1$, if $c$ holds for $x_{2}$ and $\mathrm{x'}$, then if $c$ holds for $y$ and $\mathrm{y'}$, then $\EqtMACRoH {f (x_{2} , y , \mathrm{hxy} , \mathrm{hyx})}{f (\mathrm{x'} , \mathrm{y'} , \mathrm{hxy'} , \mathrm{hyx'})}$. Then the lift on unit of $u$ and $x_{3}$ is an element of $x$.
Con.liftOn₂defMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
no wording
English
Let $q$ and $r$ be quotients of $c$. Let $f$ be a function from elements of $M$ and elements of $M$ to elements of $x_{1}$ such that for all elements $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ of $M$, if $c$ holds for $x_{2}$ and $x_{4}$, then if $c$ holds for $x_{3}$ and $x_{5}$, then $\EqtMACRoH {f (x_{2} , x_{3})}{f (x_{4} , x_{5})}$. Then $\mathrm{Con\_\_liftOn\_u2082\_}$ applied to $q$, $r$, $f$ and $h$ is an element of $x_{1}$ defined as $\mathrm{Quotient\_\_liftOn\_u2082\_'}$ applied to $q$, $r$, $f$ and $h$.
Con.toQuotientdefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the morphism into the quotient by a congruence relation of x1 (from the docstring)
English
Let $x_{1}$ be an element of $M$. Then the morphism into the quotient by a congruence relation of $x_{1}$ is a quotient of $c$ defined as $\operatorname{mk''}$ applied to $x_{1}$.
ConGen.RelinductiveMathlib.GroupTheory.Congruence.Defs, predicate
Wording
no wording
English
Let $r$ be a function from elements of $M$ and elements of $M$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $M$. Then we can say that $\operatorname{Rel}$ holds for $r$, $x_{1}$ and $x_{2}$.
ConGen.Rel.belowinductiveMathlib.GroupTheory.Congruence.Defs, predicate
Wording
no wording
English
Assume that $\operatorname{Rel}$ holds for $r$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
addConGendefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the additive congruence relation generator of r (from the name)
English
Let $r$ be a function from elements of $M$ and elements of $M$ to propositions. Then the additive congruence relation generator of $r$ is an additive congruence relation of $M$.
conGendefMathlib.GroupTheory.Congruence.Defs, function or constant
Wording
the congruence relation generator of r (from the name)
English
Let $r$ be a function from elements of $M$ and elements of $M$ to propositions. Then the congruence relation generator of $r$ is a congruence relation of $M$.

Mathlib.GroupTheory.Congruence.Hom

AddCon.correspondencedefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the correspondence (from the name)
English
The correspondence is an order isomorphism of $\SubtypeSet {d}{\mathrm{Leq} (c , d)}$ and the set of additive congruence relations of the set of quotients of $c$.
AddCon.kerdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the kernel of f (from the docstring)
English
Let $f$ be an element of $F$. Then the kernel of $f$ is an additive congruence relation of $M$.
AddCon.kerLiftdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the kernel lift of f (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $P$. Then the kernel lift of $f$ is an additive monoid homomorphism of the set of quotients of the kernel of $f$ and $P$.
AddCon.liftdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the lift of c and f (from the name)
English
Let $c$ be an additive congruence relation of $M$. Let $f$ be an additive monoid homomorphism of $M$ and $P$ such that $c$ is less than or equal to the kernel of $f$. Then the lift of $c$ and $f$ is an additive monoid homomorphism of the set of quotients of $c$ and $P$.
AddCon.mapdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the map of c and d (from the name)
English
Let $c$ and $d$ be additive congruence relations of $M$ such that $c \leq d$. Then the map of $c$ and $d$ is an additive monoid homomorphism of the set of quotients of $c$ and the set of quotients of $d$.
AddCon.mapGendefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the map generator of f (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$. Then the map generator of $f$ is an additive congruence relation of $N$ defined as the additive congruence relation generator of $\operatorname{Map}$ applied to $\operatorname{coe}$ applied to $c$, $f$ and $f$.
AddCon.mapOfSurjectivedefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the map of f (from the name)
English
Let $f$ be an element of $F$ such that the kernel of $f$ is less than or equal to $c$ and $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the map of $f$ is an additive congruence relation of $N$.
AddCon.mk'defMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
no wording
English
Let $c$ be an additive congruence relation of $M$. Then $\operatorname{mk'}$ applied to $c$ is an additive monoid homomorphism of $M$ and the set of quotients of $c$.
AddCon.mkAddHomdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the additive homomorphism of c (from the name)
English
Let $c$ be an additive congruence relation of $M$. Then the additive homomorphism of $c$ is an additive homomorphism of $M$ and the set of quotients of $c$.
Con.correspondencedefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the correspondence (from the name)
English
The correspondence is an order isomorphism of $\SubtypeSet {d}{\mathrm{Leq} (c , d)}$ and the set of congruence relations of the set of quotients of $c$.
Con.kerdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the kernel of f (from the docstring)
English
Let $f$ be an element of $F$. Then the kernel of $f$ is a congruence relation of $M$.
Con.kerLiftdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the kernel lift of f (from the name)
English
Let $f$ be a monoid homomorphism of $M$ and $P$. Then the kernel lift of $f$ is a monoid homomorphism of the set of quotients of the kernel of $f$ and $P$.
Con.liftdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the lift of c and f (from the name)
English
Let $c$ be a congruence relation of $M$. Let $f$ be a monoid homomorphism of $M$ and $P$ such that $c$ is less than or equal to the kernel of $f$. Then the lift of $c$ and $f$ is a monoid homomorphism of the set of quotients of $c$ and $P$.
Con.mapdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the map of c and d (from the name)
English
Let $c$ and $d$ be congruence relations of $M$ such that $c \leq d$. Then the map of $c$ and $d$ is a monoid homomorphism of the set of quotients of $c$ and the set of quotients of $d$.
Con.mapGendefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the map generator of f (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$. Then the map generator of $f$ is a congruence relation of $N$ defined as the congruence relation generator of $\operatorname{Map}$ applied to $\operatorname{coe}$ applied to $c$, $f$ and $f$.
Con.mapOfSurjectivedefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the map of f (from the name)
English
Let $f$ be an element of $F$ such that the kernel of $f$ is less than or equal to $c$ and $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the map of $f$ is a congruence relation of $N$.
Con.mk'defMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
no wording
English
Let $c$ be a congruence relation of $M$. Then $\operatorname{mk'}$ applied to $c$ is a monoid homomorphism of $M$ and the set of quotients of $c$.
Con.mkMulHomdefMathlib.GroupTheory.Congruence.Hom, function or constant
Wording
the multiplicative homomorphism of c (from the name)
English
Let $c$ be a congruence relation of $M$. Then the multiplicative homomorphism of $c$ is a multiplicative homomorphism of $M$ and the set of quotients of $c$.

Mathlib.GroupTheory.Congruence.Opposite

AddCon.opdefMathlib.GroupTheory.Congruence.Opposite, function or constant
Wording
the opposite of c (from the name)
English
Let $c$ be an additive congruence relation of $M$. Then the opposite of $c$ is an additive congruence relation of the set of additive opposites of $M$.
AddCon.orderIsoOpdefMathlib.GroupTheory.Congruence.Opposite, function or constant
Wording
the order isomorphism opposite (from the name)
English
The order isomorphism opposite is an order isomorphism of the set of additive congruence relations of $M$ and the set of additive congruence relations of the set of additive opposites of $M$.
AddCon.unopdefMathlib.GroupTheory.Congruence.Opposite, function or constant
Wording
the opposite of c (from the name)
English
Let $c$ be an additive congruence relation of the set of additive opposites of $M$. Then the opposite of $c$ is an additive congruence relation of $M$.
Con.opdefMathlib.GroupTheory.Congruence.Opposite, function or constant
Wording
the opposite of c (from the name)
English
Let $c$ be a congruence relation of $M$. Then the opposite of $c$ is a congruence relation of the set of multiplicative opposites of $M$.
Con.orderIsoOpdefMathlib.GroupTheory.Congruence.Opposite, function or constant
Wording
the order isomorphism opposite (from the name)
English
The order isomorphism opposite is an order isomorphism of the set of congruence relations of $M$ and the set of congruence relations of the set of multiplicative opposites of $M$.
Con.unopdefMathlib.GroupTheory.Congruence.Opposite, function or constant
Wording
the opposite of c (from the name)
English
Let $c$ be a congruence relation of the set of multiplicative opposites of $M$. Then the opposite of $c$ is a congruence relation of $M$.

Mathlib.GroupTheory.Coprod.Basic

AddEquiv.coprodAssocdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct associator of N and P (from the name)
English
Let $M$, $N$ and $P$ be sets. Then the coproduct associator of $N$ and $P$ is an additive equivalence of the set of coproducts of the set of coproducts of $M$ and $N$ and $P$ and the set of coproducts of $M$ and the set of coproducts of $N$ and $P$.
AddEquiv.coprodCommdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
Let $M$ and $N$ be sets. Then $\operatorname{coprodComm}$ applied to $M$ and $N$ is an additive equivalence of the set of coproducts of $M$ and $N$ and the set of coproducts of $N$ and $M$ defined as the additive equivalence of the swap of $M$ and $N$ and the swap of $N$ and $M$.
AddEquiv.coprodCongrdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct congruence of e and #2 (from the name)
English
Let $e$ be an additive equivalence of $M$ and $N$. Let $\mathrm{e'}$ be an additive equivalence of $\mathrm{M'}$ and $\mathrm{N'}$. Then the coproduct congruence of $e$ and $\mathrm{e'}$ is an additive equivalence of the set of coproducts of $M$ and $\mathrm{M'}$ and the set of coproducts of $N$ and $\mathrm{N'}$.
AddEquiv.coprodPUnitdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct unit of M (from the name)
English
Let $M$ be a set. Then the coproduct unit of $M$ is an additive equivalence of the set of coproducts of $M$ and $\mathrm{PUnit}$ and $M$.
AddEquiv.punitCoproddefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{punitCoprod}$ applied to $M$ is an additive equivalence of the set of coproducts of $\mathrm{PUnit}$ and $M$ and $M$.
AddMonoid.CoproddefMathlib.GroupTheory.Coprod.Basic, type
Wording
coproduct of M and N (from the name)
English
Let $M$ and $N$ be sets. Then a coproduct of $M$ and $N$ is an element of the function that maps $M$ and $N$ to the set of quotients of the coproduct congruence relation of $M$ and $N$.
AddMonoid.Coprod.cliftdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
Let $f$ be an additive monoid homomorphism of the set of free additive monoids of $\mathrm{Sum}$ applied to $M$ and $N$ and $P$ such that $\EqtMACRoH {f (\operatorname{of} (\operatorname{inl} (0)))}{0}$, $\EqtMACRoH {f (\operatorname{of} (\operatorname{inr} (0)))}{0}$, for all elements $x_{4}$ of $M$, for all elements $y_{1}$ of $M$, $\EqtMACRoH {f (\operatorname{of} (\operatorname{inl} (x_{4} + y_{1})))}{f (\operatorname{of} (\operatorname{inl} (x_{4}))+ \operatorname{of} (\operatorname{inl} (y_{1})))}$ and for all elements $x_{3}$ of $N$, for all elements $y$ of $N$, $\EqtMACRoH {f (\operatorname{of} (\operatorname{inr} (x_{3} + y)))}{f (\operatorname{of} (\operatorname{inr} (x_{3}))+ \operatorname{of} (\operatorname{inr} (y)))}$. Then $\operatorname{clift}$ applied to $f$, $h$, $h_{1}$, $\mathrm{hM}$ and $\mathrm{hN}$ is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and $P$.
AddMonoid.Coprod.fstdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the first component (from the name)
English
The first component is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and $M$ defined as the lift of the identity map of $M$ and $0$.
AddMonoid.Coprod.inldefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the left injection (from the name)
English
The left injection is an additive monoid homomorphism of $M$ and the set of coproducts of $M$ and $N$.
AddMonoid.Coprod.inrdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the right injection (from the name)
English
The right injection is an additive monoid homomorphism of $N$ and the set of coproducts of $M$ and $N$.
AddMonoid.Coprod.liftdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the lift of f and g (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $P$. Let $g$ be an additive monoid homomorphism of $N$ and $P$. Then the lift of $f$ and $g$ is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and $P$.
AddMonoid.Coprod.liftEquivdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the lift equivalence (from the name)
English
The lift equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of additive monoid homomorphisms of $M$ and $P$ and the set of additive monoid homomorphisms of $N$ and $P$ to the set of additive monoid homomorphisms of the set of coproducts of $M$ and $N$ and $P$.
AddMonoid.Coprod.mapdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the map of f and g (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $\mathrm{M'}$. Let $g$ be an additive monoid homomorphism of $N$ and $\mathrm{N'}$. Then the map of $f$ and $g$ is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and the set of coproducts of $\mathrm{M'}$ and $\mathrm{N'}$.
AddMonoid.Coprod.mkdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
$\operatorname{mk}$ is an additive monoid homomorphism of the set of free additive monoids of $\mathrm{Sum}$ applied to $M$ and $N$ and the set of coproducts of $M$ and $N$ defined as $\operatorname{mk'}$ applied to the coproduct congruence relation of $M$ and $N$.
AddMonoid.Coprod.snddefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the second component (from the name)
English
The second component is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and $N$ defined as the lift of $0$ and the identity map of $N$.
AddMonoid.Coprod.swapdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the swap of M and N (from the name)
English
Let $M$ and $N$ be sets. Then the swap of $M$ and $N$ is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and the set of coproducts of $N$ and $M$.
AddMonoid.Coprod.toProddefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the product (from the name)
English
The product is an additive monoid homomorphism of the set of coproducts of $M$ and $N$ and $\mathrm{Prod}$ applied to $M$ and $N$ defined as the lift of the left injection of $M$ and $N$ and the right injection of $M$ and $N$.
AddMonoid.coprodCondefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct congruence relation of M and N (from the name)
English
Let $M$ and $N$ be sets. Then the coproduct congruence relation of $M$ and $N$ is an additive congruence relation of the set of free additive monoids of $\mathrm{Sum}$ applied to $M$ and $N$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that for all elements $x_{2}$ of $M$, for all elements $y$ of $M$, $c$ holds for $\operatorname{of}$ applied to $\operatorname{inl}$ applied to $x_{2} + y$ and $\operatorname{of} (\operatorname{inl} (x_{2}))+ \operatorname{of} (\operatorname{inl} (y))$, for all elements $x_{3}$ of $N$, for all elements $y_{1}$ of $N$, $c$ holds for $\operatorname{of}$ applied to $\operatorname{inr}$ applied to $x_{3} + y_{1}$ and $\operatorname{of} (\operatorname{inr} (x_{3}))+ \operatorname{of} (\operatorname{inr} (y_{1}))$, $c$ holds for $\operatorname{of}$ applied to $\operatorname{inl}$ applied to $0$ and $0$ and $c$ holds for $\operatorname{of}$ applied to $\operatorname{inr}$ applied to $0$ and $0$.
Monoid.CoproddefMathlib.GroupTheory.Coprod.Basic, type
Wording
coproduct of M and N (from the name)
English
Let $M$ and $N$ be sets. Then a coproduct of $M$ and $N$ is an element of the function that maps $M$ and $N$ to the set of quotients of the coproduct congruence relation of $M$ and $N$.
Monoid.Coprod.cliftdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
Let $f$ be a monoid homomorphism of the set of free monoids of $\mathrm{Sum}$ applied to $M$ and $N$ and $P$ such that $\EqtMACRoH {f (\operatorname{of} (\operatorname{inl} (1)))}{1}$, $\EqtMACRoH {f (\operatorname{of} (\operatorname{inr} (1)))}{1}$, for all elements $x_{4}$ of $M$, for all elements $y_{1}$ of $M$, $\EqtMACRoH {f (\operatorname{of} (\operatorname{inl} (x_{4} \times y_{1})))}{f (\operatorname{of} (\operatorname{inl} (x_{4}))\times \operatorname{of} (\operatorname{inl} (y_{1})))}$ and for all elements $x_{3}$ of $N$, for all elements $y$ of $N$, $\EqtMACRoH {f (\operatorname{of} (\operatorname{inr} (x_{3} \times y)))}{f (\operatorname{of} (\operatorname{inr} (x_{3}))\times \operatorname{of} (\operatorname{inr} (y)))}$. Then $\operatorname{clift}$ applied to $f$, $h$, $h_{1}$, $\mathrm{hM}$ and $\mathrm{hN}$ is a monoid homomorphism of the set of coproducts of $M$ and $N$ and $P$.
Monoid.Coprod.fstdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the first component (from the name)
English
The first component is a monoid homomorphism of the set of coproducts of $M$ and $N$ and $M$ defined as the lift of the identity map of $M$ and $1$.
Monoid.Coprod.inldefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the left injection (from the name)
English
The left injection is a monoid homomorphism of $M$ and the set of coproducts of $M$ and $N$.
Monoid.Coprod.inrdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the right injection (from the name)
English
The right injection is a monoid homomorphism of $N$ and the set of coproducts of $M$ and $N$.
Monoid.Coprod.liftdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the lift of f and g (from the name)
English
Let $f$ be a monoid homomorphism of $M$ and $P$. Let $g$ be a monoid homomorphism of $N$ and $P$. Then the lift of $f$ and $g$ is a monoid homomorphism of the set of coproducts of $M$ and $N$ and $P$.
Monoid.Coprod.liftEquivdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the lift equivalence (from the name)
English
The lift equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of monoid homomorphisms of $M$ and $P$ and the set of monoid homomorphisms of $N$ and $P$ to the set of monoid homomorphisms of the set of coproducts of $M$ and $N$ and $P$.
Monoid.Coprod.mapdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the map of f and g (from the name)
English
Let $f$ be a monoid homomorphism of $M$ and $\mathrm{M'}$. Let $g$ be a monoid homomorphism of $N$ and $\mathrm{N'}$. Then the map of $f$ and $g$ is a monoid homomorphism of the set of coproducts of $M$ and $N$ and the set of coproducts of $\mathrm{M'}$ and $\mathrm{N'}$.
Monoid.Coprod.mkdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
$\operatorname{mk}$ is a monoid homomorphism of the set of free monoids of $\mathrm{Sum}$ applied to $M$ and $N$ and the set of coproducts of $M$ and $N$ defined as $\operatorname{mk'}$ applied to the coproduct congruence relation of $M$ and $N$.
Monoid.Coprod.snddefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the second component (from the name)
English
The second component is a monoid homomorphism of the set of coproducts of $M$ and $N$ and $N$ defined as the lift of $1$ and the identity map of $N$.
Monoid.Coprod.swapdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the swap of M and N (from the name)
English
Let $M$ and $N$ be sets. Then the swap of $M$ and $N$ is a monoid homomorphism of the set of coproducts of $M$ and $N$ and the set of coproducts of $N$ and $M$.
Monoid.Coprod.toProddefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the product (from the name)
English
The product is a monoid homomorphism of the set of coproducts of $M$ and $N$ and $\mathrm{Prod}$ applied to $M$ and $N$ defined as the lift of the left injection of $M$ and $N$ and the right injection of $M$ and $N$.
Monoid.coprodCondefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct congruence relation of M and N (from the name)
English
Let $M$ and $N$ be sets. Then the coproduct congruence relation of $M$ and $N$ is a congruence relation of the set of free monoids of $\mathrm{Sum}$ applied to $M$ and $N$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that for all elements $x_{2}$ of $M$, for all elements $y$ of $M$, $c$ holds for $\operatorname{of}$ applied to $\operatorname{inl}$ applied to $x_{2} \times y$ and $\operatorname{of} (\operatorname{inl} (x_{2}))\times \operatorname{of} (\operatorname{inl} (y))$, for all elements $x_{3}$ of $N$, for all elements $y_{1}$ of $N$, $c$ holds for $\operatorname{of}$ applied to $\operatorname{inr}$ applied to $x_{3} \times y_{1}$ and $\operatorname{of} (\operatorname{inr} (x_{3}))\times \operatorname{of} (\operatorname{inr} (y_{1}))$, $c$ holds for $\operatorname{of}$ applied to $\operatorname{inl}$ applied to $1$ and $1$ and $c$ holds for $\operatorname{of}$ applied to $\operatorname{inr}$ applied to $1$ and $1$.
MulEquiv.coprodAssocdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct associator of N and P (from the name)
English
Let $M$, $N$ and $P$ be sets. Then the coproduct associator of $N$ and $P$ is a multiplicative equivalence of the set of coproducts of the set of coproducts of $M$ and $N$ and $P$ and the set of coproducts of $M$ and the set of coproducts of $N$ and $P$.
MulEquiv.coprodCommdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
Let $M$ and $N$ be sets. Then $\operatorname{coprodComm}$ applied to $M$ and $N$ is a multiplicative equivalence of the set of coproducts of $M$ and $N$ and the set of coproducts of $N$ and $M$ defined as the multiplicative equivalence of the swap of $M$ and $N$ and the swap of $N$ and $M$.
MulEquiv.coprodCongrdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct congruence of e and #2 (from the name)
English
Let $e$ be a multiplicative equivalence of $M$ and $N$. Let $\mathrm{e'}$ be a multiplicative equivalence of $\mathrm{M'}$ and $\mathrm{N'}$. Then the coproduct congruence of $e$ and $\mathrm{e'}$ is a multiplicative equivalence of the set of coproducts of $M$ and $\mathrm{M'}$ and the set of coproducts of $N$ and $\mathrm{N'}$.
MulEquiv.coprodPUnitdefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
the coproduct unit of M (from the name)
English
Let $M$ be a set. Then the coproduct unit of $M$ is a multiplicative equivalence of the set of coproducts of $M$ and $\mathrm{PUnit}$ and $M$.
MulEquiv.punitCoproddefMathlib.GroupTheory.Coprod.Basic, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{punitCoprod}$ applied to $M$ is a multiplicative equivalence of the set of coproducts of $\mathrm{PUnit}$ and $M$ and $M$.

Mathlib.GroupTheory.CoprodI

Monoid.CoprodIdefMathlib.GroupTheory.CoprodI, type
Wording
coproduct of M (from the name)
English
Let $M$ be a function from elements of $x$ to sets. Then a coproduct of $M$ is an element of the function that maps $M$ to the set of quotients of the congruence relation generator of $\operatorname{Rel}$ applied to $M$.
Monoid.CoprodI.FreeGroupBasis.coprodIdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the coproduct of B (from the name)
English
Let $B$ be a function from elements $i_{1}$ of $x$ to free group bases of $X$ applied to $i_{1}$ and $G$ applied to $i_{1}$. Then the coproduct of $i_{1}$ is a free group basis of $\Sigma$ applied to the function that maps $i$ to $X$ applied to $i$ and the set of coproducts of $G$.
Monoid.CoprodI.NeWordinductiveMathlib.GroupTheory.CoprodI, type
Wording
no wording
English
Let $M$ be a function from elements of $x$ to sets. Let $x_{2}$ and $x_{3}$ be elements of $x$. Then the elements of $\operatorname{NeWord}$ applied to $M$, $x_{2}$ and $x_{3}$ are a basic type.
Monoid.CoprodI.NeWord.appendconstructorMathlib.GroupTheory.CoprodI, function or constant
Wording
no wording
English
Let $x_{2}$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Assume that $j \neq k$. Let $x_{3}$ be an element of $\operatorname{NeWord}$ applied to $M$, $k$ and $l$. Then $\operatorname{append}$ applied to $x_{2}$, $\mathrm{\_hne}$ and $x_{3}$ is an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $l$.
Monoid.CoprodI.NeWord.ctorElimTypedefMathlib.GroupTheory.CoprodI, 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 $i$ of $x$ and elements $x_{2}$ of $M$ applied to $i$ and elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (x_{2} , 1)$ to elements of $\mathrm{motive}$ applied to $i$, $i$ and the singleton of $x_{2}$ and $h$ and $\mathrm{PULift}$ applied to the set of functions from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements $k$ of $x$ and elements $l$ of $x$ and elements $x_{3}$ of $\operatorname{NeWord}$ applied to $M$, $i_{1}$ and $j$ and elements $\mathrm{\_hne}$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (j , k)$ and elements $x_{4}$ of $\operatorname{NeWord}$ applied to $M$, $k$ and $l$ to elements of $\mathrm{motive}$ applied to $i_{1}$, $l$ and $\operatorname{append}$ applied to $x_{3}$, $\mathrm{\_hne}$ and $x_{4}$.
Monoid.CoprodI.NeWord.headdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the head of _w (from the name)
English
Let $\mathrm{\_w}$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Then the head of $\mathrm{\_w}$ is an element of $M$ applied to $i$ defined as $\operatorname{brecOn}$ applied to $\mathrm{\_w}$ and $\mathrm{Monoid\_\_CoprodI\_\_NeWord\_\_head\_\_\_f}$.
Monoid.CoprodI.NeWord.invdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the inverse of _w (from the docstring)
English
Let $\mathrm{\_w}$ be an element of $\operatorname{NeWord}$ applied to $G$, $i$ and $j$. Then the inverse of $\mathrm{\_w}$ is an element of $\operatorname{NeWord}$ applied to $G$, $j$ and $i$ defined as $\operatorname{brecOn}$ applied to $\mathrm{\_w}$ and $\mathrm{Monoid\_\_CoprodI\_\_NeWord\_\_inv\_\_\_f}$.
Monoid.CoprodI.NeWord.lastdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the last letter of _w (from the docstring)
English
Let $\mathrm{\_w}$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Then the last letter of $\mathrm{\_w}$ is an element of $M$ applied to $j$ defined as $\operatorname{brecOn}$ applied to $\mathrm{\_w}$ and $\mathrm{Monoid\_\_CoprodI\_\_NeWord\_\_last\_\_\_f}$.
Monoid.CoprodI.NeWord.mulHeaddefMathlib.GroupTheory.CoprodI, function or constant
Wording
the multiplicative head of w and x2 (from the name)
English
Let $w$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Let $x_{2}$ be an element of $M$ applied to $i$ such that the product of $x_{2}$ and the head of $w$ is distinct from $1$. Then the multiplicative head of $w$ and $x_{2}$ is an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$ defined as $\operatorname{replaceHead}$ applied to the product of $x_{2}$ and the head of $w$, $\mathrm{hnotone}$ and $w$.
Monoid.CoprodI.NeWord.proddefMathlib.GroupTheory.CoprodI, function or constant
Wording
the product of w (from the name)
English
Let $w$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Then the product of $w$ is a coproduct of $M$ defined as the product of the word of $w$.
Monoid.CoprodI.NeWord.replaceHeaddefMathlib.GroupTheory.CoprodI, function or constant
Wording
no wording
English
Let $x_{2}$ be an element of $M$ applied to $i$ such that $x_{2} \neq 1$. Let $\mathrm{\_w}$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Then $\operatorname{replaceHead}$ applied to $x_{2}$, $\mathrm{\_hnotone}$ and $\mathrm{\_w}$ is an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$ defined as $\operatorname{brecOn}$ applied to $\mathrm{\_w}$, $\mathrm{Monoid\_\_CoprodI\_\_NeWord\_\_replaceHead\_\_\_f}$, $x_{2}$ and $\mathrm{\_hnotone}$.
Monoid.CoprodI.NeWord.singletonconstructorMathlib.GroupTheory.CoprodI, function or constant
Wording
the singleton of x2 and h (from the name)
English
Let $x_{2}$ be an element of $M$ applied to $i$ such that $x_{2} \neq 1$. Then the singleton of $x_{2}$ and $h$ is an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $i$.
Monoid.CoprodI.NeWord.toListdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the list of _w (from the name)
English
Let $\mathrm{\_w}$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Then the list of $\mathrm{\_w}$ is a list of elements of $\Sigma$ applied to the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as $\operatorname{brecOn}$ applied to $\mathrm{\_w}$ and $\mathrm{Monoid\_\_CoprodI\_\_NeWord\_\_toList\_\_\_f}$.
Monoid.CoprodI.NeWord.toWorddefMathlib.GroupTheory.CoprodI, function or constant
Wording
the word of w (from the name)
English
Let $w$ be an element of $\operatorname{NeWord}$ applied to $M$, $i$ and $j$. Then the word of $w$ is a word of $M$.
Monoid.CoprodI.RelinductiveMathlib.GroupTheory.CoprodI, predicate
Wording
no wording
English
Let $M$ be a function from elements of $x$ to sets. Let $x_{2}$ be a free monoid of $\Sigma$ applied to the function that maps $i_{1}$ to $M$ applied to $i_{1}$. Let $x_{3}$ be a free monoid of $\Sigma$ applied to the function that maps $i$ to $M$ applied to $i$. Then we can say that $\operatorname{Rel}$ holds for $M$, $x_{2}$ and $x_{3}$.
Monoid.CoprodI.WordstructureMathlib.GroupTheory.CoprodI, type
Wording
word of M (from the name)
English
Let $M$ be a function from elements of $x$ to sets. Then the words of $M$ are a basic type.
Monoid.CoprodI.Word.PairstructureMathlib.GroupTheory.CoprodI, type
Wording
pair of M and i (from the name)
English
Let $M$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then the pairs of $M$ and $i$ are a basic type.
Monoid.CoprodI.Word.Pair.headdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the head of self (from the name)
English
Let $\mathrm{self}$ be a pair of $M$ and $i$. Then the head of $\mathrm{self}$ is an element of $M$ applied to $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Monoid.CoprodI.Word.Pair.taildefMathlib.GroupTheory.CoprodI, function or constant
Wording
the tail of self (from the name)
English
Let $\mathrm{self}$ be a pair of $M$ and $i$. Then the tail of $\mathrm{self}$ is a word of $M$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Monoid.CoprodI.Word.consdefMathlib.GroupTheory.CoprodI, function or constant
Wording
no wording
English
Let $m$ be an element of $M$ applied to $i$. Let $w$ be a word of $M$ such that the first component index of $w$ is distinct from $\operatorname{some}$ applied to $i$. Assume that $m \neq 1$. Then $\operatorname{cons}$ applied to $m$, $w$, $\mathrm{hmw}$ and $h_{1}$ is a word of $M$.
Monoid.CoprodI.Word.consRecOndefMathlib.GroupTheory.CoprodI, function or constant
Wording
no wording
English
Let $w$ be a word of $M$. Let $\mathrm{empty}$ be an element of $\mathrm{motive}$ applied to the empty reduced word. Let $\mathrm{cons}$ be a function from elements $i$ of $x$ and elements $m$ of $M$ applied to $i$ and words $w_{1}$ of $M$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that the first component index of $w_{1}$ is distinct from $\operatorname{some}$ applied to $i$ and elements $h_{2}$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (m , 1)$ and elements of $\mathrm{motive}$ applied to $w_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $m$, $w_{1}$, $h_{1}$ and $h_{2}$. Then $\operatorname{consRecOn}$ applied to $w$, $\mathrm{empty}$, $i$, $m$, $w_{1}$, $h_{1}$, $h_{2}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $w$.
Monoid.CoprodI.Word.emptydefMathlib.GroupTheory.CoprodI, function or constant
Wording
the empty reduced word (from the docstring)
English
The empty reduced word is a word of $M$.
Monoid.CoprodI.Word.equivdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the equivalence (from the name)
English
The equivalence is an equivalence from the set of coproducts of $M$ to the set of words of $M$.
Monoid.CoprodI.Word.equivPairdefMathlib.GroupTheory.CoprodI, 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 words of $M$ to the set of pairs of $M$ and $i$.
Monoid.CoprodI.Word.fstIdxdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the first component index of w (from the name)
English
Let $w$ be a word of $M$. Then the first component index of $w$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{map}$ applied to $\operatorname{fst}$ and $\mathrm{List\_\_head?}$ applied to the list of $w$.
Monoid.CoprodI.Word.proddefMathlib.GroupTheory.CoprodI, function or constant
Wording
the product of w (from the name)
English
Let $w$ be a word of $M$. Then the product of $w$ is a coproduct of $M$ defined as $\operatorname{prod}$ applied to $\operatorname{map}$ applied to the function that maps $l$ to $\operatorname{of}$ applied to $\operatorname{snd}$ applied to $l$ and the list of $w$.
Monoid.CoprodI.Word.rconsdefMathlib.GroupTheory.CoprodI, function or constant
Wording
no wording
English
Let $p$ be a pair of $M$ and $i$. Then $\operatorname{rcons}$ applied to $p$ is a word of $M$ defined as $\mathrm{dite}$ applied to the proposition that the head of $p$ is equal to $1$, the function that maps $h$ to the tail of $p$ and the function that maps $h_{1}$ to $\operatorname{cons}$ applied to the head of $p$, the tail of $p$, $\mathrm{Monoid\_\_CoprodI\_\_Word\_\_Pair\_\_fstIdx\_ne}$ applied to $p$ and $h_{1}$.
Monoid.CoprodI.Word.toListdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the list of self (from the name)
English
Let $\mathrm{self}$ be a word of $M$. Then the list of $\mathrm{self}$ is a list of elements of $\Sigma$ applied to the function that maps $i$ to $M$ applied to $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Monoid.CoprodI.liftdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from elements $i$ of $x$ to monoid homomorphisms of $M$ applied to $i$ and $N$ to the set of monoid homomorphisms of the set of coproducts of $M$ and $N$.
Monoid.CoprodI.ofdefMathlib.GroupTheory.CoprodI, function or constant
Wording
no wording
English
$\operatorname{of}$ is a monoid homomorphism of $M$ applied to $i$ and the set of coproducts of $M$.
freeGroupEquivCoprodIdefMathlib.GroupTheory.CoprodI, function or constant
Wording
the free group equivalence coproduct (from the name)
English
The free group equivalence coproduct is a multiplicative equivalence of the set of free groups of $x$ and the set of coproducts of the function that maps $x_{1}$ to the set of free groups of $\mathrm{Unit}$.

Mathlib.GroupTheory.Coset.Basic

AddMonoidHom.fiberEquivdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence of a and b (from the name)
English
Let $f$ be an additive monoid homomorphism of $x$ and $H$. Let $a$ and $b$ be elements of $x$. Then the fiber equivalence of $a$ and $b$ is an equivalence from the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $f$ applied to $a$ to the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $f$ applied to $b$ defined as the composition of the fiber equivalence kernel of $f$ and $a$ and the inverse of the fiber equivalence kernel of $f$ and $b$.
AddMonoidHom.fiberEquivKerdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence kernel of f and a (from the name)
English
Let $f$ be an additive monoid homomorphism of $x$ and $H$. Let $a$ be an element of $x$. Then the fiber equivalence kernel of $f$ and $a$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{preimage} (\operatorname{coe} (f), \operatorname{singleton} (f (a))))}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{3}})})}$.
AddMonoidHom.fiberEquivKerOfSurjectivedefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence kernel of hf and h (from the name)
English
Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $h$ be an element of $H$. Then the fiber equivalence kernel of $\mathrm{hf}$ and $h$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{preimage} (\operatorname{coe} (f), \operatorname{singleton} (h)))}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{3}})})}$.
AddMonoidHom.fiberEquivOfSurjectivedefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence of h and #3 (from the name)
English
Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $h$ and $\mathrm{h'}$ be elements of $H$. Then the fiber equivalence of $h$ and $\mathrm{h'}$ is an equivalence from the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $h$ to the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $\mathrm{h'}$ defined as the composition of the fiber equivalence kernel of $\mathrm{hf}$ and $h$ and the inverse of the fiber equivalence kernel of $\mathrm{hf}$ and $\mathrm{h'}$.
AddSubgroup.addGroupEquivQuotientProdAddSubgroupdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the additive group equivalence quotient product additive subgroup (from the name)
English
The additive group equivalence quotient product additive subgroup is an equivalence from $x$ to $\mathrm{Prod}$ applied to the set of quotients of $x$ and $s$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
AddSubgroup.leftCosetEquivAddSubgroupdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural bijection between the cosets of g (from the docstring)
English
Let $g$ be an element of $x$. Then the natural bijection between the cosets of $g$ is an equivalence from the set of elements of the sum of $g$ and $s$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
AddSubgroup.quotientAddSubgroupOfEmbeddingOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient additive subgroup of H and h (from the name)
English
Let $H$ be an additive subgroup of $x$. Assume that $s \leq t$. Then the quotient additive subgroup of $H$ and $h$ is an embedding of the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and the additive subgroup of $H$ and $s$ and the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})}$ and the additive subgroup of $H$ and $t$.
AddSubgroup.quotientAddSubgroupOfMapOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient additive subgroup of H and x2 (from the name)
English
Let $H$ be an additive subgroup of $x$. Assume that $s \leq t$. Let $x_{2}$ be a quotient of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and the additive subgroup of $s$ and $H$. Then the quotient additive subgroup of $H$ and $x_{2}$ is a quotient of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the additive subgroup of $t$ and $H$.
AddSubgroup.quotientEquivProdOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient equivalence product of h_le (from the name)
English
Assume that $s \leq t$. Then the quotient equivalence product of $\mathrm{h\_le}$ is an equivalence from the set of quotients of $x$ and $s$ to $\mathrm{Prod}$ applied to the set of quotients of $x$ and $t$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$ and the additive subgroup of $s$ and $t$.
AddSubgroup.quotientEquivProdOfLE'defMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient equivalence product of f (from the name)
English
Assume that $s \leq t$. Let $f$ be a function from quotients of $x$ and $t$ to elements of $x$ such that $\operatorname{RightInverse}$ holds for $f$ and $\operatorname{mk}$. Then the quotient equivalence product of $f$ is an equivalence from the set of quotients of $x$ and $s$ to $\mathrm{Prod}$ applied to the set of quotients of $x$ and $t$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$ and the additive subgroup of $s$ and $t$.
AddSubgroup.quotientMapOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient map of h and x2 (from the name)
English
Assume that $s \leq t$. Let $x_{2}$ be a quotient of $x$ and $s$. Then the quotient map of $h$ and $x_{2}$ is a quotient of $x$ and $t$.
AddSubgroup.quotientiInfAddSubgroupOfEmbeddingdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural embedding of f and H (from the docstring)
English
Let $f$ be a function from elements of $x_{2}$ to additive subgroups of $x$. Let $H$ be an additive subgroup of $x$. Then the natural embedding of $f$ and $H$ is an embedding of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the additive subgroup of the infimum of the function that maps $i$ to $f$ applied to $i$ and $H$ and the set of functions from elements $i_{1}$ of $x_{2}$ to quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and the additive subgroup of $f$ applied to $i_{1}$ and $H$.
AddSubgroup.quotientiInfEmbeddingdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural embedding of f (from the docstring)
English
Let $f$ be a function from elements of $x_{2}$ to additive subgroups of $x$. Then the natural embedding of $f$ is an embedding of the set of quotients of $x$ and the infimum of the function that maps $i$ to $f$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{2}$ to quotients of $x$ and $f$ applied to $i_{1}$.
AddSubgroup.rightCosetEquivAddSubgroupdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural bijection between the cosets of g (from the docstring)
English
Let $g$ be an element of $x$. Then the natural bijection between the cosets of $g$ is an equivalence from the set of elements of the sum of the opposite of $g$ and $s$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
LeftAddCosetEquivalencedefMathlib.GroupTheory.Coset.Basic, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{LeftAddCosetEquivalence}$ holds for $s$, $a$ and $b$, if the sum of $a$ and $s$ is equal to the sum of $b$ and $s$.
LeftCosetEquivalencedefMathlib.GroupTheory.Coset.Basic, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{LeftCosetEquivalence}$ holds for $s$, $a$ and $b$, if $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{s}}{\HSMulhSMulMACRoAL {b}{s}}$.
MonoidHom.fiberEquivdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence of a and b (from the name)
English
Let $f$ be a monoid homomorphism of $x$ and $H$. Let $a$ and $b$ be elements of $x$. Then the fiber equivalence of $a$ and $b$ is an equivalence from the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $f$ applied to $a$ to the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $f$ applied to $b$ defined as the composition of the fiber equivalence kernel of $f$ and $a$ and the inverse of the fiber equivalence kernel of $f$ and $b$.
MonoidHom.fiberEquivKerdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence kernel of f and a (from the name)
English
Let $f$ be a monoid homomorphism of $x$ and $H$. Let $a$ be an element of $x$. Then the fiber equivalence kernel of $f$ and $a$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{preimage} (\operatorname{coe} (f), \operatorname{singleton} (f (a))))}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{3}})})}$.
MonoidHom.fiberEquivKerOfSurjectivedefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence kernel of hf and h (from the name)
English
Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $h$ be an element of $H$. Then the fiber equivalence kernel of $\mathrm{hf}$ and $h$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\operatorname{preimage} (\operatorname{coe} (f), \operatorname{singleton} (h)))}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{3}})})}$.
MonoidHom.fiberEquivOfSurjectivedefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the fiber equivalence of h and #3 (from the name)
English
Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $h$ and $\mathrm{h'}$ be elements of $H$. Then the fiber equivalence of $h$ and $\mathrm{h'}$ is an equivalence from the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $h$ to the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $\operatorname{singleton}$ applied to $\mathrm{h'}$ defined as the composition of the fiber equivalence kernel of $\mathrm{hf}$ and $h$ and the inverse of the fiber equivalence kernel of $\mathrm{hf}$ and $\mathrm{h'}$.
QuotientAddGroup.preimageMkEquivAddSubgroupProdSetdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the preimage equivalence additive subgroup product set of s and t (from the name)
English
Let $s$ be an additive subgroup of $x$. Let $t$ be an element of the power set of the set of quotients of $x$ and $s$. Then the preimage equivalence additive subgroup product set of $s$ and $t$ is an equivalence from the set of elements of the preimage of $\operatorname{mk}$ and $t$ to $\mathrm{Prod}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and the set of elements of $t$.
QuotientAddGroup.quotientEquivSelfdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient equivalence self of x (from the name)
English
Let $x$ be a set. Then the quotient equivalence self of $x$ is an equivalence from the set of quotients of $x$ and the bottom to $x$.
QuotientGroup.preimageMkEquivSubgroupProdSetdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the preimage equivalence subgroup product set of s and t (from the name)
English
Let $s$ be a subgroup of $x$. Let $t$ be an element of the power set of the set of quotients of $x$ and $s$. Then the preimage equivalence subgroup product set of $s$ and $t$ is an equivalence from the set of elements of the preimage of $\operatorname{mk}$ and $t$ to $\mathrm{Prod}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and the set of elements of $t$.
QuotientGroup.quotientEquivSelfdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient equivalence self of x (from the name)
English
Let $x$ be a set. Then the quotient equivalence self of $x$ is an equivalence from the set of quotients of $x$ and the bottom to $x$.
RightAddCosetEquivalencedefMathlib.GroupTheory.Coset.Basic, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{RightAddCosetEquivalence}$ holds for $s$, $a$ and $b$, if the sum of the opposite of $a$ and $s$ is equal to the sum of the opposite of $b$ and $s$.
RightCosetEquivalencedefMathlib.GroupTheory.Coset.Basic, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{RightCosetEquivalence}$ holds for $s$, $a$ and $b$, if $\EqtMACRoH {\HSMulhSMulMACRoAL {\operatorname{op} (a)}{s}}{\HSMulhSMulMACRoAL {\operatorname{op} (b)}{s}}$.
Subgroup.groupEquivQuotientProdSubgroupdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the group equivalence quotient product subgroup (from the name)
English
The group equivalence quotient product subgroup is an equivalence from $x$ to $\mathrm{Prod}$ applied to the set of quotients of $x$ and $s$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
Subgroup.leftCosetEquivSubgroupdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural bijection between a left coset of g (from the docstring)
English
Let $g$ be an element of $x$. Then the natural bijection between a left coset of $g$ is an equivalence from the set of elements of $\HSMulhSMulMACRoAL {g}{s}$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
Subgroup.quotientEquivProdOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient equivalence product of h_le (from the name)
English
Assume that $s \leq t$. Then the quotient equivalence product of $\mathrm{h\_le}$ is an equivalence from the set of quotients of $x$ and $s$ to $\mathrm{Prod}$ applied to the set of quotients of $x$ and $t$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$ and the subgroup of $s$ and $t$.
Subgroup.quotientEquivProdOfLE'defMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient equivalence product of f (from the name)
English
Assume that $s \leq t$. Let $f$ be a function from quotients of $x$ and $t$ to elements of $x$ such that $\operatorname{RightInverse}$ holds for $f$ and $\operatorname{mk}$. Then the quotient equivalence product of $f$ is an equivalence from the set of quotients of $x$ and $s$ to $\mathrm{Prod}$ applied to the set of quotients of $x$ and $t$ and the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$ and the subgroup of $s$ and $t$.
Subgroup.quotientMapOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient map of h and x2 (from the name)
English
Assume that $s \leq t$. Let $x_{2}$ be a quotient of $x$ and $s$. Then the quotient map of $h$ and $x_{2}$ is a quotient of $x$ and $t$.
Subgroup.quotientSubgroupOfEmbeddingOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient subgroup of H and h (from the name)
English
Let $H$ be a subgroup of $x$. Assume that $s \leq t$. Then the quotient subgroup of $H$ and $h$ is an embedding of the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and the subgroup of $H$ and $s$ and the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})}$ and the subgroup of $H$ and $t$.
Subgroup.quotientSubgroupOfMapOfLEdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the quotient subgroup of H and x2 (from the name)
English
Let $H$ be a subgroup of $x$. Assume that $s \leq t$. Let $x_{2}$ be a quotient of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and the subgroup of $s$ and $H$. Then the quotient subgroup of $H$ and $x_{2}$ is a quotient of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the subgroup of $t$ and $H$.
Subgroup.quotientiInfEmbeddingdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural embedding of f (from the docstring)
English
Let $f$ be a function from elements of $x_{2}$ to subgroups of $x$. Then the natural embedding of $f$ is an embedding of the set of quotients of $x$ and the infimum of the function that maps $i$ to $f$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{2}$ to quotients of $x$ and $f$ applied to $i_{1}$.
Subgroup.quotientiInfSubgroupOfEmbeddingdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural embedding of f and H (from the docstring)
English
Let $f$ be a function from elements of $x_{2}$ to subgroups of $x$. Let $H$ be a subgroup of $x$. Then the natural embedding of $f$ and $H$ is an embedding of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the subgroup of the infimum of the function that maps $i$ to $f$ applied to $i$ and $H$ and the set of functions from elements $i_{1}$ of $x_{2}$ to quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and the subgroup of $f$ applied to $i_{1}$ and $H$.
Subgroup.rightCosetEquivSubgroupdefMathlib.GroupTheory.Coset.Basic, function or constant
Wording
the natural bijection between a right coset of g (from the docstring)
English
Let $g$ be an element of $x$. Then the natural bijection between a right coset of $g$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\HSMulhSMulMACRoAL {\operatorname{op} (g)}{s})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})})}$.

Mathlib.GroupTheory.Coset.Defs

AddSubgroup.quotientEquivOfEqdefMathlib.GroupTheory.Coset.Defs, function or constant
Wording
the quotient equivalence of h (from the name)
English
Assume that $\EqtMACRoH {s}{t}$. Then the quotient equivalence of $h$ is an equivalence from the set of quotients of $x$ and $s$ to the set of quotients of $x$ and $t$.
QuotientAddGroup.mkdefMathlib.GroupTheory.Coset.Defs, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{mk}$ applied to $a$ is a quotient of $x$ and $s$ defined as $\operatorname{mk''}$ applied to $a$.
QuotientAddGroup.quotientRightRelEquivQuotientLeftReldefMathlib.GroupTheory.Coset.Defs, function or constant
Wording
the quotient right relative equivalence quotient left relation of s (from the name)
English
Let $s$ be an additive subgroup of $x$. Then the quotient right relative equivalence quotient left relation of $s$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{rightRel}$ applied to $s$ to the set of quotients of $x$ and $s$.
QuotientGroup.mkdefMathlib.GroupTheory.Coset.Defs, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{mk}$ applied to $a$ is a quotient of $x$ and $s$ defined as $\operatorname{mk''}$ applied to $a$.
QuotientGroup.quotientRightRelEquivQuotientLeftReldefMathlib.GroupTheory.Coset.Defs, function or constant
Wording
the quotient right relative equivalence quotient left relation of s (from the name)
English
Let $s$ be a subgroup of $x$. Then the quotient right relative equivalence quotient left relation of $s$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{rightRel}$ applied to $s$ to the set of quotients of $x$ and $s$.
Subgroup.quotientEquivOfEqdefMathlib.GroupTheory.Coset.Defs, function or constant
Wording
the quotient equivalence of h (from the name)
English
Assume that $\EqtMACRoH {s}{t}$. Then the quotient equivalence of $h$ is an equivalence from the set of quotients of $x$ and $s$ to the set of quotients of $x$ and $t$.

Mathlib.GroupTheory.Coxeter.Basic

CoxeterMatrix.GroupdefMathlib.GroupTheory.Coxeter.Basic, type
Wording
group of M (from the name)
English
Let $M$ be a Coxeter matrix of $B$. Then a group of $M$ is an element of the function that maps $M$ to the set of presented groups of the relation set of $M$.
CoxeterMatrix.IsLiftabledefMathlib.GroupTheory.Coxeter.Basic, predicate
Wording
no wording
English
Let $M$ be a Coxeter matrix of $B$. Let $f$ be a function from elements of $B$ to elements of $G$. Then $\operatorname{IsLiftable}$ holds for $M$ and $f$, if for all elements $i$ and $\mathrm{i'}$ of $B$, $\EqtMACRoH {(f (i)\times f (\mathrm{i'}))^ {\operatorname{M} (M , i , \mathrm{i'})}}{1}$.
CoxeterMatrix.reindexGroupEquivdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the reindexing group equivalence of M and e (from the name)
English
Let $M$ be a Coxeter matrix of $B$. Let $e$ be an equivalence from $B$ to $\mathrm{B'}$. Then the reindexing group equivalence of $M$ and $e$ is a multiplicative equivalence of the set of groups of the reindexing of $e$ and $M$ and the set of groups of $M$.
CoxeterMatrix.relationdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the relation of i and #3 (from the name)
English
Let $M$ be a Coxeter matrix of $B$. Let $i$ and $\mathrm{i'}$ be elements of $B$. Then the relation of $i$ and $\mathrm{i'}$ is a free group of $B$ defined as $(\operatorname{of} (i)\times \operatorname{of} (\mathrm{i'}))^ {\operatorname{M} (M , i , \mathrm{i'})}$.
CoxeterMatrix.relationsSetdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the relation set of M (from the name)
English
Let $M$ be a Coxeter matrix of $B$. Then the relation set of $M$ is an element of the power set of the set of free groups of $B$ defined as the range of $\operatorname{uncurry}$ applied to $\operatorname{relation}$.
CoxeterMatrix.simpledefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the simple reflection of the Coxeter group of M and i (from the docstring)
English
Let $M$ be a Coxeter matrix of $B$. Let $i$ be an element of $B$. Then the simple reflection of the Coxeter group of $M$ and $i$ is a group of $M$ defined as $\operatorname{of}$ applied to $i$.
CoxeterMatrix.toCoxeterSystemdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the Coxeter system of M (from the name)
English
Let $M$ be a Coxeter matrix of $B$. Then the Coxeter system of $M$ is a Coxeter system of $M$ and the set of groups of $M$ defined as $\operatorname{mk}$ applied to the identity map of the set of groups of $M$.
CoxeterSystemstructureMathlib.GroupTheory.Coxeter.Basic, type
Wording
Coxeter system of M and W (from the name)
English
Let $M$ be a Coxeter matrix of $B$. Let $W$ be a set. Then the Coxeter systems of $M$ and $W$ are a basic type.
CoxeterSystem.alternatingWorddefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the alternating word of m and #3 (from the name)
English
Let $i$ and $\mathrm{i'}$ be elements of $B$. Let $m$ be a natural number. Then the alternating word of $\mathrm{i'}$ and $m$ is a list of elements of $B$ defined as $\operatorname{brecOn}$ applied to $m$, $\mathrm{CoxeterSystem\_\_alternatingWord\_\_\_f}$, $i$ and $\mathrm{i'}$.
CoxeterSystem.braidWorddefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
no wording
English
Let $M$ be a Coxeter matrix of $B$. Let $i$ and $\mathrm{i'}$ be elements of $B$. Then $\operatorname{braidWord}$ applied to $M$, $i$ and $\mathrm{i'}$ is a list of elements of $B$ defined as the alternating word of $\mathrm{i'}$ and $\operatorname{M}$ applied to $M$, $i$ and $\mathrm{i'}$.
CoxeterSystem.liftdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the lift of cs (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Then the lift of $\mathrm{cs}$ is an equivalence from $\SubtypeSet {f}{\operatorname{IsLiftable} (M , f)}$ to the set of monoid homomorphisms of $W$ and $G$.
CoxeterSystem.mapdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the map of cs and e (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $e$ be a multiplicative equivalence of $W$ and $H$. Then the map of $\mathrm{cs}$ and $e$ is a Coxeter system of $M$ and $H$ defined as $\operatorname{mk}$ applied to the composition of the inverse of $e$ and the multiplicative equivalence of $\mathrm{cs}$.
CoxeterSystem.mulEquivdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the multiplicative equivalence of self (from the name)
English
Let $\mathrm{self}$ be a Coxeter system of $M$ and $W$. Then the multiplicative equivalence of $\mathrm{self}$ is a multiplicative equivalence of $W$ and the set of groups of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CoxeterSystem.reindexdefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the reindexing of cs and e (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $e$ be an equivalence from $B$ to $\mathrm{B'}$. Then the reindexing of $\mathrm{cs}$ and $e$ is a Coxeter system of the reindexing of $e$ and $M$ and $W$ defined as $\operatorname{mk}$ applied to the composition of the multiplicative equivalence of $\mathrm{cs}$ and the inverse of the reindexing group equivalence of $M$ and $e$.
CoxeterSystem.simpledefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $i$ be an element of $B$. Then $\operatorname{simple}$ applied to $\mathrm{cs}$ and $i$ is an element of $W$ defined as $\operatorname{symm}$ applied to the multiplicative equivalence of $\mathrm{cs}$ and $\operatorname{of}$ applied to $i$.
CoxeterSystem.wordProddefMathlib.GroupTheory.Coxeter.Basic, function or constant
Wording
the word product of cs and x1 (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $x_{1}$ be a list of elements of $B$. Then the word product of $\mathrm{cs}$ and $x_{1}$ is an element of $W$ defined as $\operatorname{prod}$ applied to $\operatorname{map}$ applied to $\operatorname{simple}$ applied to $\mathrm{cs}$ and $x_{1}$.
IsCoxeterGroupclassMathlib.GroupTheory.Coxeter.Basic, predicate
Wording
W is a Coxeter group (from the name)
English
Let $W$ be a set. Then we can say that $W$ is a Coxeter group.

Mathlib.GroupTheory.Coxeter.Inversion

CoxeterSystem.IsLeftInversiondefMathlib.GroupTheory.Coxeter.Inversion, predicate
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $w$ and $t$ be elements of $W$. Then $\operatorname{IsLeftInversion}$ holds for $\mathrm{cs}$, $w$ and $t$, if $\operatorname{IsReflection}$ holds for $\mathrm{cs}$ and $t$ and the length of $\mathrm{cs}$ and $t \times w$ is less than the length of $\mathrm{cs}$ and $w$.
CoxeterSystem.IsReflectiondefMathlib.GroupTheory.Coxeter.Inversion, predicate
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $t$ be an element of $W$. Then $\operatorname{IsReflection}$ holds for $\mathrm{cs}$ and $t$, if there exists an element $w$ of $W$, such that there exists an element $i$ of $B$, such that $\EqtMACRoH {t}{w \times \operatorname{simple} (\mathrm{cs} , i)\times \operatorname{inv} (w)}$.
CoxeterSystem.IsRightInversiondefMathlib.GroupTheory.Coxeter.Inversion, predicate
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $w$ and $t$ be elements of $W$. Then $\operatorname{IsRightInversion}$ holds for $\mathrm{cs}$, $w$ and $t$, if $\operatorname{IsReflection}$ holds for $\mathrm{cs}$ and $t$ and the length of $\mathrm{cs}$ and $w \times t$ is less than the length of $\mathrm{cs}$ and $w$.
CoxeterSystem.leftInvSeqdefMathlib.GroupTheory.Coxeter.Inversion, function or constant
Wording
the left inverse sequence of cs and x1 (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $x_{1}$ be a list of elements of $B$. Then the left inverse sequence of $\mathrm{cs}$ and $x_{1}$ is a list of elements of $W$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CoxeterSystem\_\_leftInvSeq\_\_\_f}$ applied to $\mathrm{cs}$.
CoxeterSystem.rightInvSeqdefMathlib.GroupTheory.Coxeter.Inversion, function or constant
Wording
the right inverse sequence of cs and x1 (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $x_{1}$ be a list of elements of $B$. Then the right inverse sequence of $\mathrm{cs}$ and $x_{1}$ is a list of elements of $W$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CoxeterSystem\_\_rightInvSeq\_\_\_f}$ applied to $\mathrm{cs}$.

Mathlib.GroupTheory.Coxeter.Length

CoxeterSystem.IsLeftDescentdefMathlib.GroupTheory.Coxeter.Length, predicate
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $w$ be an element of $W$. Let $i$ be an element of $B$. Then $\operatorname{IsLeftDescent}$ holds for $\mathrm{cs}$, $w$ and $i$, if the length of $\mathrm{cs}$ and $\operatorname{simple} (\mathrm{cs} , i)\times w$ is less than the length of $\mathrm{cs}$ and $w$.
CoxeterSystem.IsReduceddefMathlib.GroupTheory.Coxeter.Length, predicate
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $x_{1}$ be a list of elements of $B$. Then $\operatorname{IsReduced}$ holds for $\mathrm{cs}$ and $x_{1}$, if the length of $\mathrm{cs}$ and the word product of $\mathrm{cs}$ and $x_{1}$ is equal to $\operatorname{length}$ applied to $x_{1}$.
CoxeterSystem.IsRightDescentdefMathlib.GroupTheory.Coxeter.Length, predicate
Wording
no wording
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $w$ be an element of $W$. Let $i$ be an element of $B$. Then $\operatorname{IsRightDescent}$ holds for $\mathrm{cs}$, $w$ and $i$, if the length of $\mathrm{cs}$ and $w \times \operatorname{simple} (\mathrm{cs} , i)$ is less than the length of $\mathrm{cs}$ and $w$.
CoxeterSystem.lengthdefMathlib.GroupTheory.Coxeter.Length, function or constant
Wording
the length of cs and w (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Let $w$ be an element of $W$. Then the length of $\mathrm{cs}$ and $w$ is a natural number.
CoxeterSystem.lengthParitydefMathlib.GroupTheory.Coxeter.Length, function or constant
Wording
the length parity of cs (from the name)
English
Let $\mathrm{cs}$ be a Coxeter system of $M$ and $W$. Then the length parity of $\mathrm{cs}$ is a monoid homomorphism of $W$ and the set of multiplicatives of $\mathrm{ZMod}$ applied to $2$ defined as $\operatorname{lift}$ applied to $\mathrm{cs}$ and the function that maps $x_{1}$ to $\operatorname{ofAdd}$ applied to $1$.

Mathlib.GroupTheory.Coxeter.Matrix

CoxeterMatrixstructureMathlib.GroupTheory.Coxeter.Matrix, type
Wording
Coxeter matrix of B (from the name)
English
Let $B$ be a set. Then the Coxeter matrixes of $B$ are a basic type.
CoxeterMatrix.AdefMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
Let $n$ be a natural number. Then $\operatorname{A}$ applied to $n$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $n$.
CoxeterMatrix.BdefMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
Let $n$ be a natural number. Then $\operatorname{B}$ applied to $n$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $n$.
CoxeterMatrix.DdefMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
Let $n$ be a natural number. Then $\operatorname{D}$ applied to $n$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $n$.
CoxeterMatrix.E₆defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_E\_u2086\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $6$.
CoxeterMatrix.E₇defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_E\_u2087\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $7$.
CoxeterMatrix.E₈defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_E\_u2088\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $8$.
CoxeterMatrix.F₄defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_F\_u2084\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $4$.
CoxeterMatrix.G₂defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_G\_u2082\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $2$.
CoxeterMatrix.H₃defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_H\_u2083\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $3$.
CoxeterMatrix.H₄defMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
$\mathrm{CoxeterMatrix\_\_H\_u2084\_}$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $4$.
CoxeterMatrix.IdefMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
Let $m$ be a natural number. Then $\operatorname{I}$ applied to $m$ is a Coxeter matrix of $\mathrm{Fin}$ applied to $2$.
CoxeterMatrix.MdefMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a Coxeter matrix of $B$. Then there is a matrix of $B$ and $\Natural$. Proof. Let $\mathrm{self}$ be arbitrary. By self. By CoxeterMatrix__proj0.
CoxeterMatrix.reindexdefMathlib.GroupTheory.Coxeter.Matrix, function or constant
Wording
the reindexing of e and M (from the name)
English
Let $e$ be an equivalence from $B$ to $\mathrm{B'}$. Let $M$ be a Coxeter matrix of $B$. Then the reindexing of $e$ and $M$ is a Coxeter matrix of $\mathrm{B'}$.

Mathlib.GroupTheory.Divisible

DivisibleByclassMathlib.GroupTheory.Divisible, predicate
Wording
no wording
English
Let $A$ and $x$ be sets. Then we can say that $\mathrm{DivisibleBy}$ holds for $A$ and $x$.
DivisibleBy.divdefMathlib.GroupTheory.Divisible, function or constant
Wording
the quotient of x4 and x5 (from the name)
English
Let $x_{4}$ be an element of $A$. Let $x_{5}$ be an element of $x$. Then the quotient of $x_{4}$ and $x_{5}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{4}$ and $x_{5}$.
RootableByclassMathlib.GroupTheory.Divisible, predicate
Wording
no wording
English
Let $A$ and $x$ be sets. Then we can say that $\mathrm{RootableBy}$ holds for $A$ and $x$.
RootableBy.rootdefMathlib.GroupTheory.Divisible, function or constant
Wording
the root function of x4 and x5 (from the docstring)
English
Let $x_{4}$ be an element of $A$. Let $x_{5}$ be an element of $x$. Then the root function of $x_{4}$ and $x_{5}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{4}$ and $x_{5}$.

Mathlib.GroupTheory.DivisibleHull

DivisibleHulldefMathlib.GroupTheory.DivisibleHull, type
Wording
divisible hull of M (from the name)
English
Let $M$ be a set. Then a divisible hull of $M$ is an element of the function that maps $M$ to the set of localized modules of the non zero divisor of $\Natural$ and $M$.
DivisibleHull.archimedeanClassOrderIsodefMathlib.GroupTheory.DivisibleHull, function or constant
Wording
the archimedean class order isomorphism of M (from the name)
English
Let $M$ be a set. Then the archimedean class order isomorphism of $M$ is an order isomorphism of the set of archimedean classes of $M$ and the set of archimedean classes of the set of divisible hulls of $M$.
DivisibleHull.coedefMathlib.GroupTheory.DivisibleHull, function or constant
Wording
the coercion of m (from the name)
English
Let $m$ be an element of $M$. Then the coercion of $m$ is a divisible hull of $M$ defined as $\operatorname{mk}$ applied to $m$ and $1$.
DivisibleHull.coeAddMonoidHomdefMathlib.GroupTheory.DivisibleHull, function or constant
Wording
the coercion additive monoid homomorphism of M (from the name)
English
Let $M$ be a set. Then the coercion additive monoid homomorphism of $M$ is an additive monoid homomorphism of $M$ and the set of divisible hulls of $M$.
DivisibleHull.coeOrderAddMonoidHomdefMathlib.GroupTheory.DivisibleHull, function or constant
Wording
the coercion order additive monoid homomorphism of M (from the name)
English
Let $M$ be a set. Then the coercion order additive monoid homomorphism of $M$ is an order additive monoid homomorphism of $M$ and the set of divisible hulls of $M$.
DivisibleHull.liftOndefMathlib.GroupTheory.DivisibleHull, function or constant
Wording
no wording
English
Let $x_{2}$ be a divisible hull of $M$. Let $f$ be a function from elements of $M$ and positive natural numbers to elements of $x_{1}$ such that for all elements $m$ and $\mathrm{m'}$ of $M$, for all positive natural numbers $s$ and $\mathrm{s'}$, if $\EqtMACRoH {\operatorname{mk} (m , s)}{\operatorname{mk} (\mathrm{m'} , \mathrm{s'})}$, then $\EqtMACRoH {f (m , s)}{f (\mathrm{m'} , \mathrm{s'})}$. Then $\operatorname{liftOn}$ applied to $x_{2}$, $f$ and $h$ is an element of $x_{1}$.
DivisibleHull.liftOn₂defMathlib.GroupTheory.DivisibleHull, function or constant
Wording
no wording
English
Let $x_{2}$ and $y$ be divisible hulls of $M$. Let $f$ be a function from elements of $M$ and positive natural numbers and elements of $M$ and elements of $\PNatMACRoAD$ to elements of $x_{1}$ such that for all elements $m$, $n$, $\mathrm{m'}$ and $\mathrm{n'}$ of $M$, for all positive natural numbers $s$, $t$, $\mathrm{s'}$ and $\mathrm{t'}$, if $\EqtMACRoH {\operatorname{mk} (m , s)}{\operatorname{mk} (\mathrm{m'} , \mathrm{s'})}$, then if $\EqtMACRoH {\operatorname{mk} (n , t)}{\operatorname{mk} (\mathrm{n'} , \mathrm{t'})}$, then $\EqtMACRoH {f (m , s , n , t)}{f (\mathrm{m'} , \mathrm{s'} , \mathrm{n'} , \mathrm{t'})}$. Then $\mathrm{DivisibleHull\_\_liftOn\_u2082\_}$ applied to $x_{2}$, $y$, $f$ and $h$ is an element of $x_{1}$.
DivisibleHull.mkdefMathlib.GroupTheory.DivisibleHull, function or constant
Wording
no wording
English
Let $m$ be an element of $M$. Let $s$ be a positive natural number. Then $\operatorname{mk}$ applied to $m$ and $s$ is a divisible hull of $M$ defined as $\operatorname{mk}$ applied to $m$ and $\operatorname{equivNonZeroDivisorsNat}$ applied to $s$.

Mathlib.GroupTheory.DoubleCoset

DoubleCoset.QuotientdefMathlib.GroupTheory.DoubleCoset, type
Wording
quotient of H and K (from the name)
English
Let $H$ and $K$ be elements of $\wp G$. Then a quotient of $H$ and $K$ is an element of the function that maps $H$ and $K$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $H$ and $K$.
DoubleCoset.doubleCosetdefMathlib.GroupTheory.DoubleCoset, function or constant
Wording
the double coset as an element of a (from the docstring)
English
Let $a$ be an element of $x$. Let $s$ and $t$ be elements of $\wp x$. Then the double coset as an element of $a$ is an element of $\wp x$ defined as $s \times \operatorname{singleton} (a)\times t$.
DoubleCoset.mkdefMathlib.GroupTheory.DoubleCoset, function or constant
Wording
no wording
English
Let $H$ and $K$ be subgroups of $G$. Let $a$ be an element of $G$. Then $\operatorname{mk}$ applied to $H$, $K$ and $a$ is a quotient of $H$ and $K$ defined as $\operatorname{mk''}$ applied to $a$.
DoubleCoset.quotToDoubleCosetdefMathlib.GroupTheory.DoubleCoset, function or constant
Wording
the quotient to double coset of K and q (from the name)
English
Let $H$ and $K$ be subgroups of $G$. Let $q$ be a quotient of $H$ and $K$. Then the quotient to double coset of $K$ and $q$ is an element of $\wp G$ defined as the double coset as an element of $\operatorname{out}$ applied to $q$.

Mathlib.GroupTheory.EckmannHilton

EckmannHilton.IsUnitalstructureMathlib.GroupTheory.EckmannHilton, predicate
Wording
no wording
English
Let $m$ be a function from elements of $X$ and elements of $X$ to elements of $X$. Let $e$ be an element of $X$. Then we can say that $\operatorname{IsUnital}$ holds for $m$ and $e$.

Mathlib.GroupTheory.Exponent

AddMonoid.ExponentExistsdefMathlib.GroupTheory.Exponent, predicate
Wording
no wording
English
Let $G$ be a set. Then $\operatorname{ExponentExists}$ holds for $G$, if there exists a natural number $n$, such that $0 < n$ and for all elements $g$ of $G$, $\EqtMACRoH {\HSMulhSMulMACRoAL {n}{g}}{0}$.
AddMonoid.exponentdefMathlib.GroupTheory.Exponent, function or constant
Wording
the exponent of G (from the docstring)
English
Let $G$ be a set. Then the exponent of $G$ is a natural number defined as $\mathrm{dite}$ applied to $\operatorname{ExponentExists}$ applied to $G$, the function that maps $h$ to $\operatorname{find}$ applied to $h$ and the function that maps $h_{1}$ to $0$.
Monoid.ExponentExistsdefMathlib.GroupTheory.Exponent, predicate
Wording
no wording
English
Let $G$ be a set. Then $\operatorname{ExponentExists}$ holds for $G$, if there exists a natural number $n$, such that $0 < n$ and for all elements $g$ of $G$, $\EqtMACRoH {g ^ {n}}{1}$.
Monoid.exponentdefMathlib.GroupTheory.Exponent, function or constant
Wording
the exponent of G (from the docstring)
English
Let $G$ be a set. Then the exponent of $G$ is a natural number defined as $\mathrm{dite}$ applied to $\operatorname{ExponentExists}$ applied to $G$, the function that maps $h$ to $\operatorname{find}$ applied to $h$ and the function that maps $h_{1}$ to $0$.

Mathlib.GroupTheory.FiniteAbelian.Duality

CommGroup.monoidHomMonoidHomEquivdefMathlib.GroupTheory.FiniteAbelian.Duality, function or constant
Wording
the monoid homomorphism monoid homomorphism equivalence of G and M (from the name)
English
Let $G$ and $M$ be sets. Then the monoid homomorphism monoid homomorphism equivalence of $G$ and $M$ is a multiplicative equivalence of the set of monoid homomorphisms of the set of monoid homomorphisms of $G$ and $\UnitsMACRoAO {M}$ and $\UnitsMACRoAO {M}$ and $G$.
CommGroup.subgroupOrderIsoSubgroupMonoidHomdefMathlib.GroupTheory.FiniteAbelian.Duality, function or constant
Wording
the subgroup order isomorphism subgroup monoid homomorphism of G and M (from the name)
English
Let $G$ and $M$ be sets. Then the subgroup order isomorphism subgroup monoid homomorphism of $G$ and $M$ is an order isomorphism of the set of subgroups of $G$ and the set of order duals of the set of subgroups of the set of monoid homomorphisms of $G$ and $\UnitsMACRoAO {M}$.

Mathlib.GroupTheory.FiniteIndexNormalSubgroup

FiniteIndexNormalAddSubgroupstructureMathlib.GroupTheory.FiniteIndexNormalSubgroup, type
Wording
finite index normal additive subgroup of G (from the name)
English
Let $G$ be a set. Then the finite index normal additive subgroups of $G$ are a basic type.
FiniteIndexNormalAddSubgroup.comapdefMathlib.GroupTheory.FiniteIndexNormalSubgroup, function or constant
Wording
the preimage of f and K (from the docstring)
English
Let $f$ be an additive monoid homomorphism of $G$ and $H$. Let $K$ be a finite index normal additive subgroup of $H$. Then the preimage of $f$ and $K$ is a finite index normal additive subgroup of $G$.
FiniteIndexNormalAddSubgroup.ofAddSubgroupdefMathlib.GroupTheory.FiniteIndexNormalSubgroup, function or constant
Wording
the finite index normal additive subgroup of H (from the name)
English
Let $H$ be an additive subgroup of $G$. Then the finite index normal additive subgroup of $H$ is a finite index normal additive subgroup of $G$.
FiniteIndexNormalSubgroupstructureMathlib.GroupTheory.FiniteIndexNormalSubgroup, type
Wording
finite index normal subgroup of G (from the name)
English
Let $G$ be a set. Then the finite index normal subgroups of $G$ are a basic type.
FiniteIndexNormalSubgroup.comapdefMathlib.GroupTheory.FiniteIndexNormalSubgroup, function or constant
Wording
the preimage of f and K (from the docstring)
English
Let $f$ be a monoid homomorphism of $G$ and $H$. Let $K$ be a finite index normal subgroup of $H$. Then the preimage of $f$ and $K$ is a finite index normal subgroup of $G$.
FiniteIndexNormalSubgroup.ofSubgroupdefMathlib.GroupTheory.FiniteIndexNormalSubgroup, function or constant
Wording
the finite index normal subgroup of H (from the name)
English
Let $H$ be a subgroup of $G$. Then the finite index normal subgroup of $H$ is a finite index normal subgroup of $G$.

Mathlib.GroupTheory.FinitelyPresentedGroup

AddGroup.IsFinitelyPresentedclassMathlib.GroupTheory.FinitelyPresentedGroup, predicate
Wording
no wording
English
Let $G$ be a set. Then we can say that $\operatorname{IsFinitelyPresented}$ holds for $G$.
AddSubgroup.IsFinitelyNormallyGenerateddefMathlib.GroupTheory.FinitelyPresentedGroup, predicate
Wording
no wording
English
Let $N$ be an additive subgroup of $G$. Then $\operatorname{IsFinitelyNormallyGenerated}$ holds for $N$, if there exists an element $S$ of $\wp G$, such that $S$ is finite and the normal closure of $S$ is equal to $N$.
Group.IsFinitelyPresentedclassMathlib.GroupTheory.FinitelyPresentedGroup, predicate
Wording
no wording
English
Let $G$ be a set. Then we can say that $\operatorname{IsFinitelyPresented}$ holds for $G$.
Subgroup.IsFinitelyNormallyGenerateddefMathlib.GroupTheory.FinitelyPresentedGroup, predicate
Wording
no wording
English
Let $N$ be a subgroup of $G$. Then $\operatorname{IsFinitelyNormallyGenerated}$ holds for $N$, if there exists an element $S$ of $\wp G$, such that $S$ is finite and the normal closure of $S$ is equal to $N$.

Mathlib.GroupTheory.Finiteness

AddGroup.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $G$ be a set. Then $\operatorname{FG}$ holds for $G$, if $\mathrm{IsAddFG}$ holds for $G$.
AddMonoid.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{FG}$ holds for $M$, if $\mathrm{IsAddFG}$ holds for $M$.
AddSubgroup.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $P$ be an additive subgroup of $G$. Then $\operatorname{FG}$ holds for $P$, if $\mathrm{IsAddFG}$ holds for $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {P}{x_{1}})}$.
AddSubmonoid.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $P$ be an additive submonoid of $M$. Then $\operatorname{FG}$ holds for $P$, if $\mathrm{IsAddFG}$ holds for $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {P}{x_{1}})}$.
Group.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $G$ be a set. Then $\operatorname{FG}$ holds for $G$, if $\mathrm{IsMulFG}$ holds for $G$.
IsAddFGclassMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $M$ be a set. Then we can say that $\mathrm{IsAddFG}$ holds for $M$.
IsMulFGclassMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $M$ be a set. Then we can say that $\mathrm{IsMulFG}$ holds for $M$.
Monoid.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{FG}$ holds for $M$, if $\mathrm{IsMulFG}$ holds for $M$.
Subgroup.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $P$ be a subgroup of $G$. Then $\operatorname{FG}$ holds for $P$, if $\mathrm{IsMulFG}$ holds for $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {P}{x_{1}})}$.
Submonoid.FGdefMathlib.GroupTheory.Finiteness, predicate
Wording
no wording
English
Let $P$ be a submonoid of $M$. Then $\operatorname{FG}$ holds for $P$, if $\mathrm{IsMulFG}$ holds for $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {P}{x_{1}})}$.

Mathlib.GroupTheory.FixedPointFree

MonoidHom.FixedPointFreedefMathlib.GroupTheory.FixedPointFree, predicate
Wording
x is a fixed point free (from the name)
English
Let $x$ be a function from elements of $G$ to elements of $G$. Then $x$ is a fixed point free, if for all elements $g$ of $G$, if $\EqtMACRoH {x (g)}{g}$, then $\EqtMACRoH {g}{1}$.
MonoidHom.commutatorMapdefMathlib.GroupTheory.FixedPointFree, function or constant
Wording
the commutator map of x and g (from the docstring)
English
Let $x$ be a function from elements of $G$ to elements of $G$. Let $g$ be an element of $G$. Then the commutator map of $x$ and $g$ is an element of $G$ defined as $\frac{ g}{x (g)}$.

Mathlib.GroupTheory.Focal

AddSubgroup.focalAddSubgroupdefMathlib.GroupTheory.Focal, function or constant
Wording
the focal additive subgroup of H (from the name)
English
Let $H$ be an additive subgroup of $G$. Then the focal additive subgroup of $H$ is an additive subgroup of $G$ defined as the closure of $\operatorname{ofPred}$ applied to the function that maps $g$ to the proposition that $g$ is an element of $H$ and there exists an element $x_{1}$ of $G$ such that $x_{1}$ is an element of $H$ and there exists an element $u$ of $G$ such that $g$ is equal to the bracket of $x_{1}$ and $u$.
AddSubgroup.focalAddSubgroupOfdefMathlib.GroupTheory.Focal, function or constant
Wording
the focal additive subgroup of H (from the name)
English
Let $H$ be an additive subgroup of $G$. Then the focal additive subgroup of $H$ is an additive subgroup of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ defined as the additive subgroup of the focal additive subgroup of $H$ and $H$.
AddSubgroup.transferFocaldefMathlib.GroupTheory.Focal, function or constant
Wording
the transfer homomorphism of H (from the docstring)
English
Let $H$ be an additive subgroup of $G$. Then the transfer homomorphism of $H$ is an additive monoid homomorphism of $G$ and the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the focal additive subgroup of $H$ defined as the transfer of $\operatorname{mk'}$ applied to the focal additive subgroup of $H$.
Subgroup.focalSubgroupdefMathlib.GroupTheory.Focal, function or constant
Wording
the focal subgroup of H (from the name)
English
Let $H$ be a subgroup of $G$. Then the focal subgroup of $H$ is a subgroup of $G$ defined as the closure of $\operatorname{ofPred}$ applied to the function that maps $g$ to the proposition that $g$ is an element of $H$ and there exists an element $x_{1}$ of $G$ such that $x_{1}$ is an element of $H$ and there exists an element $u$ of $G$ such that $g$ is equal to the bracket of $x_{1}$ and $u$.
Subgroup.focalSubgroupOfdefMathlib.GroupTheory.Focal, function or constant
Wording
the focal subgroup of H (from the name)
English
Let $H$ be a subgroup of $G$. Then the focal subgroup of $H$ is a subgroup of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ defined as the subgroup of the focal subgroup of $H$ and $H$.
Subgroup.transferFocaldefMathlib.GroupTheory.Focal, function or constant
Wording
the transfer homomorphism of H (from the docstring)
English
Let $H$ be a subgroup of $G$. Then the transfer homomorphism of $H$ is a monoid homomorphism of $G$ and the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the focal subgroup of $H$ defined as the transfer of $\operatorname{mk'}$ applied to the focal subgroup of $H$.
Subgroup.transferFocal.quotientKerMulEquivQuotientFocalSubgroupOfdefMathlib.GroupTheory.Focal, function or constant
Wording
the quotient kernel multiplicative equivalence quotient focal subgroup of P (from the name)
English
Let $P$ be an element of $\mathrm{Sylow}$ applied to $p$ and $G$. Then the quotient kernel multiplicative equivalence quotient focal subgroup of $P$ is a multiplicative equivalence of the set of quotients of $G$ and the multiplicative kernel of the transfer homomorphism of $\operatorname{toSubgroup}$ applied to $P$ and the set of quotients of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (P)}{x_{1}})}$ and the focal subgroup of $\operatorname{toSubgroup}$ applied to $P$ defined as the quotient kernel equivalence of the transfer homomorphism of $\operatorname{toSubgroup}$ applied to $P$ and $\mathrm{Subgroup\_\_transferFocal\_surjective}$ applied to $P$.

Mathlib.GroupTheory.Frattini

frattinidefMathlib.GroupTheory.Frattini, function or constant
Wording
the Frattini subgroup of G (from the docstring)
English
Let $G$ be a set. Then the Frattini subgroup of $G$ is a subgroup of $G$ defined as the radical of the set of subgroups of $G$.

Mathlib.GroupTheory.FreeAbelianGroup

FreeAbelianGroupdefMathlib.GroupTheory.FreeAbelianGroup, type
Wording
free Abelian group of x (from the name)
English
Let $x$ be a set. Then a free Abelian group of $x$ is an element of the function that maps $x$ to $\mathrm{Additive}$ applied to the set of abelianizations of the set of free groups of $x$.
FreeAbelianGroup.equivOfEquivdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the equivalence of f (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Then the equivalence of $f$ is an additive equivalence of the set of free Abelian groups of $x$ and the set of free Abelian groups of $x_{1}$.
FreeAbelianGroup.liftdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of additive monoid homomorphisms of the set of free Abelian groups of $x$ and $x_{1}$ defined as the composition of the lift and the composition of the lift and $\operatorname{toAdditive}$.
FreeAbelianGroup.liftAddEquivdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the lift additive equivalence (from the name)
English
The lift additive equivalence is an additive equivalence of the set of functions from elements of $x$ to elements of $G$ and the set of additive monoid homomorphisms of the set of free Abelian groups of $x$ and $G$ defined as $\operatorname{mk}$ applied to the lift and $\mathrm{FreeAbelianGroup\_\_lift\_add}$.
FreeAbelianGroup.liftAddGroupHomdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the lift additive group homomorphism of x1 and a (from the name)
English
Let $x_{1}$ be a set. Let $a$ be a free Abelian group of $x$. Then the lift additive group homomorphism of $x_{1}$ and $a$ is an additive monoid homomorphism of the set of functions from elements of $x$ to elements of $x_{1}$ and $x_{1}$ defined as $\operatorname{mk'}$ applied to the function that maps $f$ to $\operatorname{coe}$ applied to the lift, $f$ and $a$ and the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{FreeAbelianGroup\_\_lift\_add\_apply}$ applied to $x_{5}$, $x_{6}$ and $a$.
FreeAbelianGroup.mapdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is an additive monoid homomorphism of the set of free Abelian groups of $x$ and the set of free Abelian groups of $x_{1}$ defined as $\operatorname{lift}$ applied to $\operatorname{comp}$ applied to $\operatorname{of}$ and $f$.
FreeAbelianGroup.ofdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free Abelian group of $x$ defined as $\operatorname{ofMul}$ applied to $\operatorname{of}$ applied to $\operatorname{of}$ applied to $x_{1}$.
FreeAbelianGroup.seqAddGroupHomdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the sequence additive group homomorphism of f (from the name)
English
Let $f$ be a free Abelian group of the set of functions from elements of $x$ to elements of $x_{1}$. Then the sequence additive group homomorphism of $f$ is an additive monoid homomorphism of the set of free Abelian groups of $x$ and the set of free Abelian groups of $x_{1}$.
FreeAbelianGroup.uniqueEquivdefMathlib.GroupTheory.FreeAbelianGroup, function or constant
Wording
the unique equivalence of T (from the name)
English
Let $T$ be a set. Then the unique equivalence of $T$ is an additive equivalence of the set of free Abelian groups of $T$ and $\Integer$.

Mathlib.GroupTheory.FreeGroup.Basic

FreeAddGroupdefMathlib.GroupTheory.FreeGroup.Basic, type
Wording
free additive group of x (from the name)
English
Let $x$ be a set. Then a free additive group of $x$ is an element of the function that maps $x$ to $\mathrm{Quot}$ applied to $\operatorname{Step}$.
FreeAddGroup.IsReduceddefMathlib.GroupTheory.FreeGroup.Basic, predicate
Wording
L is reduced (from the name)
English
Let $L$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $L$ is reduced, if $\operatorname{IsChain}$ holds for the function that maps $a$ and $b$ to the proposition that if $\EqtMACRoH {\ProdfstMACRoZ {a}}{\ProdfstMACRoZ {b}}$, then $\EqtMACRoH {\ProdsndMACRoAA {a}}{\ProdsndMACRoAA {b}}$ and $L$.
FreeAddGroup.ReddefMathlib.GroupTheory.FreeGroup.Basic, predicate
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be lists of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{Red}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{ReflTransGen}$ holds for $\operatorname{Step}$, $x_{1}$ and $x_{2}$.
FreeAddGroup.Red.StepinductiveMathlib.GroupTheory.FreeGroup.Basic, predicate
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be lists of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then we can say that $\operatorname{Step}$ holds for $x_{1}$ and $x_{2}$.
FreeAddGroup.addEquivIntOfUniquedefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the additive equivalence integer (from the name)
English
The additive equivalence integer is an additive equivalence of the set of free additive groups of $x$ and $\Integer$.
FreeAddGroup.freeAddGroupCongrdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the free additive group congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the free additive group congruence of $e$ is an additive equivalence of the set of free additive groups of $x$ and the set of free additive groups of $x_{1}$.
FreeAddGroup.freeAddGroupEquivAdditivedefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
$\operatorname{freeAddGroupEquivAdditive}$ is an additive equivalence of the set of free additive groups of $x$ and $\mathrm{Additive}$ applied to the set of free groups of $x$.
FreeAddGroup.liftdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of additive monoid homomorphisms of the set of free additive groups of $x$ and $x_{1}$.
FreeAddGroup.mapdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is an additive monoid homomorphism of the set of free additive groups of $x$ and the set of free additive groups of $x_{1}$.
FreeAddGroup.mkdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
Let $L$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{mk}$ applied to $L$ is a free additive group of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Step}$ and $L$.
FreeAddGroup.negRevdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
Let $w$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{negRev}$ applied to $w$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{reverse}$ applied to $\operatorname{map}$ applied to the function that maps $g$ to $\ProdmkMACRoU {\ProdfstMACRoZ {g}}{\operatorname{not} (\ProdsndMACRoAA {g})}$ and $w$.
FreeAddGroup.ofdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free additive group of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{cons}$ applied to $\ProdmkMACRoU {x_{1}}{\operatorname{true}}$ and $\operatorname{nil}$.
FreeAddGroup.sumdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the sum (from the name)
English
The sum is an additive monoid homomorphism of the set of free additive groups of $x$ and $x$ defined as $\operatorname{lift}$ applied to $\mathrm{id}$.
FreeGroupdefMathlib.GroupTheory.FreeGroup.Basic, type
Wording
free group of x (from the name)
English
Let $x$ be a set. Then a free group of $x$ is an element of the function that maps $x$ to $\mathrm{Quot}$ applied to $\operatorname{Step}$.
FreeGroup.IsReduceddefMathlib.GroupTheory.FreeGroup.Basic, predicate
Wording
L is reduced (from the name)
English
Let $L$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $L$ is reduced, if $\operatorname{IsChain}$ holds for the function that maps $a$ and $b$ to the proposition that if $\EqtMACRoH {\ProdfstMACRoZ {a}}{\ProdfstMACRoZ {b}}$, then $\EqtMACRoH {\ProdsndMACRoAA {a}}{\ProdsndMACRoAA {b}}$ and $L$.
FreeGroup.ReddefMathlib.GroupTheory.FreeGroup.Basic, predicate
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be lists of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{Red}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{ReflTransGen}$ holds for $\operatorname{Step}$, $x_{1}$ and $x_{2}$.
FreeGroup.Red.StepinductiveMathlib.GroupTheory.FreeGroup.Basic, predicate
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be lists of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then we can say that $\operatorname{Step}$ holds for $x_{1}$ and $x_{2}$.
FreeGroup.equivIntOfUniquedefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the bijection between the free group (from the docstring)
English
The bijection between the free group is an equivalence from the set of free groups of $x$ to $\Integer$.
FreeGroup.freeGroupCongrdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the free group congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the free group congruence of $e$ is a multiplicative equivalence of the set of free groups of $x$ and the set of free groups of $x_{1}$.
FreeGroup.freeGroupEquivMultiplicativedefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the free group equivalence multiplicative (from the name)
English
The free group equivalence multiplicative is a multiplicative equivalence of the set of free groups of $x$ and the set of multiplicatives of the set of free additive groups of $x$.
FreeGroup.freeGroupUnitEquivIntdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the free group unit equivalence integer (from the name)
English
The free group unit equivalence integer is an equivalence from the set of free groups of $\mathrm{Unit}$ to $\Integer$.
FreeGroup.invRevdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
Let $w$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{invRev}$ applied to $w$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{reverse}$ applied to $\operatorname{map}$ applied to the function that maps $g$ to $\ProdmkMACRoU {\ProdfstMACRoZ {g}}{\operatorname{not} (\ProdsndMACRoAA {g})}$ and $w$.
FreeGroup.liftdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of monoid homomorphisms of the set of free groups of $x$ and $x_{1}$.
FreeGroup.mapdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a monoid homomorphism of the set of free groups of $x$ and the set of free groups of $x_{1}$.
FreeGroup.mkdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
Let $L$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{mk}$ applied to $L$ is a free group of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Step}$ and $L$.
FreeGroup.mulEquivIntOfUniquedefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the isomorphism between the free group (from the docstring)
English
The isomorphism between the free group is a multiplicative equivalence of the set of free groups of $x$ and the set of multiplicatives of $\Integer$.
FreeGroup.ofdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{of}$ applied to $x_{1}$ is a free group of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{cons}$ applied to $\ProdmkMACRoU {x_{1}}{\operatorname{true}}$ and $\operatorname{nil}$.
FreeGroup.proddefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the product (from the name)
English
The product is a monoid homomorphism of the set of free groups of $x$ and $x$ defined as $\operatorname{lift}$ applied to $\mathrm{id}$.
FreeGroup.sumdefMathlib.GroupTheory.FreeGroup.Basic, function or constant
Wording
the sum of x2 (from the name)
English
Let $x_{2}$ be a free group of $x$. Then the sum of $x_{2}$ is an element of $x$ defined as $\operatorname{prod}$ applied to $x_{2}$.

Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

FreeAddGroup.IsCyclicallyReduceddefMathlib.GroupTheory.FreeGroup.CyclicallyReduced, predicate
Wording
L is cyclically reduced (from the name)
English
generation took over the time limit
FreeAddGroup.reduceCyclicallydefMathlib.GroupTheory.FreeGroup.CyclicallyReduced, function or constant
Wording
no wording
English
Let $x_{2}$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{reduceCyclically}$ applied to $x_{2}$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{bidirectionalRec}$ applied to $\operatorname{nil}$, the function that maps $x_{3}$ to $\operatorname{cons}$ applied to $x_{3}$ and $\operatorname{nil}$, the function that maps $a$, $L$, $b$ and $\mathrm{rC}$ to $\iteMACRoG {\mathrm{and} (\EqtMACRoH {\ProdfstMACRoZ {b}}{\ProdfstMACRoZ {a}}, \EqtMACRoH {\operatorname{not} (\ProdsndMACRoAA {b})}{\ProdsndMACRoAA {a}})}{\mathrm{rC}}{\operatorname{hAppend} (\operatorname{cons} (a , L), \operatorname{cons} (b , \operatorname{nil}))}$ and $x_{2}$.
FreeAddGroup.reduceCyclically.conjugatordefMathlib.GroupTheory.FreeGroup.CyclicallyReduced, function or constant
Wording
no wording
English
Let $x_{2}$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{conjugator}$ applied to $x_{2}$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{bidirectionalRec}$ applied to $\operatorname{nil}$, the function that maps $x_{3}$ to $\operatorname{nil}$, the function that maps $a$, $x_{4}$, $b$ and $\mathrm{rCC}$ to $\iteMACRoG {\mathrm{and} (\EqtMACRoH {\ProdfstMACRoZ {b}}{\ProdfstMACRoZ {a}}, \EqtMACRoH {\operatorname{not} (\ProdsndMACRoAA {b})}{\ProdsndMACRoAA {a}})}{\operatorname{cons} (a , \mathrm{rCC})}{\operatorname{nil}}$ and $x_{2}$.
FreeGroup.IsCyclicallyReduceddefMathlib.GroupTheory.FreeGroup.CyclicallyReduced, predicate
Wording
L is cyclically reduced (from the name)
English
generation took over the time limit
FreeGroup.reduceCyclicallydefMathlib.GroupTheory.FreeGroup.CyclicallyReduced, function or constant
Wording
no wording
English
Let $x_{2}$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{reduceCyclically}$ applied to $x_{2}$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{bidirectionalRec}$ applied to $\operatorname{nil}$, the function that maps $x_{3}$ to $\operatorname{cons}$ applied to $x_{3}$ and $\operatorname{nil}$, the function that maps $a$, $L$, $b$ and $\mathrm{rC}$ to $\iteMACRoG {\mathrm{and} (\EqtMACRoH {\ProdfstMACRoZ {b}}{\ProdfstMACRoZ {a}}, \EqtMACRoH {\operatorname{not} (\ProdsndMACRoAA {b})}{\ProdsndMACRoAA {a}})}{\mathrm{rC}}{\operatorname{hAppend} (\operatorname{cons} (a , L), \operatorname{cons} (b , \operatorname{nil}))}$ and $x_{2}$.
FreeGroup.reduceCyclically.conjugatordefMathlib.GroupTheory.FreeGroup.CyclicallyReduced, function or constant
Wording
no wording
English
Let $x_{2}$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{conjugator}$ applied to $x_{2}$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{bidirectionalRec}$ applied to $\operatorname{nil}$, the function that maps $x_{3}$ to $\operatorname{nil}$, the function that maps $a$, $x_{4}$, $b$ and $\mathrm{rCC}$ to $\iteMACRoG {\mathrm{and} (\EqtMACRoH {\ProdfstMACRoZ {b}}{\ProdfstMACRoZ {a}}, \EqtMACRoH {\operatorname{not} (\ProdsndMACRoAA {b})}{\ProdsndMACRoAA {a}})}{\operatorname{cons} (a , \mathrm{rCC})}{\operatorname{nil}}$ and $x_{2}$.

Mathlib.GroupTheory.FreeGroup.GeneratorEquiv

Equiv.ofFreeAbelianGroupEquivdefMathlib.GroupTheory.FreeGroup.GeneratorEquiv, function or constant
Wording
the equivalence of e (from the name)
English
Let $e$ be an additive equivalence of the set of free Abelian groups of $x$ and the set of free Abelian groups of $x_{1}$. Then the equivalence of $e$ is an equivalence from $x$ to $x_{1}$ defined as the equivalence of the integer linear equivalence of $e$.
Equiv.ofFreeAbelianGroupLinearEquivdefMathlib.GroupTheory.FreeGroup.GeneratorEquiv, function or constant
Wording
the equivalence of e (from the name)
English
Let $e$ be a linear equivalence of the set of free Abelian groups of $x$ and the set of free Abelian groups of $x_{1}$. Then the equivalence of $e$ is an equivalence from $x$ to $x_{1}$ defined as the index equivalence of the map of the basis of $x$ and $e$ and the basis of $x_{1}$.
Equiv.ofFreeGroupEquivdefMathlib.GroupTheory.FreeGroup.GeneratorEquiv, function or constant
Wording
the equivalence of e (from the name)
English
Let $e$ be a multiplicative equivalence of the set of free groups of $x$ and the set of free groups of $x_{1}$. Then the equivalence of $e$ is an equivalence from $x$ to $x_{1}$ defined as the equivalence of $\operatorname{toAdditive}$ applied to the abelianization congruence of $e$.
Equiv.ofIsFreeGroupEquivdefMathlib.GroupTheory.FreeGroup.GeneratorEquiv, function or constant
Wording
the equivalence of e (from the name)
English
Let $e$ be a multiplicative equivalence of $G$ and $H$. Then the equivalence of $e$ is an equivalence from the set of generators of $G$ to the set of generators of $H$ defined as the equivalence of the composition of the inverse of the free group of $G$ and the composition of $e$ and the free group of $H$.
FreeAbelianGroup.basisdefMathlib.GroupTheory.FreeGroup.GeneratorEquiv, function or constant
Wording
the basis of x (from the name)
English
Let $x$ be a set. Then the basis of $x$ is a basis of $\Integer$ and the set of free Abelian groups of $x$ defined as $\operatorname{ofRepr}$ applied to the integer linear equivalence of the equivalence finitely supported function of $x$.

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

FreeAddGroupBasisstructureMathlib.GroupTheory.FreeGroup.IsFreeGroup, type
Wording
free additive group basis of x and G (from the name)
English
Let $x$ and $G$ be sets. Then the free additive group bases of $x$ and $G$ are a basic type.
FreeAddGroupBasis.freeGroupBasisdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free group basis of b (from the name)
English
Let $b$ be a free additive group basis of $x$ and $G$. Then the free group basis of $b$ is a free group basis of $x$ and the set of multiplicatives of $G$ defined as $\operatorname{ofRepr}$ applied to the composition of $\operatorname{toMultiplicative}$ applied to the representation of $b$ and the inverse of the free group equivalence multiplicative.
FreeAddGroupBasis.liftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the lift of b (from the name)
English
Let $b$ be a free additive group basis of $x$ and $G$. Then the lift of $b$ is an equivalence from the set of functions from elements of $x$ to elements of $H$ to the set of additive monoid homomorphisms of $G$ and $H$.
FreeAddGroupBasis.mapdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the map of b and e (from the name)
English
Let $b$ be a free additive group basis of $x$ and $G$. Let $e$ be an additive equivalence of $G$ and $H$. Then the map of $b$ and $e$ is a free additive group basis of $x$ and $H$ defined as $\operatorname{ofRepr}$ applied to the composition of the inverse of $e$ and the representation of $b$.
FreeAddGroupBasis.ofFreeAddGroupdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the canonical basis of the additive free group over X (from the docstring)
English
Let $X$ be a set. Then the canonical basis of the additive free group over $X$ is a free additive group basis of $X$ and the set of free additive groups of $X$ defined as $\operatorname{ofRepr}$ applied to the identity map of the set of free additive groups of $X$.
FreeAddGroupBasis.ofLiftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free additive group basis of of and lift (from the name)
English
Let $X$ be a set. Let $\mathrm{of}$ be a function from elements of $X$ to elements of $G$. Let $\mathrm{lift}$ be a function from sets $H_{1}$ and elements $x_{5}$ of $\mathrm{Proof}$ applied to the proposition that $H_{1}$ is an additive group to equivalences from the set of functions from elements of $X$ to elements of $H_{1}$ to the set of additive monoid homomorphisms of $G$ and $H_{1}$ such that for all sets $H$, for all elements $x_{1}$ of $\mathrm{AddGroup}$ applied to $H$, for all functions $f$ from elements of $X$ to elements of $H$, for all elements $a$ of $X$, $\EqtMACRoH {\operatorname{coe} (\mathrm{lift} (H , x_{1}), f , \mathrm{of} (a))}{f (a)}$. Then the free additive group basis of $\mathrm{of}$ and $H_{1}$ is a free additive group basis of $X$ and $G$.
FreeAddGroupBasis.ofUniqueLiftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free additive group basis of of (from the name)
English
Let $X$ be a set. Let $\mathrm{of}$ be a function from elements of $X$ to elements of $G$ such that for all sets $H$, for all elements $x_{1}$ of $\mathrm{AddGroup}$ applied to $H$, for all functions $f$ from elements of $X$ to elements of $H$, $\mathrm{ExistsUnique}$ holds for the function that maps $F$ to the proposition that for all elements $a$ of $X$, $\EqtMACRoH {F (\mathrm{of} (a))}{f (a)}$. Then the free additive group basis of $\mathrm{of}$ is a free additive group basis of $X$ and $G$.
FreeAddGroupBasis.reindexdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the reindexing of b and e (from the name)
English
Let $b$ be a free additive group basis of $x$ and $G$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the reindexing of $b$ and $e$ is a free additive group basis of $x_{1}$ and $G$ defined as $\operatorname{ofRepr}$ applied to the composition of the representation of $b$ and the free additive group congruence of $e$.
FreeAddGroupBasis.reprdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the representation of self (from the name)
English
Let $\mathrm{self}$ be a free additive group basis of $x$ and $G$. Then the representation of $\mathrm{self}$ is an additive equivalence of $G$ and the set of free additive groups of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FreeGroupBasisstructureMathlib.GroupTheory.FreeGroup.IsFreeGroup, type
Wording
free group basis of x and G (from the name)
English
Let $x$ and $G$ be sets. Then the free group bases of $x$ and $G$ are a basic type.
FreeGroupBasis.freeAddGroupBasisdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free additive group basis of b (from the name)
English
Let $b$ be a free group basis of $x$ and $G$. Then the free additive group basis of $b$ is a free additive group basis of $x$ and $\mathrm{Additive}$ applied to $G$ defined as $\operatorname{ofRepr}$ applied to the composition of $\operatorname{toAdditive}$ applied to the representation of $b$ and the inverse of $\operatorname{freeAddGroupEquivAdditive}$.
FreeGroupBasis.liftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the lift of b (from the name)
English
Let $b$ be a free group basis of $x$ and $G$. Then the lift of $b$ is an equivalence from the set of functions from elements of $x$ to elements of $H$ to the set of monoid homomorphisms of $G$ and $H$.
FreeGroupBasis.mapdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the map of b and e (from the name)
English
Let $b$ be a free group basis of $x$ and $G$. Let $e$ be a multiplicative equivalence of $G$ and $H$. Then the map of $b$ and $e$ is a free group basis of $x$ and $H$ defined as $\operatorname{ofRepr}$ applied to the composition of the inverse of $e$ and the representation of $b$.
FreeGroupBasis.ofFreeGroupdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the canonical basis of the free group over X (from the docstring)
English
Let $X$ be a set. Then the canonical basis of the free group over $X$ is a free group basis of $X$ and the set of free groups of $X$ defined as $\operatorname{ofRepr}$ applied to the identity map of the set of free groups of $X$.
FreeGroupBasis.ofLiftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free group basis of of and lift (from the name)
English
Let $X$ be a set. Let $\mathrm{of}$ be a function from elements of $X$ to elements of $G$. Let $\mathrm{lift}$ be a function from sets $H_{1}$ and elements $x_{5}$ of $\mathrm{Proof}$ applied to the proposition that $H_{1}$ is a group to equivalences from the set of functions from elements of $X$ to elements of $H_{1}$ to the set of monoid homomorphisms of $G$ and $H_{1}$ such that for all sets $H$, for all elements $x_{1}$ of $\mathrm{Group}$ applied to $H$, for all functions $f$ from elements of $X$ to elements of $H$, for all elements $a$ of $X$, $\EqtMACRoH {\operatorname{coe} (\mathrm{lift} (H , x_{1}), f , \mathrm{of} (a))}{f (a)}$. Then the free group basis of $\mathrm{of}$ and $H_{1}$ is a free group basis of $X$ and $G$.
FreeGroupBasis.ofUniqueLiftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free group basis of of (from the name)
English
Let $X$ be a set. Let $\mathrm{of}$ be a function from elements of $X$ to elements of $G$ such that for all sets $H$, for all elements $x_{1}$ of $\mathrm{Group}$ applied to $H$, for all functions $f$ from elements of $X$ to elements of $H$, $\mathrm{ExistsUnique}$ holds for the function that maps $F$ to the proposition that for all elements $a$ of $X$, $\EqtMACRoH {F (\mathrm{of} (a))}{f (a)}$. Then the free group basis of $\mathrm{of}$ is a free group basis of $X$ and $G$.
FreeGroupBasis.reindexdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the reindexing of b and e (from the name)
English
Let $b$ be a free group basis of $x$ and $G$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the reindexing of $b$ and $e$ is a free group basis of $x_{1}$ and $G$ defined as $\operatorname{ofRepr}$ applied to the composition of the representation of $b$ and the free group congruence of $e$.
FreeGroupBasis.reprdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the representation of self (from the name)
English
Let $\mathrm{self}$ be a free group basis of $x$ and $G$. Then the representation of $\mathrm{self}$ is a multiplicative equivalence of $G$ and the set of free groups of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
IsFreeAddGroupclassMathlib.GroupTheory.FreeGroup.IsFreeGroup, predicate
Wording
G is free (from the docstring)
English
Let $G$ be a set. Then we can say that $G$ is free.
IsFreeAddGroup.GeneratorsdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, type
Wording
generator of G (from the name)
English
Let $G$ be a set. Then a generator of $G$ is an element of the function that maps $G$ to $\operatorname{choose}$ applied to $\mathrm{IsFreeAddGroup\_\_nonempty\_basis}$.
IsFreeAddGroup.addEquivdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the additive equivalence of G (from the name)
English
Let $G$ be a set. Then the additive equivalence of $G$ is an additive equivalence of the set of free additive groups of the set of generators of $G$ and $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{IsFreeGroup\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_GroupTheory\_\_FreeGroup\_\_IsFreeGroup\_\_3799744388\_\_\_hygCtx\_\_\_hyg\_\_19}$ and $G$.
IsFreeAddGroup.basisdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the basis of G (from the name)
English
Let $G$ be a set. Then the basis of $G$ is a free additive group basis of the set of generators of $G$ and $G$ defined as $\operatorname{ofRepr}$ applied to the inverse of the additive equivalence of $G$.
IsFreeAddGroup.liftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from generators of $G$ to elements of $H$ to the set of additive monoid homomorphisms of $G$ and $H$ defined as the lift of the basis of $G$.
IsFreeAddGroup.ofdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
no wording
English
Let $x_{1}$ be a generator of $G$. Then $\operatorname{of}$ applied to $x_{1}$ is an element of $G$ defined as $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toEquiv}$ applied to the additive equivalence of $G$, $\operatorname{of}$ and $x_{1}$.
IsFreeAddGroup.toFreeAddGroupdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free additive group of G (from the name)
English
Let $G$ be a set. Then the free additive group of $G$ is an additive equivalence of $G$ and the set of free additive groups of the set of generators of $G$ defined as the inverse of the additive equivalence of $G$.
IsFreeGroupclassMathlib.GroupTheory.FreeGroup.IsFreeGroup, predicate
Wording
G is free (from the docstring)
English
Let $G$ be a set. Then we can say that $G$ is free.
IsFreeGroup.GeneratorsdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, type
Wording
generator of G (from the name)
English
Let $G$ be a set. Then a generator of $G$ is an element of the function that maps $G$ to $\operatorname{choose}$ applied to $\mathrm{IsFreeGroup\_\_nonempty\_basis}$.
IsFreeGroup.basisdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the basis of G (from the name)
English
Let $G$ be a set. Then the basis of $G$ is a free group basis of the set of generators of $G$ and $G$ defined as $\operatorname{ofRepr}$ applied to the inverse of the multiplicative equivalence of $G$.
IsFreeGroup.liftdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the lift (from the name)
English
The lift is an equivalence from the set of functions from generators of $G$ to elements of $H$ to the set of monoid homomorphisms of $G$ and $H$ defined as the lift of the basis of $G$.
IsFreeGroup.mulEquivdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the multiplicative equivalence of G (from the name)
English
Let $G$ be a set. Then the multiplicative equivalence of $G$ is a multiplicative equivalence of the set of free groups of the set of generators of $G$ and $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{IsFreeGroup\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_GroupTheory\_\_FreeGroup\_\_IsFreeGroup\_\_3799744388\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $G$.
IsFreeGroup.ofdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
no wording
English
Let $x_{1}$ be a generator of $G$. Then $\operatorname{of}$ applied to $x_{1}$ is an element of $G$ defined as $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toEquiv}$ applied to the multiplicative equivalence of $G$, $\operatorname{of}$ and $x_{1}$.
IsFreeGroup.toFreeGroupdefMathlib.GroupTheory.FreeGroup.IsFreeGroup, function or constant
Wording
the free group of G (from the name)
English
Let $G$ be a set. Then the free group of $G$ is a multiplicative equivalence of $G$ and the set of free groups of the set of generators of $G$ defined as the inverse of the multiplicative equivalence of $G$.

‹ previous next ›