Definitions: Mathlib.GroupTheory, part 2 of 3

IsFreeGroupoid.SpanningTree.functorOfMonoidHomdefMathlib.GroupTheory.FreeGroup.NielsenSchreier, function or constant

Wording

the functor of T and f (from the name)

English

Let $T$ be a wide subquiver of $\operatorname{Symmetrify}$ applied to the set of generators of $G$. Let $f$ be a monoid homomorphism of the set of ends of $\mathrm{\_private\_\_Mathlib\_\_GroupTheory\_\_FreeGroup\_\_NielsenSchreier\_\_0\_\_IsFreeGroupoid\_\_SpanningTree\_\_root'}$ applied to $T$ and $X$. Then the functor of $T$ and $f$ is a functor of $G$ and the set of single objects of $X$.

IsFreeGroupoid.SpanningTree.homOfPathdefMathlib.GroupTheory.FreeGroup.NielsenSchreier, function or constant

Wording

the homomorphism of T and x3 (from the name)

English

Let $T$ be a wide subquiver of $\operatorname{Symmetrify}$ applied to the set of generators of $G$. Let $x_{3}$ be a path of the root of the set of types of $\operatorname{Symmetrify}$ applied to the set of generators of $G$ and $T$ and $a$. Then the homomorphism of $T$ and $x_{3}$ is a homomorphism of $\mathrm{\_private\_\_Mathlib\_\_GroupTheory\_\_FreeGroup\_\_NielsenSchreier\_\_0\_\_IsFreeGroupoid\_\_SpanningTree\_\_root'}$ applied to $T$ and $a$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{IsFreeGroupoid\_\_SpanningTree\_\_homOfPath\_\_\_f}$ applied to $T$.

IsFreeGroupoid.SpanningTree.loopOfHomdefMathlib.GroupTheory.FreeGroup.NielsenSchreier, function or constant

Wording

the loop of T and p (from the name)

English

Let $T$ be a wide subquiver of $\operatorname{Symmetrify}$ applied to the set of generators of $G$. Let $p$ be a homomorphism of $a$ and $b$. Then the loop of $T$ and $p$ is an end of $\mathrm{\_private\_\_Mathlib\_\_GroupTheory\_\_FreeGroup\_\_NielsenSchreier\_\_0\_\_IsFreeGroupoid\_\_SpanningTree\_\_root'}$ applied to $T$ defined as $\operatorname{of}$ applied to the composition of the tree homomorphism of $T$ and $a$ and the composition of $p$ and the inverse of the tree homomorphism of $T$ and $b$.

IsFreeGroupoid.SpanningTree.treeHomdefMathlib.GroupTheory.FreeGroup.NielsenSchreier, function or constant

Wording

the tree homomorphism of T and a (from the name)

English

Let $T$ be a wide subquiver of $\operatorname{Symmetrify}$ applied to the set of generators of $G$. Let $a$ be an element of $G$. Then the tree homomorphism of $T$ and $a$ is a homomorphism of $\mathrm{\_private\_\_Mathlib\_\_GroupTheory\_\_FreeGroup\_\_NielsenSchreier\_\_0\_\_IsFreeGroupoid\_\_SpanningTree\_\_root'}$ applied to $T$ and $a$ defined as the homomorphism of $T$ and $\operatorname{default}$.

IsFreeGroupoid.ofdefMathlib.GroupTheory.FreeGroup.NielsenSchreier, function or constant

Wording

no wording

English

Let $x_{1}$ be a homomorphism of $a$ and $b$. Then $\operatorname{of}$ applied to $x_{1}$ is a homomorphism of $a$ and $b$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

Mathlib.GroupTheory.FreeGroup.Orbit

FreeGroup.startsWithdefMathlib.GroupTheory.FreeGroup.Orbit, function or constant

Wording

no wording

English

Let $w$ be an element of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{startsWith}$ applied to $w$ is an element of the power set of the set of free groups of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $g$ to the proposition that $\mathrm{GetElem?\_\_getElem?}$ applied to the word of $g$ and $0$ is equal to $\operatorname{some}$ applied to $w$.

Mathlib.GroupTheory.FreeGroup.Reduce

FreeAddGroup.normdefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

the norm of x2 (from the name)

English

Let $x_{2}$ be a free additive group of $x$. Then the norm of $x_{2}$ is a natural number defined as $\operatorname{length}$ applied to the word of $x_{2}$.

FreeAddGroup.reducedefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

the maximal reduction of L (from the docstring)

English

Let $L$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then the maximal reduction of $L$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$.

FreeAddGroup.reduce.churchRosserdefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

no wording

English

Assume that $\operatorname{Red}$ holds for $x_{1}$ and $x_{2}$. Assume that $\operatorname{Red}$ holds for $x_{1}$ and $x_{3}$. Then $\operatorname{churchRosser}$ applied to $H_{12}$ and $H_{13}$ is an element of $\SubtypeSet {x_{5}}{\mathrm{and} (\operatorname{Red} (x_{2} , x_{5}), \operatorname{Red} (x_{3} , x_{5}))}$ defined as the maximal reduction of $x_{1}$.

FreeAddGroup.toWorddefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

the word of x2 (from the name)

English

Let $x_{2}$ be a free additive group of $x$. Then the word of $x_{2}$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{lift}$ applied to $\operatorname{reduce}$, the function that maps $x_{2}$, $x_{3}$ and $H$ to $\operatorname{eq}$ applied to $H$ and $x_{2}$.

FreeGroup.Red.enumdefMathlib.GroupTheory.FreeGroup.Reduce, 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{enum}$ applied to $x_{2}$ is a list of lists of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{filter}$ applied to the function that maps $b$ to $\operatorname{decide}$ applied to $\operatorname{Red}$ applied to $x_{2}$ and $b$ and $\operatorname{sublists}$ applied to $x_{2}$.

FreeGroup.normdefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

the norm of x2 (from the name)

English

Let $x_{2}$ be a free group of $x$. Then the norm of $x_{2}$ is a natural number defined as $\operatorname{length}$ applied to the word of $x_{2}$.

FreeGroup.reducedefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

the maximal reduction of L (from the docstring)

English

Let $L$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then the maximal reduction of $L$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$.

FreeGroup.reduce.churchRosserdefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

no wording

English

FreeGroup.toWorddefMathlib.GroupTheory.FreeGroup.Reduce, function or constant

Wording

the word of x2 (from the name)

English

Let $x_{2}$ be a free group of $x$. Then the word of $x_{2}$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$ defined as $\operatorname{lift}$ applied to $\operatorname{reduce}$, the function that maps $x_{2}$, $x_{3}$ and $H$ to $\operatorname{eq}$ applied to $H$ and $x_{2}$.

Mathlib.GroupTheory.Generators

Group.GeneratorsstructureMathlib.GroupTheory.Generators, type

Wording

generator of G and x1 (from the name)

English

Let $G$ and $x_{1}$ be sets. Then the generators of $G$ and $x_{1}$ are a basic type.

Group.Generators.liftdefMathlib.GroupTheory.Generators, function or constant

Wording

the lift of P (from the name)

English

Let $P$ be a generator of $G$ and $x$. Then the lift of $P$ is a monoid homomorphism of the set of free groups of $x$ and $G$ defined as $\operatorname{lift}$ applied to $\operatorname{val}$ applied to $P$.

Group.Generators.mapdefMathlib.GroupTheory.Generators, function or constant

Wording

the map of P and f (from the name)

English

Let $P$ be a generator of $G$ and $x$. Let $f$ be a monoid homomorphism of $G$ and $H$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the map of $P$ and $f$ is a generator of $H$ and $x$.

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

Wording

the generator of x2 and h (from the name)

English

Let $x_{2}$ be a monoid homomorphism of the set of free groups of $x$ and $G$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{2}$. Then the generator of $x_{2}$ and $h$ is a generator of $G$ and $x$.

Group.Generators.ofSetdefMathlib.GroupTheory.Generators, function or constant

Wording

the generator of h (from the name)

English

Assume that the closure of $S$ is equal to the top. Then the generator of $h$ is a generator of $G$ and the set of elements of $S$.

Group.Generators.reindexdefMathlib.GroupTheory.Generators, function or constant

Wording

the reindexing of P and he (from the name)

English

Let $P$ be a generator of $G$ and $x$. Assume that $\operatorname{Surjective}$ holds for $e$. Then the reindexing of $P$ and $\mathrm{he}$ is a generator of $G$ and $x_{1}$.

Group.Generators.valdefMathlib.GroupTheory.Generators, function or constant

Wording

the value of self and x2 (from the name)

English

Let $\mathrm{self}$ be a generator of $G$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then the value of $\mathrm{self}$ and $x_{2}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Mathlib.GroupTheory.Goursat

AddSubgroup.goursatFstdefMathlib.GroupTheory.Goursat, function or constant

Wording

no wording

English

Let $I$ be an additive subgroup of $\mathrm{Prod}$ applied to $G$ and $H$. Then $\operatorname{goursatFst}$ applied to $I$ is an additive subgroup of $G$ defined as the map of the composition of the first component of $G$ and $H$ and the subtype of $I$ and the additive kernel of the composition of the second component of $G$ and $H$ and the subtype of $I$.

AddSubgroup.goursatSnddefMathlib.GroupTheory.Goursat, function or constant

Wording

no wording

English

Let $I$ be an additive subgroup of $\mathrm{Prod}$ applied to $G$ and $H$. Then $\operatorname{goursatSnd}$ applied to $I$ is an additive subgroup of $H$ defined as the map of the composition of the second component of $G$ and $H$ and the subtype of $I$ and the additive kernel of the composition of the first component of $G$ and $H$ and the subtype of $I$.

Subgroup.goursatFstdefMathlib.GroupTheory.Goursat, function or constant

Wording

no wording

English

Let $I$ be a subgroup of $\mathrm{Prod}$ applied to $G$ and $H$. Then $\operatorname{goursatFst}$ applied to $I$ is a subgroup of $G$ defined as the map of the composition of the first component of $G$ and $H$ and the subtype of $I$ and the multiplicative kernel of the composition of the second component of $G$ and $H$ and the subtype of $I$.

Subgroup.goursatSnddefMathlib.GroupTheory.Goursat, function or constant

Wording

no wording

English

Let $I$ be a subgroup of $\mathrm{Prod}$ applied to $G$ and $H$. Then $\operatorname{goursatSnd}$ applied to $I$ is a subgroup of $H$ defined as the map of the composition of the second component of $G$ and $H$ and the subtype of $I$ and the multiplicative kernel of the composition of the first component of $G$ and $H$ and the subtype of $I$.

Mathlib.GroupTheory.GroupAction.Basic

AddAction.stabilizerEquivStabilizerdefMathlib.GroupTheory.GroupAction.Basic, function or constant

Wording

the stabilizer equivalence stabilizer of hg (from the name)

English

Assume that $\EqtMACRoH {b}{\operatorname{hVAdd} (g , a)}$. Then the stabilizer equivalence stabilizer of $\mathrm{hg}$ is an additive equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , a)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{4}})}$.

AddAction.stabilizerEquivStabilizerOfOrbitReldefMathlib.GroupTheory.GroupAction.Basic, function or constant

Wording

the stabilizer equivalence stabilizer of h (from the name)

English

Assume that $\operatorname{r}$ holds for $a$ and $b$. Then the stabilizer equivalence stabilizer of $h$ is an additive equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , a)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{4}})}$.

MulAction.stabilizerEquivStabilizerdefMathlib.GroupTheory.GroupAction.Basic, function or constant

Wording

the stabilizer equivalence stabilizer of hg (from the name)

English

Assume that $\EqtMACRoH {b}{\HSMulhSMulMACRoAL {g}{a}}$. Then the stabilizer equivalence stabilizer of $\mathrm{hg}$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , a)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{4}})}$.

MulAction.stabilizerEquivStabilizerOfOrbitReldefMathlib.GroupTheory.GroupAction.Basic, function or constant

Wording

the stabilizer equivalence stabilizer of h (from the name)

English

Assume that $\operatorname{r}$ holds for $a$ and $b$. Then the stabilizer equivalence stabilizer of $h$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , a)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{4}})}$.

Mathlib.GroupTheory.GroupAction.Blocks

AddAction.BlockMemdefMathlib.GroupTheory.GroupAction.Blocks, type

Wording

block membership of G and a (from the name)

English

Let $G$ be a set. Let $a$ be an element of $X$. Then a block membership of $G$ and $a$ is an element of the function that maps $G$ and $a$ to $\SubtypeSet {B}{\mathrm{and} (\MembershipmemMACRoT {B}{a}, \operatorname{IsBlock} (B))}$.

AddAction.IsBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a block (from the name)

English

Let $G$ be a set. Let $B$ be an element of $\wp X$. Then $B$ is a block, if for all elements $x_{1}$ and $x_{2}$ of $G$, if the sum of $x_{1}$ and $B$ is distinct from the sum of $x_{2}$ and $B$, then the sum of $x_{1}$ and $B$ is disjoint to the sum of $x_{2}$ and $B$.

AddAction.IsBlockSystemdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

x2 is a block system (from the name)

English

Let $G$ be a set. Let $x_{2}$ be an element of $\wp (\wp X)$. Then $x_{2}$ is a block system, if $x_{2}$ is a partition and for all elements $B$ of $\wp X$, if $B$ is an element of $x_{2}$, then $B$ is a block.

AddAction.IsFixedBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a fixed block (from the name)

English

Let $G$ be a set. Let $B$ be an element of $\wp X$. Then $B$ is a fixed block, if for all elements $g$ of $G$, the sum of $g$ and $B$ is equal to $B$.

AddAction.IsInvariantBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a invariant block (from the name)

English

Let $G$ be a set. Let $B$ be an element of $\wp X$. Then $B$ is an invariant block, if for all elements $g$ of $G$, the sum of $g$ and $B$ is less than or equal to $B$.

AddAction.IsTrivialBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a trivial block (from the name)

English

Let $B$ be an element of $\wp X$. Then $B$ is a trivial block, if $B$ is a subsingleton or $B$ is equal to the universal set.

AddAction.block_stabilizerOrderIsodefMathlib.GroupTheory.GroupAction.Blocks, function or constant

Wording

the block stabilizer order isomorphism of G and a (from the name)

English

Let $G$ be a set. Let $a$ be an element of $X$. Then the block stabilizer order isomorphism of $G$ and $a$ is an order isomorphism of $\SubtypeSet {B}{\mathrm{and} (\MembershipmemMACRoT {B}{a}, \operatorname{IsBlock} (B))}$ and the set of elements of $\operatorname{Ici}$ applied to the stabilizer of $G$ and $a$.

MulAction.BlockMemdefMathlib.GroupTheory.GroupAction.Blocks, type

Wording

block membership of G and a (from the name)

English

MulAction.IsBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a block (from the name)

English

Let $G$ be a set. Let $B$ be an element of $\wp X$. Then $B$ is a block, if for all elements $x_{1}$ and $x_{2}$ of $G$, if $\HSMulhSMulMACRoAL {x_{1}}{B}\neq \HSMulhSMulMACRoAL {x_{2}}{B}$, then $\HSMulhSMulMACRoAL {x_{1}}{B}$ is disjoint to $\HSMulhSMulMACRoAL {x_{2}}{B}$.

MulAction.IsBlockSystemdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

x2 is a block system (from the name)

English

MulAction.IsFixedBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a fixed block (from the name)

English

Let $G$ be a set. Let $B$ be an element of $\wp X$. Then $B$ is a fixed block, if for all elements $g$ of $G$, $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{B}}{B}$.

MulAction.IsInvariantBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a invariant block (from the name)

English

Let $G$ be a set. Let $B$ be an element of $\wp X$. Then $B$ is an invariant block, if for all elements $g$ of $G$, $\HSMulhSMulMACRoAL {g}{B}\leq B$.

MulAction.IsTrivialBlockdefMathlib.GroupTheory.GroupAction.Blocks, predicate

Wording

B is a trivial block (from the name)

English

Let $B$ be an element of $\wp X$. Then $B$ is a trivial block, if $B$ is a subsingleton or $B$ is equal to the universal set.

MulAction.block_stabilizerOrderIsodefMathlib.GroupTheory.GroupAction.Blocks, function or constant

Wording

the block stabilizer order isomorphism of G and a (from the name)

English

Mathlib.GroupTheory.GroupAction.ConjAct

ConjActdefMathlib.GroupTheory.GroupAction.ConjAct, type

Wording

no wording

English

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

ConjAct.ofConjActdefMathlib.GroupTheory.GroupAction.ConjAct, function or constant

Wording

no wording

English

$\operatorname{ofConjAct}$ is a multiplicative equivalence of $\mathrm{ConjAct}$ applied to $G$ and $G$.

ConjAct.toConjActdefMathlib.GroupTheory.GroupAction.ConjAct, function or constant

Wording

no wording

English

$\operatorname{toConjAct}$ is a multiplicative equivalence of $G$ and $\mathrm{ConjAct}$ applied to $G$ defined as the inverse of $\operatorname{ofConjAct}$.

MulAut.conjNormaldefMathlib.GroupTheory.GroupAction.ConjAct, function or constant

Wording

the conjugate normal (from the name)

English

The conjugate normal is a monoid homomorphism of $G$ and the set of multiplicative automorphisms of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ defined as the composition of the multiplicative automorphism of $\mathrm{ConjAct}$ applied to $G$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {H}{x_{1}})}$ and the monoid homomorphism of $\operatorname{toConjAct}$.

unitsCentralizerEquivdefMathlib.GroupTheory.GroupAction.ConjAct, function or constant

Wording

the unit centralizer equivalence of M and x1 (from the name)

English

Let $M$ be a set. Let $x_{1}$ be an element of $\UnitsMACRoAO {M}$. Then the unit centralizer equivalence of $M$ and $x_{1}$ is a multiplicative equivalence of $\UnitsMACRoAO {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{centralizer} (\operatorname{singleton} (\operatorname{val} (x_{1})))}{x_{2}})})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (\mathrm{ConjAct} (\UnitsMACRoAO {M}), x_{1})}{x_{3}})}$.

Mathlib.GroupTheory.GroupAction.Defs

AddAction.fixedBydefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

no wording

English

Let $x$ be a set. Let $m$ be an element of $M$. Then $\operatorname{fixedBy}$ applied to $x$ and $m$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to the proposition that the sum of $m$ and $x_{3}$ is equal to $x_{3}$.

AddAction.fixedPointsdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the fixed point of M and x (from the name)

English

Let $M$ and $x$ be sets. Then the fixed point of $M$ and $x$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that for all elements $m$ of $M$, the sum of $m$ and $a$ is equal to $a$.

AddAction.orbitdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the orbit of x and a (from the docstring)

English

Let $x$ be a set. Let $a$ be an element of $x_{1}$. Then the orbit of $x$ and $a$ is an element of $\wp x_{1}$ defined as the range of the function that maps $m$ to the sum of $m$ and $a$.

AddAction.orbitRel.QuotientdefMathlib.GroupTheory.GroupAction.Defs, type

Wording

quotient of G and x (from the name)

English

Let $G$ and $x$ be sets. Then a quotient of $G$ and $x$ is an element of the function that maps $G$ and $x$ to $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $x$.

AddAction.orbitRel.Quotient.orbitdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the orbit of x3 (from the name)

English

Let $x_{3}$ be a quotient of $G$ and $x$. Then the orbit of $x_{3}$ is an element of $\wp x$.

AddAction.selfEquivSigmaOrbitsdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the self equivalence sigma orbit of G and x (from the name)

English

Let $G$ and $x$ be sets. Then the self equivalence sigma orbit of $G$ and $x$ is an equivalence from $x$ to $\Sigma$ applied to the function that maps $x_{3}$ to the set of elements of the orbit of $G$ and $\operatorname{out}$ applied to $x_{3}$.

AddAction.selfEquivSigmaOrbits'defMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the self equivalence sigma orbit of G and x (from the name)

English

AddAction.stabilizerdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the stabilizer of G and a (from the docstring)

English

Let $G$ be a set. Let $a$ be an element of $x$. Then the stabilizer of $G$ and $a$ is an additive subgroup of $G$.

AddAction.stabilizerAddSubmonoiddefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the stabilizer of M and a (from the docstring)

English

Let $M$ be a set. Let $a$ be an element of $x$. Then the stabilizer of $M$ and $a$ is an additive submonoid of $M$.

FixedPoints.subgroupdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the subgroup of M and x (from the name)

English

Let $M$ and $x$ be sets. Then the subgroup of $M$ and $x$ is a subgroup of $x$.

FixedPoints.submonoiddefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the submonoid of M and x (from the name)

English

Let $M$ and $x$ be sets. Then the submonoid of $M$ and $x$ is a submonoid of $x$.

MulAction.fixedBydefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

no wording

English

Let $x$ be a set. Let $m$ be an element of $M$. Then $\operatorname{fixedBy}$ applied to $x$ and $m$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to $\EqtMACRoH {(\HSMulhSMulMACRoAL {m}{x_{3}})}{x_{3}}$.

MulAction.fixedPointsdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the fixed point of M and x (from the name)

English

MulAction.orbitdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the orbit of x and a (from the docstring)

English

Let $x$ be a set. Let $a$ be an element of $x_{1}$. Then the orbit of $x$ and $a$ is an element of $\wp x_{1}$ defined as the range of the function that maps $m$ to $\HSMulhSMulMACRoAL {m}{a}$.

MulAction.orbitRel.QuotientdefMathlib.GroupTheory.GroupAction.Defs, type

Wording

quotient of G and x (from the name)

English

Let $G$ and $x$ be sets. Then a quotient of $G$ and $x$ is an element of the function that maps $G$ and $x$ to $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $x$.

MulAction.orbitRel.Quotient.orbitdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the orbit of x3 (from the name)

English

Let $x_{3}$ be a quotient of $G$ and $x$. Then the orbit of $x_{3}$ is an element of $\wp x$.

MulAction.selfEquivSigmaOrbitsdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the self equivalence sigma orbit of G and x (from the name)

English

MulAction.selfEquivSigmaOrbits'defMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the self equivalence sigma orbit of G and x (from the name)

English

MulAction.stabilizerdefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the stabilizer of G and a (from the docstring)

English

Let $G$ be a set. Let $a$ be an element of $x$. Then the stabilizer of $G$ and $a$ is a subgroup of $G$.

MulAction.stabilizerSubmonoiddefMathlib.GroupTheory.GroupAction.Defs, function or constant

Wording

the stabilizer of M and a (from the docstring)

English

Let $M$ be a set. Let $a$ be an element of $x$. Then the stabilizer of $M$ and $a$ is a submonoid of $M$.

Mathlib.GroupTheory.GroupAction.DomAct.Basic

DomAddActdefMathlib.GroupTheory.GroupAction.DomAct.Basic, type

Wording

no wording

English

Let $M$ be a set. Then an element of $\mathrm{DomAddAct}$ applied to $M$ is an element of the function that maps $M$ to the set of additive opposites of $M$.

DomAddAct.mkdefMathlib.GroupTheory.GroupAction.DomAct.Basic, function or constant

Wording

no wording

English

$\operatorname{mk}$ is an element of $\EquivMACRoAE {M}{\mathrm{DomAddAct} (M)}$ defined as the opposite equivalence.

DomMulActdefMathlib.GroupTheory.GroupAction.DomAct.Basic, type

Wording

no wording

English

Let $M$ be a set. Then an element of $\mathrm{DomMulAct}$ applied to $M$ is an element of the function that maps $M$ to the set of multiplicative opposites of $M$.

DomMulAct.mkdefMathlib.GroupTheory.GroupAction.DomAct.Basic, function or constant

Wording

no wording

English

$\operatorname{mk}$ is an element of $\EquivMACRoAE {M}{\mathrm{DomMulAct} (M)}$ defined as the opposite equivalence.

Mathlib.GroupTheory.GroupAction.FixingSubgroup

fixingAddSubgroupdefMathlib.GroupTheory.GroupAction.FixingSubgroup, function or constant

Wording

no wording

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then $\mathrm{fixingAddSubgroup}$ applied to $M$ and $s$ is an additive subgroup of $M$.

fixingAddSubmonoiddefMathlib.GroupTheory.GroupAction.FixingSubgroup, function or constant

Wording

no wording

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then $\mathrm{fixingAddSubmonoid}$ applied to $M$ and $s$ is an additive submonoid of $M$.

fixingSubgroupdefMathlib.GroupTheory.GroupAction.FixingSubgroup, function or constant

Wording

no wording

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then $\mathrm{fixingSubgroup}$ applied to $M$ and $s$ is a subgroup of $M$.

fixingSubmonoiddefMathlib.GroupTheory.GroupAction.FixingSubgroup, function or constant

Wording

no wording

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then $\mathrm{fixingSubmonoid}$ applied to $M$ and $s$ is a submonoid of $M$.

Mathlib.GroupTheory.GroupAction.Hom

AddActionHomstructureMathlib.GroupTheory.GroupAction.Hom, type

Wording

additive action homomorphism of X and Y (from the name)

English

Let $x$ be a function from elements of $M$ to elements of $N$. Let $X$ and $Y$ be sets. Then the additive action homomorphisms of $X$ and $Y$ are a basic type.

AddActionHom.End.addOppositeEquivdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the additive opposite equivalence (from the name)

English

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

AddActionHom.End.equivAddOppositedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the equivalence additive opposite (from the name)

English

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

AddActionHom.compdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be an additive action homomorphism of $Y$ and $Z$. Let $f$ be an additive action homomorphism of $X$ and $Y$. Then the composition of $g$ and $f$ is an additive action homomorphism of $X$ and $Z$.

AddActionHom.fstdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

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

English

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

AddActionHom.iddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the identity map of M (from the docstring)

English

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

AddActionHom.inversedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

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

AddActionHom.inverse'defMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be an additive action homomorphism of $X$ and $Y$. Let $g$ be a function from elements of $Y$ to elements of $X$. Assume that $\operatorname{RightInverse}$ holds for $x_{3}$ and $x$. Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Assume that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is an additive action homomorphism of $Y$ and $X$.

AddActionHom.ofEqdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the additive action homomorphism of h and f (from the name)

English

Assume that $\EqtMACRoH {x}{x_{3}}$. Let $f$ be an additive action homomorphism of $X$ and $Y$. Then the additive action homomorphism of $h$ and $f$ is an additive action homomorphism of $X$ and $Y$.

AddActionHom.proddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an additive action homomorphism of $x$ and $x_{1}$. Let $g$ be an additive action homomorphism of $x$ and $x_{2}$. Then the product of $f$ and $g$ is an additive action homomorphism of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

AddActionHom.prodMapdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

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

English

Let $f$ be an additive action homomorphism of $x$ and $x_{2}$. Let $g$ be an additive action homomorphism of $x_{1}$ and $x_{3}$. Then the product map of $f$ and $g$ is an additive action homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

AddActionHom.snddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

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

English

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

AddActionHom.toFundefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the additive action homomorphism of self and x3 (from the name)

English

Let $\mathrm{self}$ be an additive action homomorphism of $X$ and $Y$. Let $x_{3}$ be an element of $X$. Then the additive action homomorphism of $\mathrm{self}$ and $x_{3}$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

AddActionHomClassdefMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $M$, $X$ and $Y$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{AddActionHomClass}$ holds for $F$, $M$, $X$ and $Y$, if $\mathrm{AddActionSemiHomClass}$ holds for $F$, $\mathrm{id}$, $X$ and $Y$.

AddActionSemiHomClassclassMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $M$ to elements of $N$. Let $X$ and $Y$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{AddActionSemiHomClass}$ holds for $F$, $x$, $X$ and $Y$.

AddActionSemiHomClass.toAddActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the additive action homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the additive action homomorphism of $f$ is an additive action homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{AddActionSemiHomClass\_\_map\_vadd\_u209b\_\_u2097\_}$ applied to $f$.

DistribMulActionHomstructureMathlib.GroupTheory.GroupAction.Hom, type

Wording

distributive multiplicative action homomorphism of A and B (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $M$ and $N$. Let $A$ and $B$ be sets. Then the distributive multiplicative action homomorphisms of $A$ and $B$ are a basic type.

DistribMulActionHom.compdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a distributive multiplicative action homomorphism of $B$ and $C$. Let $f$ be a distributive multiplicative action homomorphism of $A$ and $B$. Then the composition of $g$ and $f$ is a distributive multiplicative action homomorphism of $A$ and $C$.

DistribMulActionHom.iddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the identity map of M (from the docstring)

English

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

DistribMulActionHom.inversedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

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

DistribMulActionHom.toAddMonoidHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the additive monoid homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a distributive multiplicative action homomorphism of $A$ and $B$. Then the additive monoid homomorphism of $\mathrm{self}$ is an additive monoid homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toMulActionHom}$ applied to $\mathrm{self}$ and $\mathrm{DistribMulActionHom\_\_map\_zero'}$ applied to $\mathrm{self}$ and $\mathrm{DistribMulActionHom\_\_map\_add'}$ applied to $\mathrm{self}$.

DistribMulActionHomClassdefMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $M$, $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{DistribMulActionHomClass}$ holds for $F$, $M$, $A$ and $B$, if $\mathrm{DistribMulActionSemiHomClass}$ holds for $F$, $\operatorname{coe}$ applied to the identity map of $M$, $A$ and $B$.

DistribMulActionSemiHomClassclassMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $M$ to elements of $N$. Let $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{DistribMulActionSemiHomClass}$ holds for $F$, $x$, $A$ and $B$.

DistribMulActionSemiHomClass.toDistribMulActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the distributive multiplicative action homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the distributive multiplicative action homomorphism of $f$ is a distributive multiplicative action homomorphism of $A$ and $B$.

MulActionHomstructureMathlib.GroupTheory.GroupAction.Hom, type

Wording

multiplicative action homomorphism of X and Y (from the name)

English

Let $x$ be a function from elements of $M$ to elements of $N$. Let $X$ and $Y$ be sets. Then the multiplicative action homomorphisms of $X$ and $Y$ are a basic type.

MulActionHom.End.equivMulOppositedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the equivalence multiplicative opposite (from the name)

English

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

MulActionHom.End.mulOppositeEquivdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative opposite equivalence (from the name)

English

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

MulActionHom.compdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a multiplicative action homomorphism of $Y$ and $Z$. Let $f$ be a multiplicative action homomorphism of $X$ and $Y$. Then the composition of $g$ and $f$ is a multiplicative action homomorphism of $X$ and $Z$.

MulActionHom.fstdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

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

English

Let $M$, $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is a multiplicative action homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

MulActionHom.iddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the identity map of M (from the docstring)

English

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

MulActionHom.inversedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

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

MulActionHom.inverse'defMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a multiplicative action homomorphism of $X$ and $Y$. Let $g$ be a function from elements of $Y$ to elements of $X$. Assume that $\operatorname{RightInverse}$ holds for $x_{3}$ and $x$. Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Assume that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is a multiplicative action homomorphism of $Y$ and $X$.

MulActionHom.ofEqdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative action homomorphism of h and f (from the name)

English

Assume that $\EqtMACRoH {x}{x_{3}}$. Let $f$ be a multiplicative action homomorphism of $X$ and $Y$. Then the multiplicative action homomorphism of $h$ and $f$ is a multiplicative action homomorphism of $X$ and $Y$.

MulActionHom.proddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a multiplicative action homomorphism of $x$ and $x_{1}$. Let $g$ be a multiplicative action homomorphism of $x$ and $x_{2}$. Then the product of $f$ and $g$ is a multiplicative action homomorphism of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

MulActionHom.prodMapdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

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

English

Let $f$ be a multiplicative action homomorphism of $x$ and $x_{2}$. Let $g$ be a multiplicative action homomorphism of $x_{1}$ and $x_{3}$. Then the product map of $f$ and $g$ is a multiplicative action homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

MulActionHom.snddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

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

English

Let $M$, $x$ and $x_{1}$ be sets. Then the second component of $x$ and $x_{1}$ is a multiplicative action homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

MulActionHom.toFundefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative action homomorphism of self and x3 (from the name)

English

Let $\mathrm{self}$ be a multiplicative action homomorphism of $X$ and $Y$. Let $x_{3}$ be an element of $X$. Then the multiplicative action homomorphism of $\mathrm{self}$ and $x_{3}$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

MulActionHomClassdefMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $M$, $X$ and $Y$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{MulActionHomClass}$ holds for $F$, $M$, $X$ and $Y$, if $\mathrm{MulActionSemiHomClass}$ holds for $F$, $\mathrm{id}$, $X$ and $Y$.

MulActionSemiHomClassclassMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $M$ to elements of $N$. Let $X$ and $Y$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulActionSemiHomClass}$ holds for $F$, $x$, $X$ and $Y$.

MulActionSemiHomClass.toMulActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative action homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the multiplicative action homomorphism of $f$ is a multiplicative action homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{MulActionSemiHomClass\_\_map\_smul\_u209b\_\_u2097\_}$ applied to $f$.

MulDistribMulActionHomstructureMathlib.GroupTheory.GroupAction.Hom, type

Wording

multiplicative distributive multiplicative action homomorphism of A and B (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $M$ and $N$. Let $A$ and $B$ be sets. Then the multiplicative distributive multiplicative action homomorphisms of $A$ and $B$ are a basic type.

MulDistribMulActionHom.compdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a multiplicative distributive multiplicative action homomorphism of $B$ and $C$. Let $f$ be a multiplicative distributive multiplicative action homomorphism of $A$ and $B$. Then the composition of $g$ and $f$ is a multiplicative distributive multiplicative action homomorphism of $A$ and $C$.

MulDistribMulActionHom.iddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the identity map of M (from the docstring)

English

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

MulDistribMulActionHom.inversedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

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

MulDistribMulActionHom.toMonoidHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the monoid homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a multiplicative distributive multiplicative action homomorphism of $A$ and $B$. Then the monoid homomorphism of $\mathrm{self}$ is a monoid homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toMulActionHom}$ applied to $\mathrm{self}$ and $\mathrm{MulDistribMulActionHom\_\_map\_one'}$ applied to $\mathrm{self}$ and $\mathrm{MulDistribMulActionHom\_\_map\_mul'}$ applied to $\mathrm{self}$.

MulDistribMulActionHomClassdefMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $M$, $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{MulDistribMulActionHomClass}$ holds for $F$, $M$, $A$ and $B$, if $\mathrm{MulDistribMulActionSemiHomClass}$ holds for $F$, $\operatorname{coe}$ applied to the identity map of $M$, $A$ and $B$.

MulDistribMulActionSemiHomClassclassMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $M$ to elements of $N$. Let $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulDistribMulActionSemiHomClass}$ holds for $F$, $x$, $A$ and $B$.

MulDistribMulActionSemiHomClass.toMulDistribMulActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative distributive multiplicative action homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the multiplicative distributive multiplicative action homomorphism of $f$ is a multiplicative distributive multiplicative action homomorphism of $A$ and $B$.

MulSemiringActionHomstructureMathlib.GroupTheory.GroupAction.Hom, type

Wording

multiplicative semiring action homomorphism of R and S (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $M$ and $N$. Let $R$ and $S$ be sets. Then the multiplicative semiring action homomorphisms of $R$ and $S$ are a basic type.

MulSemiringActionHom.compdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a multiplicative semiring action homomorphism of $S$ and $T$. Let $f$ be a multiplicative semiring action homomorphism of $R$ and $S$. Then the composition of $g$ and $f$ is a multiplicative semiring action homomorphism of $R$ and $T$.

MulSemiringActionHom.iddefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the identity map of M (from the docstring)

English

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

MulSemiringActionHom.inversedefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

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

MulSemiringActionHom.inverse'defMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a multiplicative semiring action homomorphism of $R$ and $S$. Let $g$ be a function from elements of $S$ to elements of $R$. Assume that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $x_{3}$ and $\operatorname{coe}$ applied to $x_{2}$. Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Assume that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is a multiplicative semiring action homomorphism of $S$ and $R$.

MulSemiringActionHom.toRingHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the ring homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a multiplicative semiring action homomorphism of $R$ and $S$. Then the ring homomorphism of $\mathrm{self}$ is a ring homomorphism of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toMulActionHom}$ applied to $\operatorname{toDistribMulActionHom}$ applied to $\mathrm{self}$ and $\mathrm{MulSemiringActionHom\_\_map\_one'}$ applied to $\mathrm{self}$ and $\mathrm{MulSemiringActionHom\_\_map\_mul'}$ applied to $\mathrm{self}$, $\mathrm{DistribMulActionHom\_\_map\_zero'}$ applied to $\operatorname{toDistribMulActionHom}$ applied to $\mathrm{self}$ and $\mathrm{DistribMulActionHom\_\_map\_add'}$ applied to $\operatorname{toDistribMulActionHom}$ applied to $\mathrm{self}$.

MulSemiringActionHomClassdefMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$ and $S$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{MulSemiringActionHomClass}$ holds for $F$, $R$ and $S$, if $\mathrm{MulSemiringActionSemiHomClass}$ holds for $F$, $\operatorname{coe}$ applied to the identity map of $M$, $R$ and $S$.

MulSemiringActionHomClass.toMulSemiringActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative semiring action homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the multiplicative semiring action homomorphism of $f$ is a multiplicative semiring action homomorphism of $R$ and $S$.

MulSemiringActionSemiHomClassclassMathlib.GroupTheory.GroupAction.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $M$ to elements of $N$. Let $R$ and $S$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulSemiringActionSemiHomClass}$ holds for $F$, $x_{2}$, $R$ and $S$.

Pi.evalAddActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the evaluation additive action homomorphism of i (from the name)

English

Let $i$ be an element of $x$. Then the evaluation additive action homomorphism of $i$ is an additive action homomorphism of the set of functions from elements $i_{1}$ of $x$ to elements of $X$ applied to $i_{1}$ and $X$ applied to $i$.

Pi.evalMulActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the evaluation multiplicative action homomorphism of i (from the name)

English

Let $i$ be an element of $x$. Then the evaluation multiplicative action homomorphism of $i$ is a multiplicative action homomorphism of the set of functions from elements $i_{1}$ of $x$ to elements of $X$ applied to $i_{1}$ and $X$ applied to $i$.

SMulCommClass.toDistribMulActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the distributive multiplicative action homomorphism of c (from the name)

English

Let $N$ and $A$ be sets. Let $c$ be an element of $M$. Then the distributive multiplicative action homomorphism of $c$ is a distributive multiplicative action homomorphism of $A$ and $A$.

SMulCommClass.toMulActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the multiplicative action homomorphism of c (from the name)

English

Let $N$ and $x$ be sets. Let $c$ be an element of $M$. Then the multiplicative action homomorphism of $c$ is a multiplicative action homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $\HSMulhSMulMACRoAL {c}{x_{3}}$ and $\mathrm{SMulCommClass\_\_smul\_comm}$ applied to $c$.

VAddCommClass.toAddActionHomdefMathlib.GroupTheory.GroupAction.Hom, function or constant

Wording

the additive action homomorphism of c (from the name)

English

Let $N$ and $x$ be sets. Let $c$ be an element of $M$. Then the additive action homomorphism of $c$ is an additive action homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to the sum of $c$ and $x_{3}$ and $\mathrm{VAddCommClass\_\_vadd\_comm}$ applied to $c$.

Mathlib.GroupTheory.GroupAction.IterateAct

IterateAddActstructureMathlib.GroupTheory.GroupAction.IterateAct, type

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x$. Then the elements of $\mathrm{IterateAddAct}$ applied to $f$ are a basic type.

IterateAddAct.valdefMathlib.GroupTheory.GroupAction.IterateAct, function or constant

Wording

the value of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\mathrm{IterateAddAct}$ applied to $f$. Then the value of $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

IterateMulActstructureMathlib.GroupTheory.GroupAction.IterateAct, type

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x$. Then the elements of $\mathrm{IterateMulAct}$ applied to $f$ are a basic type.

IterateMulAct.valdefMathlib.GroupTheory.GroupAction.IterateAct, function or constant

Wording

the value of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\mathrm{IterateMulAct}$ applied to $f$. Then the value of $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.GroupTheory.GroupAction.Iwasawa

MulAction.IwasawaStructurestructureMathlib.GroupTheory.GroupAction.Iwasawa, type

Wording

no wording

English

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

MulAction.IwasawaStructure.TdefMathlib.GroupTheory.GroupAction.Iwasawa, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{IwasawaStructure}$ applied to $M$ and $x_{1}$. Let $x_{3}$ be an element of $x_{1}$. Then $\operatorname{T}$ applied to $\mathrm{self}$ and $x_{3}$ is a subgroup of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

AddAction.IsMultiplyPreprimitiveclassMathlib.GroupTheory.GroupAction.MultiplePrimitivity, predicate

Wording

no wording

English

Let $M$ and $x$ be sets. Let $n$ be a natural number. Then we can say that $\operatorname{IsMultiplyPreprimitive}$ holds for $M$, $x$ and $n$.

MulAction.IsMultiplyPreprimitiveclassMathlib.GroupTheory.GroupAction.MultiplePrimitivity, predicate

Wording

no wording

English

Let $M$ and $x$ be sets. Let $n$ be a natural number. Then we can say that $\operatorname{IsMultiplyPreprimitive}$ holds for $M$, $x$ and $n$.

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

AddAction.IsMultiplyPretransitivedefMathlib.GroupTheory.GroupAction.MultipleTransitivity, predicate

Wording

no wording

English

Let $G$ and $x$ be sets. Let $n$ be a natural number. Then $\operatorname{IsMultiplyPretransitive}$ holds for $G$, $x$ and $n$, if $\operatorname{IsPretransitive}$ holds for $G$ and the set of embeddings of $\mathrm{Fin}$ applied to $n$ and $x$.

AddActionHom.embMapdefMathlib.GroupTheory.GroupAction.MultipleTransitivity, function or constant

Wording

the embedding map of e (from the name)

English

Let $G$ and $x$ be sets. Let $e$ be an embedding of $m$ and $n$. Then the embedding map of $e$ is an additive action homomorphism of the set of embeddings of $n$ and $x$ and the set of embeddings of $m$ and $x$.

AddActionHom.zeroEmbeddingMapdefMathlib.GroupTheory.GroupAction.MultipleTransitivity, function or constant

Wording

the zero embedding map (from the name)

English

The zero embedding map is an additive action homomorphism of the set of embeddings of $\mathrm{zero}$ and $x$ and $x$.

Function.Injective.addActionHom_embeddingdefMathlib.GroupTheory.GroupAction.MultipleTransitivity, function or constant

Wording

the additive action homomorphism embedding of x7 and hf (from the name)

English

Let $x_{7}$ be a set. Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the additive action homomorphism embedding of $x_{7}$ and $\mathrm{hf}$ is an additive action homomorphism of the set of embeddings of $x_{7}$ and $x$ and the set of embeddings of $x_{7}$ and $x_{3}$.

Function.Injective.mulActionHom_embeddingdefMathlib.GroupTheory.GroupAction.MultipleTransitivity, function or constant

Wording

the multiplicative action homomorphism embedding of x7 and hf (from the name)

English

Let $x_{7}$ be a set. Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the multiplicative action homomorphism embedding of $x_{7}$ and $\mathrm{hf}$ is a multiplicative action homomorphism of the set of embeddings of $x_{7}$ and $x$ and the set of embeddings of $x_{7}$ and $x_{3}$.

MulAction.IsMultiplyPretransitivedefMathlib.GroupTheory.GroupAction.MultipleTransitivity, predicate

Wording

no wording

English

MulActionHom.embMapdefMathlib.GroupTheory.GroupAction.MultipleTransitivity, function or constant

Wording

the embedding map of e (from the name)

English

Let $G$ and $x$ be sets. Let $e$ be an embedding of $m$ and $n$. Then the embedding map of $e$ is a multiplicative action homomorphism of the set of embeddings of $n$ and $x$ and the set of embeddings of $m$ and $x$.

MulActionHom.oneEmbeddingMapdefMathlib.GroupTheory.GroupAction.MultipleTransitivity, function or constant

Wording

the one embedding map (from the name)

English

The one embedding map is a multiplicative action homomorphism of the set of embeddings of $\mathrm{one}$ and $x$ and $x$.

Mathlib.GroupTheory.GroupAction.Primitive

AddAction.IsPreprimitiveclassMathlib.GroupTheory.GroupAction.Primitive, predicate

Wording

G is preprimitive (from the docstring)

English

Let $G$ and $X$ be sets. Then we can say that $G$ is preprimitive.

AddAction.IsQuasiPreprimitiveclassMathlib.GroupTheory.GroupAction.Primitive, predicate

Wording

no wording

English

Let $G$ and $X$ be sets. Then we can say that $\operatorname{IsQuasiPreprimitive}$ holds for $G$ and $X$.

MulAction.IsPreprimitiveclassMathlib.GroupTheory.GroupAction.Primitive, predicate

Wording

G is preprimitive (from the docstring)

English

Let $G$ and $X$ be sets. Then we can say that $G$ is preprimitive.

MulAction.IsQuasiPreprimitiveclassMathlib.GroupTheory.GroupAction.Primitive, predicate

Wording

no wording

English

Let $G$ and $X$ be sets. Then we can say that $\operatorname{IsQuasiPreprimitive}$ holds for $G$ and $X$.

Mathlib.GroupTheory.GroupAction.Quotient

AddAction.QuotientActionclassMathlib.GroupTheory.GroupAction.Quotient, predicate

Wording

H is a quotient action (from the name)

English

Let $X$ be a set. Let $H$ be an additive subgroup of $G$. Then we can say that $H$ is a quotient action.

AddAction.equivAddSubgroupOrbitsdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the equivalence additive subgroup orbit of X and H (from the name)

English

Let $X$ be a set. Let $H$ be an additive subgroup of $G$. Then the equivalence additive subgroup orbit of $X$ and $H$ is an equivalence from the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $X$ to $\Sigma$ applied to the function that maps $x_{3}$ to the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and the set of elements of the orbit of $x_{3}$ defined as the composition of the inverse of the sigma quotient equivalence of $\mathrm{AddAction\_\_orbitRel\_addSubgroup\_le}$ applied to $H$ and the right sigma congruence of the function that maps $x_{2}$ to the inverse of the equivalence additive subgroup orbit setoid preimage of $H$ and $x_{2}$.

AddAction.equivAddSubgroupOrbitsQuotientAddGroupdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the equivalence additive subgroup orbit quotient additive group of x2 and H (from the name)

English

Let $x_{2}$ be an element of $X$. Let $H$ be an additive subgroup of $G$. Then the equivalence additive subgroup orbit quotient additive group of $x_{2}$ and $H$ is an equivalence from the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $X$ to the set of quotients of $G$ and $H$.

AddAction.equivAddSubgroupOrbitsSetoidComapdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the equivalence additive subgroup orbit setoid preimage of H and x2 (from the name)

English

Let $H$ be an additive subgroup of $G$. Let $x_{2}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $X$. Then the equivalence additive subgroup orbit setoid preimage of $H$ and $x_{2}$ is an equivalence from the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the set of elements of the orbit of $x_{2}$ to $\mathrm{Quotient}$ applied to $\operatorname{comap}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is an element of the preimage of $\operatorname{mk}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $X$ and $\operatorname{singleton}$ applied to $x_{2}$ and $\operatorname{orbitRel}$ applied to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ and $X$.

AddAction.ofQuotientStabilizerdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the additive action of x2 and g (from the name)

English

Let $G$ be a set. Let $x_{2}$ be an element of $X$. Let $g$ be a quotient of $G$ and the stabilizer of $G$ and $x_{2}$. Then the additive action of $x_{2}$ and $g$ is an element of $X$.

AddAction.orbitEquivQuotientStabilizerdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the orbit equivalence quotient stabilizer of G and b (from the name)

English

Let $G$ be a set. Let $b$ be an element of $X$. Then the orbit equivalence quotient stabilizer of $G$ and $b$ is an equivalence from the set of elements of the orbit of $G$ and $b$ to the set of quotients of $G$ and the stabilizer of $G$ and $b$.

AddAction.orbitProdStabilizerEquivAddGroupdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the orbit product stabilizer equivalence additive group of G and b (from the name)

English

Let $G$ be a set. Let $b$ be an element of $X$. Then the orbit product stabilizer equivalence additive group of $G$ and $b$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\operatorname{Elem} (\operatorname{orbit} (G , b)), \SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{2}})})}{G}$ defined as the composition of the product congruence of the orbit equivalence quotient stabilizer of $G$ and $b$ and the identity of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{2}})}$ and the inverse of the additive group equivalence quotient product additive subgroup.

AddAction.selfEquivOrbitsQuotientProddefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence orbit quotient product of h (from the name)

English

Assume that for all elements $b$ of $X$, the stabilizer of $G$ and $b$ is equal to the bottom. Then the self equivalence orbit quotient product of $h$ is an element of $\EquivMACRoAE {X}{\mathrm{Prod} (\mathrm{Quotient} (\operatorname{orbitRel} (G , X)), G)}$.

AddAction.selfEquivOrbitsQuotientProd'defMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence orbit quotient product of h and h1 (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{mk''}$ and $x_{2}$. Assume that for all elements $b$ of $X$, the stabilizer of $G$ and $b$ is equal to the bottom. Then the self equivalence orbit quotient product of $h$ and $h_{1}$ is an element of $\EquivMACRoAE {X}{\mathrm{Prod} (\mathrm{Quotient} (\operatorname{orbitRel} (G , X)), G)}$.

AddAction.selfEquivSigmaOrbitsQuotientStabilizerdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence sigma orbit quotient stabilizer of G and X (from the name)

English

Let $G$ and $X$ be sets. Then the self equivalence sigma orbit quotient stabilizer of $G$ and $X$ is an equivalence from $X$ to $\Sigma$ applied to the function that maps $x_{2}$ to the set of quotients of $G$ and the stabilizer of $G$ and $\operatorname{out}$ applied to $x_{2}$.

AddAction.selfEquivSigmaOrbitsQuotientStabilizer'defMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence sigma orbit quotient stabilizer of X and h (from the name)

English

Let $G$ and $X$ be sets. Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{mk''}$ and $x_{2}$. Then the self equivalence sigma orbit quotient stabilizer of $X$ and $h$ is an equivalence from $X$ to $\Sigma$ applied to the function that maps $x_{3}$ to the set of quotients of $G$ and the stabilizer of $G$ and $x_{2}$ applied to $x_{3}$ defined as $\operatorname{trans}$ applied to the self equivalence sigma orbit of $G$ and $X$ and the right sigma congruence of the function that maps $x_{3}$ to the composition of the equivalence of $\mathrm{AddAction\_\_orbitRel\_\_Quotient\_\_orbit\_eq\_orbit\_out}$ applied to $x_{3}$ and $h$ and the orbit equivalence quotient stabilizer of $G$ and $x_{2}$ applied to $x_{3}$.

AddAction.sigmaFixedByEquivOrbitsProdAddGroupdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the sigma fixed by equivalence orbit product additive group of G and X (from the name)

English

Let $G$ and $X$ be sets. Then the sigma fixed by equivalence orbit product additive group of $G$ and $X$ is an equivalence from $\Sigma$ applied to the function that maps $g$ to the set of elements of $\operatorname{fixedBy}$ applied to $X$ and $g$ to $\mathrm{Prod}$ applied to $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $X$ and $G$.

MulAction.QuotientActionclassMathlib.GroupTheory.GroupAction.Quotient, predicate

Wording

H is a quotient action (from the name)

English

Let $X$ be a set. Let $H$ be a subgroup of $G$. Then we can say that $H$ is a quotient action.

MulAction.equivSubgroupOrbitsdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the equivalence subgroup orbit of X and H (from the name)

English

Let $X$ be a set. Let $H$ be a subgroup of $G$. Then the equivalence subgroup orbit of $X$ and $H$ is an equivalence from the set of quotients of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {H}{x_{2}})}$ and $X$ to $\Sigma$ applied to the function that maps $x_{3}$ to the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and the set of elements of the orbit of $x_{3}$ defined as the composition of the inverse of the sigma quotient equivalence of $\mathrm{MulAction\_\_orbitRel\_subgroup\_le}$ applied to $H$ and the right sigma congruence of the function that maps $x_{2}$ to the inverse of the equivalence subgroup orbit setoid preimage of $H$ and $x_{2}$.

MulAction.equivSubgroupOrbitsQuotientGroupdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the equivalence subgroup orbit quotient group of x2 and H (from the name)

English

Let $x_{2}$ be an element of $X$. Let $H$ be a subgroup of $G$. Then the equivalence subgroup orbit quotient group of $x_{2}$ and $H$ is an equivalence from the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $X$ to the set of quotients of $G$ and $H$.

MulAction.equivSubgroupOrbitsSetoidComapdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the equivalence subgroup orbit setoid preimage of H and x2 (from the name)

English

Let $H$ be a subgroup of $G$. Let $x_{2}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $X$. Then the equivalence subgroup orbit setoid preimage of $H$ and $x_{2}$ is an equivalence from the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the set of elements of the orbit of $x_{2}$ to $\mathrm{Quotient}$ applied to $\operatorname{comap}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is an element of the preimage of $\operatorname{mk}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $X$ and $\operatorname{singleton}$ applied to $x_{2}$ and $\operatorname{orbitRel}$ applied to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ and $X$.

MulAction.ofQuotientStabilizerdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the multiplicative action of x2 and g (from the name)

English

Let $G$ be a set. Let $x_{2}$ be an element of $X$. Let $g$ be a quotient of $G$ and the stabilizer of $G$ and $x_{2}$. Then the multiplicative action of $x_{2}$ and $g$ is an element of $X$.

MulAction.orbitEquivQuotientStabilizerdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the orbit equivalence quotient stabilizer of G and b (from the name)

English

MulAction.orbitProdStabilizerEquivGroupdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the orbit product stabilizer equivalence group of G and b (from the name)

English

Let $G$ be a set. Let $b$ be an element of $X$. Then the orbit product stabilizer equivalence group of $G$ and $b$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\operatorname{Elem} (\operatorname{orbit} (G , b)), \SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{2}})})}{G}$ defined as the composition of the product congruence of the orbit equivalence quotient stabilizer of $G$ and $b$ and the identity of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , b)}{x_{2}})}$ and the inverse of the group equivalence quotient product subgroup.

MulAction.selfEquivOrbitsQuotientProddefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence orbit quotient product of h (from the name)

English

MulAction.selfEquivOrbitsQuotientProd'defMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence orbit quotient product of h and h1 (from the name)

English

MulAction.selfEquivSigmaOrbitsQuotientStabilizerdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence sigma orbit quotient stabilizer of G and X (from the name)

English

MulAction.selfEquivSigmaOrbitsQuotientStabilizer'defMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the self equivalence sigma orbit quotient stabilizer of X and h (from the name)

English

Let $G$ and $X$ be sets. Assume that $\operatorname{LeftInverse}$ holds for $\operatorname{mk''}$ and $x_{2}$. Then the self equivalence sigma orbit quotient stabilizer of $X$ and $h$ is an equivalence from $X$ to $\Sigma$ applied to the function that maps $x_{3}$ to the set of quotients of $G$ and the stabilizer of $G$ and $x_{2}$ applied to $x_{3}$ defined as $\operatorname{trans}$ applied to the self equivalence sigma orbit of $G$ and $X$ and the right sigma congruence of the function that maps $x_{3}$ to the composition of the equivalence of $\mathrm{MulAction\_\_orbitRel\_\_Quotient\_\_orbit\_eq\_orbit\_out}$ applied to $x_{3}$ and $h$ and the orbit equivalence quotient stabilizer of $G$ and $x_{2}$ applied to $x_{3}$.

MulAction.sigmaFixedByEquivOrbitsProdGroupdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the sigma fixed by equivalence orbit product group of G and X (from the name)

English

Let $G$ and $X$ be sets. Then the sigma fixed by equivalence orbit product group of $G$ and $X$ is an equivalence from $\Sigma$ applied to the function that maps $g$ to the set of elements of $\operatorname{fixedBy}$ applied to $X$ and $g$ to $\mathrm{Prod}$ applied to $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $X$ and $G$.

MulActionHom.toQuotientdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the quotient of H (from the name)

English

Let $H$ be a subgroup of $G$. Then the quotient of $H$ is a multiplicative action homomorphism of $G$ and the set of quotients of $G$ and $H$.

Subgroup.quotientCenterEmbeddingdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the quotient center embedding of hS (from the name)

English

Assume that the closure of $S$ is equal to the top. Then the quotient center embedding of $\mathrm{hS}$ is an embedding of the set of quotients of $G$ and the center of $G$ and the set of functions from elements of $S$ to elements of the commutator set of $G$ defined as the composition of the embedding of the quotient equivalence of $\mathrm{Subgroup\_\_center\_eq\_infi'}$ applied to $\mathrm{hS}$ and the composition of the natural embedding of the function that maps $g$ to the centralizer of $\operatorname{singleton}$ applied to $g$ and the right product congruence of the function that maps $g_{1}$ to the quotient centralizer embedding of $g_{1}$.

Subgroup.quotientCentralizerEmbeddingdefMathlib.GroupTheory.GroupAction.Quotient, function or constant

Wording

the quotient centralizer embedding of g (from the name)

English

Let $g$ be an element of $G$. Then the quotient centralizer embedding of $g$ is an embedding of the set of quotients of $G$ and the centralizer of $\operatorname{singleton}$ applied to $g$ and the set of elements of the commutator set of $G$.

Mathlib.GroupTheory.GroupAction.SubMulAction

SMulMemClassclassMathlib.GroupTheory.GroupAction.SubMulAction, predicate

Wording

R is a multiplicative membership class (from the name)

English

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

SubAddActionstructureMathlib.GroupTheory.GroupAction.SubMulAction, type

Wording

difference additive action of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the difference additive actions of $R$ and $M$ are a basic type.

SubAddAction.SMulMemClass.subtypedefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the subtype of #1 (from the name)

English

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

SubAddAction.carrierdefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the carrier of self (from the name)

English

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

SubAddAction.copydefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the copy of p and s (from the name)

English

Let $p$ be a difference additive action of $R$ and $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{p}$. Then the copy of $p$ and $s$ is a difference additive action of $R$ and $M$.

SubAddAction.inclusiondefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the inclusion of s (from the docstring)

English

Let $s$ be a difference additive action of $M$ and $x$. Then the inclusion of $s$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ and $x$.

SubAddAction.subtypedefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the subtype of p (from the name)

English

Let $p$ be a difference additive action of $R$ and $M$. Then the subtype of $p$ is an additive action homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {p}{x_{1}})}$ and $M$.

SubMulActionstructureMathlib.GroupTheory.GroupAction.SubMulAction, type

Wording

difference multiplicative action of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the difference multiplicative actions of $R$ and $M$ are a basic type.

SubMulAction.SMulMemClass.subtypedefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the subtype of #1 (from the name)

English

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

SubMulAction.carrierdefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the carrier of self (from the name)

English

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

SubMulAction.copydefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the copy of p and s (from the name)

English

Let $p$ be a difference multiplicative action of $R$ and $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{p}$. Then the copy of $p$ and $s$ is a difference multiplicative action of $R$ and $M$.

SubMulAction.inclusiondefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the inclusion of s (from the docstring)

English

Let $s$ be a difference multiplicative action of $M$ and $x$. Then the inclusion of $s$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$ and $x$.

SubMulAction.subtypedefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the subtype of p (from the name)

English

Let $p$ be a difference multiplicative action of $R$ and $M$. Then the subtype of $p$ is a multiplicative action homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {p}{x_{1}})}$ and $M$.

Units.nonZeroSubMuldefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the non zero difference product of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the non zero difference product of $R$ and $M$ is a difference multiplicative action of $\UnitsMACRoAO {R}$ and $M$.

VAddMemClassclassMathlib.GroupTheory.GroupAction.SubMulAction, predicate

Wording

R is a additive membership class (from the name)

English

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

fixedPointsSubAddOfNormaldefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

no wording

English

$\mathrm{fixedPointsSubAddOfNormal}$ is a difference additive action of $G$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the fixed point of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $x_{1}$ and $\mathrm{vadd\_mem\_fixedPoints\_of\_normal}$.

fixedPointsSubMulOfNormaldefMathlib.GroupTheory.GroupAction.SubMulAction, function or constant

Wording

the fixed point difference multiplicative (from the name)

English

The fixed point difference multiplicative is a difference multiplicative action of $G$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the fixed point of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $x_{1}$ and $\mathrm{smul\_mem\_fixedPoints\_of\_normal}$.

Mathlib.GroupTheory.GroupAction.SubMulAction.Closure

SubAddAction.FGdefMathlib.GroupTheory.GroupAction.SubMulAction.Closure, predicate

Wording

no wording

English

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

SubAddAction.closuredefMathlib.GroupTheory.GroupAction.SubMulAction.Closure, function or constant

Wording

the closure of R and s (from the name)

English

Let $R$ be a set. Let $s$ be an element of $\wp M$. Then the closure of $R$ and $s$ is a difference additive action of $R$ and $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $p$ to $\mathrm{Leq} (s , p)$.

SubMulAction.FGdefMathlib.GroupTheory.GroupAction.SubMulAction.Closure, predicate

Wording

no wording

English

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

SubMulAction.closuredefMathlib.GroupTheory.GroupAction.SubMulAction.Closure, function or constant

Wording

the closure of R and s (from the name)

English

Let $R$ be a set. Let $s$ be an element of $\wp M$. Then the closure of $R$ and $s$ is a difference multiplicative action of $R$ and $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $p$ to $\mathrm{Leq} (s , p)$.

Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Set.powersetCard.addActionHom_of_embeddingdefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the additive action homomorphism of n (from the name)

English

Let $G$ and $x_{1}$ be sets. Let $n$ be a natural number. Then the additive action homomorphism of $n$ is an additive action homomorphism of the set of embeddings of $\mathrm{Fin}$ applied to $n$ and $x_{1}$ and the set of elements of the powerset cardinality of $x_{1}$ and $n$.

Set.powersetCard.addActionHom_singletondefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the additive action homomorphism singleton of G and x1 (from the name)

English

Let $G$ and $x_{1}$ be sets. Then the additive action homomorphism singleton of $G$ and $x_{1}$ is an additive action homomorphism of $x_{1}$ and the set of elements of the powerset cardinality of $x_{1}$ and $1$.

Set.powersetCard.mulActionHom_compldefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the multiplicative action homomorphism complement of x1 and hm (from the name)

English

Let $G$ and $x_{1}$ be sets such that $m + n$ is equal to the cardinality of $x_{1}$. Then the multiplicative action homomorphism complement of $x_{1}$ and $\mathrm{hm}$ is a multiplicative action homomorphism of the set of elements of the powerset cardinality of $x_{1}$ and $n$ and the set of elements of the powerset cardinality of $x_{1}$ and $m$.

Set.powersetCard.mulActionHom_of_embeddingdefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the multiplicative action homomorphism of n (from the name)

English

Let $G$ and $x_{1}$ be sets. Let $n$ be a natural number. Then the multiplicative action homomorphism of $n$ is a multiplicative action homomorphism of the set of embeddings of $\mathrm{Fin}$ applied to $n$ and $x_{1}$ and the set of elements of the powerset cardinality of $x_{1}$ and $n$.

Set.powersetCard.mulActionHom_singletondefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the multiplicative action homomorphism singleton of G and x1 (from the name)

English

Let $G$ and $x_{1}$ be sets. Then the multiplicative action homomorphism singleton of $G$ and $x_{1}$ is a multiplicative action homomorphism of $x_{1}$ and the set of elements of the powerset cardinality of $x_{1}$ and $1$.

Set.powersetCard.subAddActiondefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the difference additive action of n (from the name)

English

Let $G$ and $x_{1}$ be sets. Let $n$ be a natural number. Then the difference additive action of $n$ is a difference additive action of $G$ and the set of finite sets of $x_{1}$.

Set.powersetCard.subMulActiondefMathlib.GroupTheory.GroupAction.SubMulAction.Combination, function or constant

Wording

the difference multiplicative action of n (from the name)

English

Let $G$ and $x_{1}$ be sets. Let $n$ be a natural number. Then the difference multiplicative action of $n$ is a difference multiplicative action of $G$ and the set of finite sets of $x_{1}$.

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

SubAddAction.addConjMap_ofFixingAddSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the additive conjugate map of hg (from the name)

English

Assume that $\EqtMACRoH {\operatorname{hVAdd} (g , t)}{s}$. Then the additive conjugate map of $\mathrm{hg}$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , t)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{4}})}$.

SubAddAction.fixingAddSubgroupEquivFixingAddSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the equivalence of hg (from the docstring)

English

Assume that the sum of $g$ and $t$ is equal to $s$. Then the equivalence of $\mathrm{hg}$ is an additive equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , t)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , s)}{x_{4}})}$ defined as the composition of the additive subgroup map of $\operatorname{addConj}$ applied to $g$ and $\mathrm{fixingAddSubgroup}$ applied to $M$ and $t$ and the additive subgroup congruence of $\mathrm{SubAddAction\_\_fixingAddSubgroup\_map\_addConj\_eq}$ applied to $\mathrm{hg}$.

SubAddAction.fixingAddSubgroupInsertEquivdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be an element of $\wp (\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{7}})})$. Then $\operatorname{fixingAddSubgroupInsertEquiv}$ applied to $a$ and $s$ is an additive equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , \operatorname{insert} (a , \operatorname{image} (\lambda x_{4} . \MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{4}}, s)))}{x_{3}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (M , a)}{x_{6}})}, s)}{x_{5}})}$.

SubAddAction.fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

no wording

English

$\mathrm{SubAddAction\_\_fixingAddSubgroup\_union\_to\_fixingAddSubgroup\_of\_fixingAddSubgroup}$ is an additive monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , \UnionunionMACRoAB {s}{t})}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , s)}{x_{5}})}, \operatorname{preimage} (\lambda x_{6} . \MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{6}}, t))}{x_{4}})}$.

SubAddAction.map_ofFixingAddSubgroupUniondefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the map of s and t (from the name)

English

Let $M$ be a set. Let $s$ and $t$ be elements of $\wp x$. Then the map of $s$ and $t$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , \UnionunionMACRoAB {s}{t})}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , s)}{x_{5}})}, \operatorname{preimage} (\lambda x_{6} . \MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{6}}, t))}{x_{4}})}$.

SubAddAction.ofFixingAddSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference additive action of M and s (from the name)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then the difference additive action of $M$ and $s$ is a difference additive action of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingAddSubgroup} (M , s)}{x_{3}})}$ and $x$.

SubAddAction.ofFixingAddSubgroup.appenddefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

no wording

English

Let $x_{3}$ be an embedding of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{4}})}$. Then $\operatorname{append}$ applied to $x_{3}$ is an embedding of $\mathrm{Fin}$ applied to $\operatorname{ncard} (s)+ n$ and $x$.

SubAddAction.ofFixingAddSubgroup_equivariantMapdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference additive action of M and s (from the name)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then the difference additive action of $M$ and $s$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{3}})}$ and $x$.

SubAddAction.ofFixingAddSubgroup_insert_mapdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference additive action of a and s (from the name)

English

Let $a$ be an element of $x$. Let $s$ be an element of $\wp (\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{7}})})$. Then the difference additive action of $a$ and $s$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , \operatorname{insert} (a , \operatorname{image} (\lambda x_{4} . \MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{4}}, s)))}{x_{3}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (M , a)}{x_{6}})}, s)}{x_{5}})}$.

SubAddAction.ofFixingAddSubgroup_of_eqdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference additive action of M and hst (from the name)

English

Let $M$ be a set. Assume that $\EqtMACRoH {s}{t}$. Then the difference additive action of $M$ and $\mathrm{hst}$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , t)}{x_{4}})}$.

SubAddAction.ofFixingAddSubgroup_of_inclusiondefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference additive action of M and hst (from the name)

English

Let $M$ be a set. Assume that $t \leq s$. Then the difference additive action of $M$ and $\mathrm{hst}$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , s)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , t)}{x_{4}})}$.

SubAddAction.ofFixingAddSubgroup_of_singletondefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference additive action of M and a (from the name)

English

Let $M$ be a set. Let $a$ be an element of $x$. Then the difference additive action of $M$ and $a$ is an additive action homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{ofFixingAddSubgroup} (M , \operatorname{singleton} (a))}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{7}})}$.

SubMulAction.conjMap_ofFixingSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the conjugate map of hg (from the name)

English

Assume that $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{t}}{s}$. Then the conjugate map of $\mathrm{hg}$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , t)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{4}})}$.

SubMulAction.fixingSubgroupEquivFixingSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the equivalence of hg (from the docstring)

English

Assume that $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{t}}{s}$. Then the equivalence of $\mathrm{hg}$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , t)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , s)}{x_{4}})}$ defined as the composition of the subgroup map of $\operatorname{conj}$ applied to $g$ and $\mathrm{fixingSubgroup}$ applied to $M$ and $t$ and the subgroup congruence of $\mathrm{SubMulAction\_\_fixingSubgroup\_map\_conj\_eq}$ applied to $\mathrm{hg}$.

SubMulAction.fixingSubgroupInsertEquivdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be an element of $\wp (\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{7}})})$. Then $\operatorname{fixingSubgroupInsertEquiv}$ applied to $a$ and $s$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , \operatorname{insert} (a , \operatorname{image} (\lambda x_{4} . \MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{4}}, s)))}{x_{3}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (M , a)}{x_{6}})}, s)}{x_{5}})}$.

SubMulAction.fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

no wording

English

$\mathrm{SubMulAction\_\_fixingSubgroup\_union\_to\_fixingSubgroup\_of\_fixingSubgroup}$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , \UnionunionMACRoAB {s}{t})}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , s)}{x_{5}})}, \operatorname{preimage} (\lambda x_{6} . \MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{6}}, t))}{x_{4}})}$.

SubMulAction.map_ofFixingSubgroupUniondefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the map of s and t (from the name)

English

Let $M$ be a set. Let $s$ and $t$ be elements of $\wp x$. Then the map of $s$ and $t$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , \UnionunionMACRoAB {s}{t})}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , s)}{x_{5}})}, \operatorname{preimage} (\lambda x_{6} . \MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{6}}, t))}{x_{4}})}$.

SubMulAction.ofFixingSubgroupdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference multiplicative action of M and s (from the name)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then the difference multiplicative action of $M$ and $s$ is a difference multiplicative action of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{fixingSubgroup} (M , s)}{x_{3}})}$ and $x$.

SubMulAction.ofFixingSubgroup.appenddefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

no wording

English

Let $x_{3}$ be an embedding of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{4}})}$. Then $\operatorname{append}$ applied to $x_{3}$ is an embedding of $\mathrm{Fin}$ applied to $\operatorname{ncard} (s)+ n$ and $x$.

SubMulAction.ofFixingSubgroup_equivariantMapdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference multiplicative action of M and s (from the name)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then the difference multiplicative action of $M$ and $s$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{3}})}$ and $x$.

SubMulAction.ofFixingSubgroup_insert_mapdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference multiplicative action of a and s (from the name)

English

Let $a$ be an element of $x$. Let $s$ be an element of $\wp (\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{7}})})$. Then the difference multiplicative action of $a$ and $s$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , \operatorname{insert} (a , \operatorname{image} (\lambda x_{4} . \MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{4}}, s)))}{x_{3}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (M , a)}{x_{6}})}, s)}{x_{5}})}$.

SubMulAction.ofFixingSubgroup_of_eqdefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference multiplicative action of M and hst (from the name)

English

Let $M$ be a set. Assume that $\EqtMACRoH {s}{t}$. Then the difference multiplicative action of $M$ and $\mathrm{hst}$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , t)}{x_{4}})}$.

SubMulAction.ofFixingSubgroup_of_inclusiondefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference multiplicative action of M and hst (from the name)

English

Let $M$ be a set. Assume that $t \leq s$. Then the difference multiplicative action of $M$ and $\mathrm{hst}$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , s)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , t)}{x_{4}})}$.

SubMulAction.ofFixingSubgroup_of_singletondefMathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup, function or constant

Wording

the difference multiplicative action of M and a (from the name)

English

Let $M$ be a set. Let $a$ be an element of $x$. Then the difference multiplicative action of $M$ and $a$ is a multiplicative action homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{ofFixingSubgroup} (M , \operatorname{singleton} (a))}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (M , a)}{x_{7}})}$.

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

SubAddAction.ofStabilizerdefMathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer, function or constant

Wording

the difference additive action of G and a (from the name)

English

Let $G$ be a set. Let $a$ be an element of $x_{1}$. Then the difference additive action of $G$ and $a$ is a difference additive action of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , a)}{x_{3}})}$ and $x_{1}$.

SubAddAction.ofStabilizer.conjMapdefMathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer, function or constant

Wording

the conjugate map of hg (from the name)

English

Assume that $\EqtMACRoH {b}{\operatorname{hVAdd} (g , a)}$. Then the conjugate map of $\mathrm{hg}$ is an additive action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (G , a)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (G , b)}{x_{4}})}$.

SubAddAction.ofStabilizer.snocdefMathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer, function or constant

Wording

no wording

English

Let $x_{3}$ be an embedding of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (G , a)}{x_{4}})}$. Then $\operatorname{snoc}$ applied to $x_{3}$ is an embedding of $\mathrm{Fin}$ applied to the successor of $n$ and $x_{1}$.

SubMulAction.ofStabilizerdefMathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer, function or constant

Wording

the difference multiplicative action of G and a (from the name)

English

Let $G$ be a set. Let $a$ be an element of $x_{1}$. Then the difference multiplicative action of $G$ and $a$ is a difference multiplicative action of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , a)}{x_{3}})}$ and $x_{1}$.

SubMulAction.ofStabilizer.conjMapdefMathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer, function or constant

Wording

the conjugate map of hg (from the name)

English

Assume that $\EqtMACRoH {b}{\HSMulhSMulMACRoAL {g}{a}}$. Then the conjugate map of $\mathrm{hg}$ is a multiplicative action homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (G , a)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofStabilizer} (G , b)}{x_{4}})}$.

SubMulAction.ofStabilizer.snocdefMathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer, function or constant

Wording

no wording

English

Mathlib.GroupTheory.GroupAction.Support

AddAction.SupportsdefMathlib.GroupTheory.GroupAction.Support, predicate

Wording

no wording

English

Let $G$ be a set. Let $s$ be an element of $\wp x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{Supports}$ holds for $G$, $s$ and $b$, if for all elements $g$ of $G$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then the sum of $g$ and $a$ is equal to $a$, then the sum of $g$ and $b$ is equal to $b$.

MulAction.SupportsdefMathlib.GroupTheory.GroupAction.Support, predicate

Wording

no wording

English

Let $G$ be a set. Let $s$ be an element of $\wp x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{Supports}$ holds for $G$, $s$ and $b$, if for all elements $g$ of $G$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{a}}{a}$, then $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{b}}{b}$.

Mathlib.GroupTheory.GroupExtension.Basic

AddGroupExtension.AddConjClassesdefMathlib.GroupTheory.GroupExtension.Basic, type

Wording

additive conjugate class of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then an additive conjugate class of $S$ is an element of the function that maps $S$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $S$.

AddGroupExtension.Equiv.ofAddMonoidHomdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the equivalence of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $E$ and $\mathrm{E'}$ such that the composition of $f$ and the left injection of $S$ is equal to the left injection of $\mathrm{S'}$ and the composition of the projection homomorphism of $\mathrm{S'}$ and $f$ is equal to the projection homomorphism of $S$. Then the equivalence of $f$ is an equivalence of $S$ and $\mathrm{S'}$.

AddGroupExtension.Section.equivCompdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the composition of x4 and equiv (from the docstring)

English

Let $x_{4}$ be a section of $S$. Let $\mathrm{equiv}$ be an equivalence of $S$ and $\mathrm{S'}$. Then the composition of $x_{4}$ and $\mathrm{equiv}$ is a section of $\mathrm{S'}$.

AddGroupExtension.quotientKerRightHomEquivRightdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the right quotient kernel right homomorphism equivalence of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then the right quotient kernel right homomorphism equivalence of $S$ is an additive equivalence of the set of quotients of $E$ and the additive kernel of the projection homomorphism of $S$ and $G$ defined as the quotient kernel equivalence of the projection homomorphism of $S$ and $\mathrm{AddGroupExtension\_\_rightHom\_surjective}$ applied to $S$.

AddGroupExtension.quotientRangeInlEquivRightdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the right quotient range left injection equivalence of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then the right quotient range left injection equivalence of $S$ is an additive equivalence of the set of quotients of $E$ and the range of the left injection of $S$ and $G$ defined as the lift equivalence of the range of the left injection of $S$.

AddGroupExtension.surjInvRightHomdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the surjection inverse right homomorphism of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then the surjection inverse right homomorphism of $S$ is a section of $S$.

GroupExtension.ConjClassesdefMathlib.GroupTheory.GroupExtension.Basic, type

Wording

conjugate class of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then a conjugate class of $S$ is an element of the function that maps $S$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $S$.

GroupExtension.Equiv.ofMonoidHomdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the equivalence of f (from the name)

English

Let $f$ be a monoid homomorphism of $E$ and $\mathrm{E'}$ such that the composition of $f$ and the left injection of $S$ is equal to the left injection of $\mathrm{S'}$ and the composition of the projection homomorphism of $\mathrm{S'}$ and $f$ is equal to the projection homomorphism of $S$. Then the equivalence of $f$ is an equivalence of $S$ and $\mathrm{S'}$.

GroupExtension.Section.equivCompdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the composition of x4 and equiv (from the docstring)

English

Let $x_{4}$ be a section of $S$. Let $\mathrm{equiv}$ be an equivalence of $S$ and $\mathrm{S'}$. Then the composition of $x_{4}$ and $\mathrm{equiv}$ is a section of $\mathrm{S'}$.

GroupExtension.Splitting.conjActdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

no wording

English

Let $s$ be a splitting of $S$. Then $\operatorname{conjAct}$ applied to $s$ is a monoid homomorphism of $G$ and the set of multiplicative automorphisms of $N$ defined as the composition of $\operatorname{conjAct}$ applied to $S$ and the monoid homomorphism of $s$.

GroupExtension.Splitting.semidirectProductMulEquivdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the semidirect product multiplicative equivalence of s (from the name)

English

Let $s$ be a splitting of $S$. Then the semidirect product multiplicative equivalence of $s$ is a multiplicative equivalence of the set of semidirect products of $G$ and $\operatorname{conjAct}$ applied to $s$ and $E$ defined as $\operatorname{toMulEquiv}$ applied to the semidirect product to group extension equivalence of $s$.

GroupExtension.Splitting.semidirectProductToGroupExtensionEquivdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the semidirect product to group extension equivalence of s (from the name)

English

Let $s$ be a splitting of $S$. Then the semidirect product to group extension equivalence of $s$ is an equivalence of the group extension of $\operatorname{conjAct}$ applied to $s$ and $S$.

GroupExtension.quotientKerRightHomEquivRightdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the right quotient kernel right homomorphism equivalence of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then the right quotient kernel right homomorphism equivalence of $S$ is a multiplicative equivalence of the set of quotients of $E$ and the multiplicative kernel of the projection homomorphism of $S$ and $G$ defined as the quotient kernel equivalence of the projection homomorphism of $S$ and $\mathrm{GroupExtension\_\_rightHom\_surjective}$ applied to $S$.

GroupExtension.quotientRangeInlEquivRightdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the right quotient range left injection equivalence of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then the right quotient range left injection equivalence of $S$ is a multiplicative equivalence of the set of quotients of $E$ and the range of the left injection of $S$ and $G$ defined as the lift equivalence of the range of the left injection of $S$.

GroupExtension.surjInvRightHomdefMathlib.GroupTheory.GroupExtension.Basic, function or constant

Wording

the surjection inverse right homomorphism of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then the surjection inverse right homomorphism of $S$ is a section of $S$.

Mathlib.GroupTheory.GroupExtension.Defs

AddGroupExtensionstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

additive group extension of E and G (from the name)

English

Let $N$, $E$ and $G$ be sets. Then the additive group extensions of $E$ and $G$ are a basic type.

AddGroupExtension.EquivstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

equivalence of S and #2 (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Let $\mathrm{S'}$ be an additive group extension of $\mathrm{E'}$ and $G$. Then the equivalences of $S$ and $\mathrm{S'}$ are a basic type.

AddGroupExtension.Equiv.refldefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the identity of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then the identity of $S$ is an equivalence of $S$ and $S$.

AddGroupExtension.Equiv.symmdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the inverse of equiv (from the docstring)

English

Let $\mathrm{equiv}$ be an equivalence of $S$ and $\mathrm{S'}$. Then the inverse of $\mathrm{equiv}$ is an equivalence of $\mathrm{S'}$ and $S$.

AddGroupExtension.Equiv.transdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the composition of equiv and #2 (from the name)

English

Let $\mathrm{equiv}$ be an equivalence of $S$ and $\mathrm{S'}$. Let $\mathrm{equiv'}$ be an equivalence of $\mathrm{S'}$ and $\mathrm{S''}$. Then the composition of $\mathrm{equiv}$ and $\mathrm{equiv'}$ is an equivalence of $S$ and $\mathrm{S''}$.

AddGroupExtension.IsAddConjdefMathlib.GroupTheory.GroupExtension.Defs, predicate

Wording

s is a additive conjugate with respect to #3 (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Let $s$ and $\mathrm{s'}$ be splittings of $S$. Then $s$ is an additive conjugate with respect to $\mathrm{s'}$, if there exists an element $n$ of $N$, such that $\operatorname{coe}$ applied to $s$ is equal to the function that maps $g$ to $\operatorname{inl} (S , n)+ \mathrm{s'} (g)+ \operatorname{neg} (\operatorname{inl} (S , n))$.

AddGroupExtension.SectionstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

section of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then the sections of $S$ are a basic type.

AddGroupExtension.Section.toFundefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the section of self and x3 (from the name)

English

Let $\mathrm{self}$ be a section of $S$. Let $x_{3}$ be an element of $G$. Then the section of $\mathrm{self}$ and $x_{3}$ is an element of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

AddGroupExtension.SplittingstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

splitting of S (from the name)

English

Let $S$ be an additive group extension of $E$ and $G$. Then the splittings of $S$ are a basic type.

AddGroupExtension.Splitting.toSectiondefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the section of self (from the name)

English

Let $\mathrm{self}$ be a splitting of $S$. Then the section of $\mathrm{self}$ is a section of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toZeroHom}$ applied to $\operatorname{toAddMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{AddGroupExtension\_\_Splitting\_\_rightInverse\_rightHom}$ applied to $\mathrm{self}$.

AddGroupExtension.inldefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the left injection of self (from the name)

English

Let $\mathrm{self}$ be an additive group extension of $E$ and $G$. Then the left injection of $\mathrm{self}$ is an additive monoid homomorphism of $N$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AddGroupExtension.rightHomdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the projection homomorphism of self (from the docstring)

English

Let $\mathrm{self}$ be an additive group extension of $E$ and $G$. Then the projection homomorphism of $\mathrm{self}$ is an additive monoid homomorphism of $E$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

GroupExtensionstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

group extension of E and G (from the name)

English

Let $N$, $E$ and $G$ be sets. Then the group extensions of $E$ and $G$ are a basic type.

GroupExtension.EquivstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

equivalence of S and #2 (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Let $\mathrm{S'}$ be a group extension of $\mathrm{E'}$ and $G$. Then the equivalences of $S$ and $\mathrm{S'}$ are a basic type.

GroupExtension.Equiv.refldefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the identity of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then the identity of $S$ is an equivalence of $S$ and $S$.

GroupExtension.Equiv.symmdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the inverse of equiv (from the docstring)

English

Let $\mathrm{equiv}$ be an equivalence of $S$ and $\mathrm{S'}$. Then the inverse of $\mathrm{equiv}$ is an equivalence of $\mathrm{S'}$ and $S$.

GroupExtension.Equiv.transdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the composition of equiv and #2 (from the name)

English

GroupExtension.IsConjdefMathlib.GroupTheory.GroupExtension.Defs, predicate

Wording

s is conjugate to #3 (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Let $s$ and $\mathrm{s'}$ be splittings of $S$. Then $s$ is conjugate to $\mathrm{s'}$, if there exists an element $n$ of $N$, such that $\operatorname{coe}$ applied to $s$ is equal to the function that maps $g$ to $\operatorname{inl} (S , n)\times \mathrm{s'} (g)\times \operatorname{inv} (\operatorname{inl} (S , n))$.

GroupExtension.SectionstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

section of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then the sections of $S$ are a basic type.

GroupExtension.Section.toFundefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the section of self and x3 (from the name)

English

GroupExtension.SplittingstructureMathlib.GroupTheory.GroupExtension.Defs, type

Wording

splitting of S (from the name)

English

Let $S$ be a group extension of $E$ and $G$. Then the splittings of $S$ are a basic type.

GroupExtension.Splitting.toSectiondefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the section of self (from the name)

English

Let $\mathrm{self}$ be a splitting of $S$. Then the section of $\mathrm{self}$ is a section of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{GroupExtension\_\_Splitting\_\_rightInverse\_rightHom}$ applied to $\mathrm{self}$.

GroupExtension.conjActdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

no wording

English

Let $S$ be a group extension of $E$ and $G$. Then $\operatorname{conjAct}$ applied to $S$ is a monoid homomorphism of $E$ and the set of multiplicative automorphisms of $N$.

GroupExtension.inldefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the left injection of self (from the name)

English

Let $\mathrm{self}$ be a group extension of $E$ and $G$. Then the left injection of $\mathrm{self}$ is a monoid homomorphism of $N$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

GroupExtension.rightHomdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the projection homomorphism of self (from the docstring)

English

Let $\mathrm{self}$ be a group extension of $E$ and $G$. Then the projection homomorphism of $\mathrm{self}$ is a monoid homomorphism of $E$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

SemidirectProduct.inr_splittingdefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the right injection splitting of x2 (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and the set of multiplicative automorphisms of $N$. Then the right injection splitting of $x_{2}$ is a splitting of the group extension of $x_{2}$ defined as $\operatorname{mk}$ applied to the right injection and $\mathrm{SemidirectProduct\_\_rightHom\_inr}$.

SemidirectProduct.toGroupExtensiondefMathlib.GroupTheory.GroupExtension.Defs, function or constant

Wording

the group extension of x2 (from the name)

English

Let $x_{2}$ be a monoid homomorphism of $G$ and the set of multiplicative automorphisms of $N$. Then the group extension of $x_{2}$ is a group extension of the set of semidirect products of $G$ and $x_{2}$ and $G$ defined as $\operatorname{mk}$ applied to the left injection, the right homomorphism, $\mathrm{SemidirectProduct\_\_inl\_injective}$, $\mathrm{SemidirectProduct\_\_range\_inl\_eq\_ker\_rightHom}$ and $\mathrm{SemidirectProduct\_\_rightHom\_surjective}$.

Mathlib.GroupTheory.HNNExtension

HNNExtensiondefMathlib.GroupTheory.HNNExtension, type

Wording

no wording

English

Let $G$ be a set. Let $A$ and $B$ be subgroups of $G$. Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {B}{x_{3}})}$. Then an element of $\mathrm{HNNExtension}$ applied to $G$, $A$, $B$ and $x_{1}$ is an element of the function that maps $G$, $A$, $B$ and $x_{1}$ to the set of quotients of the congruence relation of $B$ and $x_{1}$.

HNNExtension.NormalWordstructureMathlib.GroupTheory.HNNExtension, type

Wording

normal word of d (from the name)

English

Let $d$ be a transversal pair of $A$ and $B$. Then the normal words of $d$ are a basic type.

HNNExtension.NormalWord.CancelsdefMathlib.GroupTheory.HNNExtension, predicate

Wording

no wording

English

Let $u$ be a unit of $\Integer$. Let $w$ be a normal word of $d$. Then $\operatorname{Cancels}$ holds for $u$ and $w$, if the head of $\operatorname{toReducedWord}$ applied to $w$ is an element of the subgroup of $B$ and $u$ and $\operatorname{map}$ applied to $\ProdfstMACRoZ$ and $\mathrm{List\_\_head?}$ applied to the list of $\operatorname{toReducedWord}$ applied to $w$ is equal to $\operatorname{some}$ applied to $\operatorname{neg}$ applied to $u$.

HNNExtension.NormalWord.ReducedWordstructureMathlib.GroupTheory.HNNExtension, type

Wording

reduced word of A and B (from the name)

English

Let $G$ be a set. Let $A$ and $B$ be subgroups of $G$. Then the reduced words of $A$ and $B$ are a basic type.

HNNExtension.NormalWord.ReducedWord.emptydefMathlib.GroupTheory.HNNExtension, function or constant

Wording

no wording

English

Let $G$ be a set. Let $A$ and $B$ be subgroups of $G$. Then $\operatorname{empty}$ applied to $G$, $A$ and $B$ is a reduced word of $A$ and $B$.

HNNExtension.NormalWord.ReducedWord.headdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the head of self (from the name)

English

Let $\mathrm{self}$ be a reduced word of $A$ and $B$. Then the head of $\mathrm{self}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

HNNExtension.NormalWord.ReducedWord.proddefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the product of x1 and x2 (from the docstring)

English

Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {B}{x_{4}})}$. Let $x_{2}$ be a reduced word of $A$ and $B$. Then the product of $x_{1}$ and $x_{2}$ is an element of $\mathrm{HNNExtension}$ applied to $G$, $A$, $B$ and $x_{1}$ defined as the product of $\operatorname{of}$ applied to the head of $x_{2}$ and $\operatorname{prod}$ applied to $\operatorname{map}$ applied to the function that maps $x_{3}$ to the product of the exponentiation of $\operatorname{t}$ to the underlying value in the base of $\ProdfstMACRoZ {x_{3}}$ and $\operatorname{of}$ applied to $\ProdsndMACRoAA {x_{3}}$ and the list of $x_{2}$.

HNNExtension.NormalWord.ReducedWord.toListdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the list of self (from the name)

English

Let $\mathrm{self}$ be a reduced word of $A$ and $B$. Then the list of $\mathrm{self}$ is a list of elements of $\mathrm{Prod}$ applied to $\UnitsMACRoAO {\Integer}$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

HNNExtension.NormalWord.TransversalPairstructureMathlib.GroupTheory.HNNExtension, type

Wording

transversal pair of A and B (from the name)

English

Let $G$ be a set. Let $A$ and $B$ be subgroups of $G$. Then the transversal pairs of $A$ and $B$ are a basic type.

HNNExtension.NormalWord.TransversalPair.setdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the set of self and x1 (from the name)

English

Let $\mathrm{self}$ be a transversal pair of $A$ and $B$. Let $x_{1}$ be a unit of $\Integer$. Then the set of $\mathrm{self}$ and $x_{1}$ is an element of $\wp G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

HNNExtension.NormalWord.consdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

no wording

English

Let $g$ be an element of $G$. Let $u$ be a unit of $\Integer$. Let $w$ be a normal word of $d$ such that the head of $\operatorname{toReducedWord}$ applied to $w$ is an element of the set of $d$ and $u$ and for all units $\mathrm{u'}$ of $\Integer$, if $\mathrm{u'}$ is an element of $\operatorname{map}$ applied to $\ProdfstMACRoZ$ and $\mathrm{List\_\_head?}$ applied to the list of $\operatorname{toReducedWord}$ applied to $w$, then if the head of $\operatorname{toReducedWord}$ applied to $w$ is an element of the subgroup of $B$ and $u$, then $\EqtMACRoH {u}{\mathrm{u'}}$. Then $\operatorname{cons}$ applied to $g$, $u$, $w$, $h_{1}$ and $h_{2}$ is a normal word of $d$.

HNNExtension.NormalWord.consRecOndefMathlib.GroupTheory.HNNExtension, function or constant

Wording

no wording

English

Let $w$ be a normal word of $d$. Let $\mathrm{ofGroup}$ be a function from elements $g_{1}$ of $G$ to elements of $\mathrm{motive}$ applied to the normal word of $g_{1}$. Let $\mathrm{cons}$ be a function from elements $g$ of $G$ and units $u$ of $\Integer$ and normal words $w_{1}$ of $d$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that the head of $\operatorname{toReducedWord}$ applied to $w_{1}$ is an element of the set of $d$ and $u$ and elements $h_{2}$ of $\mathrm{Proof}$ applied to the proposition that for all units $\mathrm{u'}$ of $\Integer$, if $\mathrm{u'}$ is an element of $\operatorname{map}$ applied to $\ProdfstMACRoZ$ and $\mathrm{List\_\_head?}$ applied to the list of $\operatorname{toReducedWord}$ applied to $w_{1}$, then if the head of $\operatorname{toReducedWord}$ applied to $w_{1}$ is an element of the subgroup of $B$ and $u$, then $\EqtMACRoH {u}{\mathrm{u'}}$ and elements of $\mathrm{motive}$ applied to $w_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $g$, $u$, $w_{1}$, $h_{1}$ and $h_{2}$. Then $\operatorname{consRecOn}$ applied to $w$, $g_{1}$, $\mathrm{ofGroup}$, $g$, $u$, $w_{1}$, $h_{1}$, $h_{2}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $w$.

HNNExtension.NormalWord.emptydefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the empty word (from the docstring)

English

The empty word is a normal word of $d$.

HNNExtension.NormalWord.equivdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the equivalence of x1 and d (from the name)

English

Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {B}{x_{3}})}$. Let $d$ be a transversal pair of $A$ and $B$. Then the equivalence of $x_{1}$ and $d$ is an equivalence from $\mathrm{HNNExtension}$ applied to $G$, $A$, $B$ and $x_{1}$ to the set of normal words of $d$.

HNNExtension.NormalWord.ofGroupdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the normal word of g (from the name)

English

Let $g$ be an element of $G$. Then the normal word of $g$ is a normal word of $d$.

HNNExtension.NormalWord.unitsSMuldefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the unit product of u and w (from the name)

English

HNNExtension.NormalWord.unitsSMulEquivdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the unit multiplicative equivalence of x1 (from the name)

English

HNNExtension.NormalWord.unitsSMulGroupdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the unit multiplicative group of u and g (from the name)

English

Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {B}{x_{4}})}$. Let $d$ be a transversal pair of $A$ and $B$. Let $u$ be an element of $\UnitsMACRoAO {\Integer}$. Let $g$ be an element of $G$. Then the unit multiplicative group of $u$ and $g$ is an element of $\mathrm{Prod}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (B , \operatorname{neg} (u))}{x_{2}})}$ and the set of elements of the set of $d$ and $u$ defined as $\ProdmkMACRoU {\operatorname{toSubgroupEquiv} (x_{1} , u , \ProdfstMACRoZ {\operatorname{equiv} (\operatorname{compl} (d , u), g)})}{\ProdsndMACRoAA {\operatorname{equiv} (\operatorname{compl} (d , u), g)}}$.

HNNExtension.NormalWord.unitsSMulWithCanceldefMathlib.GroupTheory.HNNExtension, function or constant

Wording

no wording

English

Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {B}{x_{3}})}$. Let $u$ be a unit of $\Integer$. Let $w$ be a normal word of $d$ such that $\operatorname{Cancels}$ holds for $u$ and $w$. Then $\operatorname{unitsSMulWithCancel}$ applied to $x_{1}$, $u$, $w$ and $h$ is a normal word of $d$ defined as $\operatorname{consRecOn}$ applied to $w$, $\mathrm{id}$ applied to the function that maps $x_{2}$ and $h$ to $w$, the function that maps $g$, $x_{3}$, $w_{1}$, $h_{1}$, $h_{2}$, $x_{4}$ and $\mathrm{can}$ to $\HSMulhSMulMACRoAL {\operatorname{toSubgroupEquiv} (x_{1} , u , g)}{w_{1}}$ and $h$.

HNNExtension.condefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the congruence relation of B and x1 (from the name)

English

Let $G$ be a set. Let $A$ and $B$ be subgroups of $G$. Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {A}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {B}{x_{3}})}$. Then the congruence relation of $B$ and $x_{1}$ is a congruence relation of the set of coproducts of $G$ and the set of multiplicatives of $\Integer$ defined as the congruence relation generator of the function that maps $x_{2}$ and $y$ to the proposition that there exists an element $a$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$, such that $\EqtMACRoH {x_{2}}{\operatorname{inr} (\operatorname{ofAdd} (1))\times \operatorname{inl} (a)}$ and $\EqtMACRoH {y}{\operatorname{inl} (x_{1} (a))\times \operatorname{inr} (\operatorname{ofAdd} (1))}$.

HNNExtension.liftdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the lift of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be an element of $H$ such that for all elements $a$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$, $\EqtMACRoH {x_{3} \times f (a)}{f (x_{1} (a))\times x_{3}}$. Then the lift of $f$ and $x_{3}$ is a monoid homomorphism of $\mathrm{HNNExtension}$ applied to $G$, $A$, $B$ and $x_{1}$ and $H$.

HNNExtension.ofdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

no wording

English

$\operatorname{of}$ is a monoid homomorphism of $G$ and $\mathrm{HNNExtension}$ applied to $G$, $A$, $B$ and $x_{1}$ defined as the composition of $\operatorname{mk'}$ applied to the congruence relation of $B$ and $x_{1}$ and the left injection.

HNNExtension.tdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

no wording

English

$\operatorname{t}$ is an element of $\mathrm{HNNExtension}$ applied to $G$, $A$, $B$ and $x_{1}$ defined as $\operatorname{comp}$ applied to $\operatorname{mk'}$ applied to the congruence relation of $B$ and $x_{1}$, the right injection and $\operatorname{ofAdd}$ applied to $1$.

HNNExtension.toSubgroupdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the subgroup of B and u (from the name)

English

Let $A$ and $B$ be subgroups of $G$. Let $u$ be a unit of $\Integer$. Then the subgroup of $B$ and $u$ is a subgroup of $G$ defined as $\iteMACRoG {(\EqtMACRoH {u}{1})}{A}{B}$.

HNNExtension.toSubgroupEquivdefMathlib.GroupTheory.HNNExtension, function or constant

Wording

the subgroup equivalence of x1 and u (from the name)

English

Let $x_{1}$ be a multiplicative equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {B}{x_{5}})}$. Let $u$ be an element of $\UnitsMACRoAO {\Integer}$. Then the subgroup equivalence of $x_{1}$ and $u$ is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (B , u)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (B , \operatorname{neg} (u))}{x_{3}})}$.

Mathlib.GroupTheory.Index

AddSubgroup.FiniteIndexclassMathlib.GroupTheory.Index, predicate

Wording

H is a finite index (from the name)

English

Let $H$ be an additive subgroup of $G$. Then we can say that $H$ is a finite index.

AddSubgroup.IsFiniteRelIndexclassMathlib.GroupTheory.Index, predicate

Wording

no wording

English

Let $H$ and $K$ be additive subgroups of $G$. Then we can say that $\operatorname{IsFiniteRelIndex}$ holds for $H$ and $K$.

AddSubgroup.indexdefMathlib.GroupTheory.Index, function or constant

Wording

the index of H (from the docstring)

English

Let $H$ be an additive subgroup of $G$. Then the index of $H$ is a natural number defined as the cardinality of the set of quotients of $G$ and $H$.

AddSubgroup.relIndexdefMathlib.GroupTheory.Index, function or constant

Wording

the relative index of H and K (from the name)

English

Let $H$ and $K$ be additive subgroups of $G$. Then the relative index of $H$ and $K$ is a natural number defined as the index of the additive subgroup of $H$ and $K$.

Subgroup.FiniteIndexclassMathlib.GroupTheory.Index, predicate

Wording

H is a finite index (from the name)

English

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

Subgroup.IsFiniteRelIndexclassMathlib.GroupTheory.Index, predicate

Wording

no wording

English

Let $H$ and $K$ be subgroups of $G$. Then we can say that $\operatorname{IsFiniteRelIndex}$ holds for $H$ and $K$.

Subgroup.indexdefMathlib.GroupTheory.Index, function or constant

Wording

the index of H (from the docstring)

English

Let $H$ be a subgroup of $G$. Then the index of $H$ is a natural number defined as the cardinality of the set of quotients of $G$ and $H$.

Subgroup.relIndexdefMathlib.GroupTheory.Index, function or constant

Wording

the relative index of H and K (from the name)

English

Let $H$ and $K$ be subgroups of $G$. Then the relative index of $H$ and $K$ is a natural number defined as the index of the subgroup of $H$ and $K$.

Mathlib.GroupTheory.IsPerfect

Group.IsPerfectclassMathlib.GroupTheory.IsPerfect, predicate

Wording

G is perfect (from the name)

English

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

Mathlib.GroupTheory.IsSubnormal

AddSubgroup.IsSubnormalinductiveMathlib.GroupTheory.IsSubnormal, predicate

Wording

x1 is a subnormal (from the name)

English

Let $x_{1}$ be an additive subgroup of $G$. Then we can say that $x_{1}$ is a subnormal.

AddSubgroup.IsSubnormal.belowinductiveMathlib.GroupTheory.IsSubnormal, predicate

Wording

no wording

English

Assume that $x_{1}$ is a subnormal. Then we can say that $\operatorname{below}$ holds for $t$.

Subgroup.IsSubnormalinductiveMathlib.GroupTheory.IsSubnormal, predicate

Wording

x1 is a subnormal (from the name)

English

Let $x_{1}$ be a subgroup of $G$. Then we can say that $x_{1}$ is a subnormal.

Subgroup.IsSubnormal.belowinductiveMathlib.GroupTheory.IsSubnormal, predicate

Wording

no wording

English

Assume that $x_{1}$ is a subnormal. Then we can say that $\operatorname{below}$ holds for $t$.

Mathlib.GroupTheory.MonoidLocalization.Away

AddLocalization.AwaydefMathlib.GroupTheory.MonoidLocalization.Away, type

Wording

no wording

English

Let $x_{1}$ be an element of $M$. Then an element of $\operatorname{Away}$ applied to $x_{1}$ is an element of the function that maps $x_{1}$ to the set of additive localizations of the multiple of $x_{1}$.

AddLocalization.Away.addEquivOfQuotientdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

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

English

Let $x_{2}$ be an element of $M$. Let $f$ be an element of $\operatorname{AwayMap}$ applied to $x_{2}$ and $N$. Then the additive equivalence of $x_{2}$ and $f$ is an additive equivalence of $\operatorname{Away}$ applied to $x_{2}$ and $N$ defined as the additive equivalence of $f$.

AddLocalization.Away.addMonoidOfdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the additive monoid of x1 (from the name)

English

Let $x_{1}$ be an element of $M$. Then the additive monoid of $x_{1}$ is an element of $\operatorname{AwayMap}$ applied to $x_{1}$ and $\operatorname{Away}$ applied to $x_{1}$ defined as the additive monoid of the multiple of $x_{1}$.

AddLocalization.Away.negSelfdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the negation self of x1 (from the name)

English

Let $x_{1}$ be an element of $M$. Then the negation self of $x_{1}$ is an element of $\operatorname{Away}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $0$ and $x_{1}$.

AddSubmonoid.LocalizationMap.AwayMapdefMathlib.GroupTheory.MonoidLocalization.Away, type

Wording

no wording

English

Let $x_{1}$ be an element of $M$. Let $\mathrm{N'}$ be a set. Then an element of $\operatorname{AwayMap}$ applied to $x_{1}$ and $\mathrm{N'}$ is an element of the function that maps $x_{1}$ and $\mathrm{N'}$ to the set of localization maps of the multiple of $x_{1}$ and $\mathrm{N'}$.

AddSubmonoid.LocalizationMap.AwayMap.liftdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the lift of x1 and F (from the name)

English

Let $x_{1}$ be an element of $A$. Let $F$ be an element of $\operatorname{AwayMap}$ applied to $x_{1}$ and $B$. Assume that $g$ applied to $x_{1}$ is an additive unit. Then the lift of $x_{1}$ and $F$ is an additive monoid homomorphism of $B$ and $C$.

AddSubmonoid.LocalizationMap.AwayMap.negSelfdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the negation self of x1 and F (from the name)

English

Let $x_{1}$ be an element of $A$. Let $F$ be an element of $\operatorname{AwayMap}$ applied to $x_{1}$ and $B$. Then the negation self of $x_{1}$ and $F$ is an element of $B$ defined as $\operatorname{mk'}$ applied to $F$, $0$ and $x_{1}$.

AddSubmonoid.LocalizationMap.awayToAwayRightdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $A$. Let $F$ be an element of $\operatorname{AwayMap}$ applied to $x_{1}$ and $B$. Let $G$ be an element of $\operatorname{AwayMap}$ applied to $x_{1} + y$ and $C$. Then $\operatorname{awayToAwayRight}$ applied to $x_{1}$, $F$, $y$ and $G$ is an additive monoid homomorphism of $B$ and $C$.

Localization.AwaydefMathlib.GroupTheory.MonoidLocalization.Away, type

Wording

no wording

English

Let $x_{1}$ be an element of $M$. Then an element of $\operatorname{Away}$ applied to $x_{1}$ is an element of the function that maps $x_{1}$ to the set of localizations of the power of $x_{1}$.

Localization.Away.invSelfdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the inverse self of x1 (from the name)

English

Let $x_{1}$ be an element of $M$. Then the inverse self of $x_{1}$ is an element of $\operatorname{Away}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $1$ and $x_{1}$.

Localization.Away.monoidOfdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the monoid of x1 (from the name)

English

Let $x_{1}$ be an element of $M$. Then the monoid of $x_{1}$ is an element of $\operatorname{AwayMap}$ applied to $x_{1}$ and $\operatorname{Away}$ applied to $x_{1}$ defined as the monoid of the power of $x_{1}$.

Localization.Away.mulEquivOfQuotientdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

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

English

Let $x_{2}$ be an element of $M$. Let $f$ be an element of $\operatorname{AwayMap}$ applied to $x_{2}$ and $N$. Then the multiplicative equivalence of $x_{2}$ and $f$ is a multiplicative equivalence of $\operatorname{Away}$ applied to $x_{2}$ and $N$ defined as the multiplicative equivalence of $f$.

Submonoid.LocalizationMap.AwayMapdefMathlib.GroupTheory.MonoidLocalization.Away, type

Wording

no wording

English

Submonoid.LocalizationMap.AwayMap.invSelfdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the inverse self of x2 and F (from the name)

English

Let $x_{2}$ be an element of $M$. Let $F$ be an element of $\operatorname{AwayMap}$ applied to $x_{2}$ and $N$. Then the inverse self of $x_{2}$ and $F$ is an element of $N$ defined as $\operatorname{mk'}$ applied to $F$, $1$ and $x_{2}$.

Submonoid.LocalizationMap.AwayMap.liftdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

the lift of x3 and F (from the name)

English

Let $x_{3}$ be an element of $M$. Let $F$ be an element of $\operatorname{AwayMap}$ applied to $x_{3}$ and $N$. Assume that $g$ applied to $x_{3}$ is a unit. Then the lift of $x_{3}$ and $F$ is a monoid homomorphism of $N$ and $P$.

Submonoid.LocalizationMap.awayToAwayRightdefMathlib.GroupTheory.MonoidLocalization.Away, function or constant

Wording

no wording

English

Let $x_{3}$ and $y$ be elements of $M$. Let $F$ be an element of $\operatorname{AwayMap}$ applied to $x_{3}$ and $N$. Let $G$ be an element of $\operatorname{AwayMap}$ applied to $x_{3} \times y$ and $P$. Then $\operatorname{awayToAwayRight}$ applied to $x_{3}$, $F$, $y$ and $G$ is a monoid homomorphism of $N$ and $P$.

Mathlib.GroupTheory.MonoidLocalization.Basic

AddLocalizationdefMathlib.GroupTheory.MonoidLocalization.Basic, type

Wording

additive localization of S (from the name)

English

Let $S$ be an additive submonoid of $M$. Then an additive localization of $S$ is an element of the function that maps $S$ to $\mathrm{AddOreLocalization}$ applied to $S$ and $M$.

AddLocalization.addMonoidOfdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the additive monoid of S (from the name)

English

Let $S$ be an additive submonoid of $M$. Then the additive monoid of $S$ is a localization map of $S$ and the set of additive localizations of $S$.

AddLocalization.liftOndefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be an additive localization of $S$. Let $f$ be a function from elements of $M$ and elements of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$ to elements of $p$ such that for all elements $a$ and $c$ of $M$, for all elements $b$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, for all elements $d$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, if $\operatorname{r}$ holds for $S$, $\ProdmkMACRoU {a}{b}$ and $\ProdmkMACRoU {c}{d}$, then $\EqtMACRoH {f (a , b)}{f (c , d)}$. Then $\operatorname{liftOn}$ applied to $x_{1}$, $f$ and $H$ is an element of $p$.

AddLocalization.liftOn₂defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be additive localizations of $S$. Let $f$ be a function from elements of $M$ and elements of $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {S}{x_{13}})}$ and elements of $M$ and elements of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {S}{x_{12}})}$ to elements of $p$ such that for all elements $a$ and $\mathrm{a'}$ of $M$, for all elements $b$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$, for all elements $\mathrm{b'}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, for all elements $c$ and $\mathrm{c'}$ of $M$, for all elements $d$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, for all elements $\mathrm{d'}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, if $\operatorname{r}$ holds for $S$, $\ProdmkMACRoU {a}{b}$ and $\ProdmkMACRoU {\mathrm{a'}}{\mathrm{b'}}$, then if $\operatorname{r}$ holds for $S$, $\ProdmkMACRoU {c}{d}$ and $\ProdmkMACRoU {\mathrm{c'}}{\mathrm{d'}}$, then $\EqtMACRoH {f (a , b , c , d)}{f (\mathrm{a'} , \mathrm{b'} , \mathrm{c'} , \mathrm{d'})}$. Then $\mathrm{AddLocalization\_\_liftOn\_u2082\_}$ applied to $x_{1}$, $y$, $f$ and $H$ is an element of $p$.

AddLocalization.mkdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $M$. Let $y$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then $\operatorname{mk}$ applied to $x_{1}$ and $y$ is an additive localization of $S$ defined as $\operatorname{oreSub}$ applied to $x_{1}$ and $y$.

AddLocalization.mkHomdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the homomorphism (from the name)

English

The homomorphism is an additive monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and the set of additive localizations of $S$.

AddLocalization.rdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $S$ be an additive submonoid of $M$. Then $\operatorname{r}$ applied to $S$ is an additive congruence relation of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that for all elements $y$ of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$, $c$ holds for $0$ and $\ProdmkMACRoU {y}{y}$.

AddLocalization.r'defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $S$ be an additive submonoid of $M$. Then $\operatorname{r'}$ applied to $S$ is an additive congruence relation of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$.

AddLocalization.recOnSubsingleton₂defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be additive localizations of $S$. Let $f$ be a function from elements $a$ of $M$ and elements $c$ of $M$ and elements $b$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and elements $d$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ to elements of $r$ applied to $\operatorname{mk}$ applied to $a$ and $b$ and $\operatorname{mk}$ applied to $c$ and $d$. Then $\mathrm{AddLocalization\_\_recOnSubsingleton\_u2082\_}$ applied to $x_{1}$, $y$, $a$, $c$, $b$, $d$ and $f$ is an element of $r$ applied to $x_{1}$ and $y$.

AddMonoidHom.toLocalizationMapdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the localization map of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that for all elements $y_{1}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, $f$ applied to $y_{1}$ is an additive unit, for all elements $z$ of $N$, there exists an element $x_{4}$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ such that $\EqtMACRoH {z + f (\ProdsndMACRoAA {x_{4}})}{f (\ProdfstMACRoZ {x_{4}})}$ and for all elements $x_{2}$ of $M$, for all elements $y$ of $M$, if $\EqtMACRoH {f (x_{2})}{f (y)}$, then there exists an element $c$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ such that $\EqtMACRoH {c + x_{2}}{c + y}$. Then the localization map of $f$ is a localization map of $S$ and $N$.

AddSubmonoid.IsLocalizationMapstructureMathlib.GroupTheory.MonoidLocalization.Basic, predicate

Wording

no wording

English

Let $S$ be an additive submonoid of $M$. Let $f$ be a function from elements of $M$ to elements of $N$. Then we can say that $\operatorname{IsLocalizationMap}$ holds for $S$ and $f$.

AddSubmonoid.LocalizationMapstructureMathlib.GroupTheory.MonoidLocalization.Basic, type

Wording

localization map of S and N (from the name)

English

Let $S$ be an additive submonoid of $M$. Let $N$ be a set. Then the localization maps of $S$ and $N$ are a basic type.

AddSubmonoid.LocalizationMap.mk'defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $f$ be a localization map of $S$ and $N$. Let $x_{2}$ be an element of $M$. Let $y$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{mk'}$ applied to $f$, $x_{2}$ and $y$ is an element of $N$ defined as the sum of $f$ applied to $x_{2}$ and the underlying value in the base of $\operatorname{neg}$ applied to $\operatorname{liftRight}$ applied to $\operatorname{domRestrict}$ applied to the additive monoid homomorphism of $f$ and $S$, $\mathrm{AddSubmonoid\_\_LocalizationMap\_\_map\_addUnits}$ applied to $f$ and $y$.

AddSubmonoid.LocalizationMap.secdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $f$ be a localization map of $S$ and $N$. Let $z$ be an element of $N$. Then $\operatorname{sec}$ applied to $f$ and $z$ is an element of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ defined as $\operatorname{choose}$ applied to $\operatorname{surj}$ applied to $f$ and $z$.

AddSubmonoid.LocalizationMap.toAddMonoidHomdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

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

LocalizationdefMathlib.GroupTheory.MonoidLocalization.Basic, type

Wording

localization of S (from the name)

English

Let $S$ be a submonoid of $M$. Then a localization of $S$ is an element of the function that maps $S$ to $\mathrm{OreLocalization}$ applied to $S$ and $M$.

Localization.liftOndefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a localization of $S$. Let $f$ be a function from elements of $M$ and elements of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$ to elements of $p$ such that for all elements $a$ and $c$ of $M$, for all elements $b$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, for all elements $d$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, if $\operatorname{r}$ holds for $S$, $\ProdmkMACRoU {a}{b}$ and $\ProdmkMACRoU {c}{d}$, then $\EqtMACRoH {f (a , b)}{f (c , d)}$. Then $\operatorname{liftOn}$ applied to $x_{1}$, $f$ and $H$ is an element of $p$.

Localization.liftOn₂defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be localizations of $S$. Let $f$ be a function from elements of $M$ and elements of $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {S}{x_{13}})}$ and elements of $M$ and elements of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {S}{x_{12}})}$ to elements of $p$ such that for all elements $a$ and $\mathrm{a'}$ of $M$, for all elements $b$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$, for all elements $\mathrm{b'}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, for all elements $c$ and $\mathrm{c'}$ of $M$, for all elements $d$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, for all elements $\mathrm{d'}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, if $\operatorname{r}$ holds for $S$, $\ProdmkMACRoU {a}{b}$ and $\ProdmkMACRoU {\mathrm{a'}}{\mathrm{b'}}$, then if $\operatorname{r}$ holds for $S$, $\ProdmkMACRoU {c}{d}$ and $\ProdmkMACRoU {\mathrm{c'}}{\mathrm{d'}}$, then $\EqtMACRoH {f (a , b , c , d)}{f (\mathrm{a'} , \mathrm{b'} , \mathrm{c'} , \mathrm{d'})}$. Then $\mathrm{Localization\_\_liftOn\_u2082\_}$ applied to $x_{1}$, $y$, $f$ and $H$ is an element of $p$.

Localization.mkdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $M$. Let $y$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then $\operatorname{mk}$ applied to $x_{1}$ and $y$ is a localization of $S$ defined as $\operatorname{oreDiv}$ applied to $x_{1}$ and $y$.

Localization.mkHomdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the homomorphism (from the name)

English

The homomorphism is a monoid homomorphism of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and the set of localizations of $S$.

Localization.monoidOfdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the monoid of S (from the name)

English

Let $S$ be a submonoid of $M$. Then the monoid of $S$ is a localization map of $S$ and the set of localizations of $S$.

Localization.rdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $M$. Then $\operatorname{r}$ applied to $S$ is a congruence relation of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that for all elements $y$ of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$, $c$ holds for $1$ and $\ProdmkMACRoU {y}{y}$.

Localization.r'defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $M$. Then $\operatorname{r'}$ applied to $S$ is a congruence relation of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$.

Localization.recOnSubsingleton₂defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be localizations of $S$. Let $f$ be a function from elements $a$ of $M$ and elements $c$ of $M$ and elements $b$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ and elements $d$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ to elements of $r$ applied to $\operatorname{mk}$ applied to $a$ and $b$ and $\operatorname{mk}$ applied to $c$ and $d$. Then $\mathrm{Localization\_\_recOnSubsingleton\_u2082\_}$ applied to $x_{1}$, $y$, $a$, $c$, $b$, $d$ and $f$ is an element of $r$ applied to $x_{1}$ and $y$.

MonoidHom.toLocalizationMapdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the localization map of f (from the name)

English

Let $f$ be a monoid homomorphism of $M$ and $N$ such that for all elements $y_{1}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, $f$ applied to $y_{1}$ is a unit, for all elements $z$ of $N$, there exists an element $x_{4}$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ such that $\EqtMACRoH {z \times f (\ProdsndMACRoAA {x_{4}})}{f (\ProdfstMACRoZ {x_{4}})}$ and for all elements $x_{2}$ of $M$, for all elements $y$ of $M$, if $\EqtMACRoH {f (x_{2})}{f (y)}$, then there exists an element $c$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$ such that $\EqtMACRoH {c \times x_{2}}{c \times y}$. Then the localization map of $f$ is a localization map of $S$ and $N$.

OreLocalization.equivMonoidLocalizationdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the equivalence monoid localization of R and S (from the name)

English

Let $R$ be a set. Let $S$ be a submonoid of $R$. Then the equivalence monoid localization of $R$ and $S$ is a multiplicative equivalence of the set of localizations of $S$ and $\mathrm{OreLocalization}$ applied to $S$ and $R$ defined as the identity map of the set of localizations of $S$.

OreLocalization.localizationMapdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the localization map of R and S (from the name)

English

Let $R$ be a set. Let $S$ be a submonoid of $R$. Then the localization map of $R$ and $S$ is a localization map of $S$ and $\mathrm{OreLocalization}$ applied to $S$ and $R$ defined as the monoid of $S$.

Submonoid.IsLocalizationMapstructureMathlib.GroupTheory.MonoidLocalization.Basic, predicate

Wording

no wording

English

Let $S$ be a submonoid of $M$. Let $f$ be a function from elements of $M$ to elements of $N$. Then we can say that $\operatorname{IsLocalizationMap}$ holds for $S$ and $f$.

Submonoid.LocalizationMapstructureMathlib.GroupTheory.MonoidLocalization.Basic, type

Wording

localization map of S and N (from the name)

English

Let $S$ be a submonoid of $M$. Let $N$ be a set. Then the localization maps of $S$ and $N$ are a basic type.

Submonoid.LocalizationMap.mk'defMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Let $f$ be a localization map of $S$ and $N$. Let $x_{2}$ be an element of $M$. Let $y$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{mk'}$ applied to $f$, $x_{2}$ and $y$ is an element of $N$ defined as the product of $f$ applied to $x_{2}$ and the underlying value in the base of $\operatorname{inv}$ applied to $\operatorname{liftRight}$ applied to $\operatorname{domRestrict}$ applied to the monoid homomorphism of $f$ and $S$, $\mathrm{Submonoid\_\_LocalizationMap\_\_map\_units}$ applied to $f$ and $y$.

Submonoid.LocalizationMap.secdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

no wording

English

Submonoid.LocalizationMap.toMonoidHomdefMathlib.GroupTheory.MonoidLocalization.Basic, function or constant

Wording

the monoid homomorphism of f (from the name)

English

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

Mathlib.GroupTheory.MonoidLocalization.DivPairs

AddSubmonoid.subPairsdefMathlib.GroupTheory.MonoidLocalization.DivPairs, function or constant

Wording

the difference pair of f and s (from the name)

English

Let $f$ be a localization map of the top and $G$. Let $s$ be an additive submonoid of $G$. Then the difference pair of $f$ and $s$ is an additive submonoid of $\mathrm{Prod}$ applied to $M$ and $M$ defined as the preimage of the composition of the difference additive monoid homomorphism and the product map of the additive monoid homomorphism of $f$ and the additive monoid homomorphism of $f$ and $s$.

Submonoid.divPairsdefMathlib.GroupTheory.MonoidLocalization.DivPairs, function or constant

Wording

the quotient pair of f and s (from the name)

English

Let $f$ be a localization map of the top and $G$. Let $s$ be a submonoid of $G$. Then the quotient pair of $f$ and $s$ is a submonoid of $\mathrm{Prod}$ applied to $M$ and $M$ defined as the preimage of the composition of the quotient monoid homomorphism and the product map of the monoid homomorphism of $f$ and the monoid homomorphism of $f$ and $s$.

Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Algebra.GrothendieckAddGroupdefMathlib.GroupTheory.MonoidLocalization.GrothendieckGroup, type

Wording

Grothendieck additive group of M (from the name)

English

Let $M$ be a set. Then a Grothendieck additive group of $M$ is an element of the function that maps $M$ to the set of additive localizations of the top.

Algebra.GrothendieckAddGroup.liftdefMathlib.GroupTheory.MonoidLocalization.GrothendieckGroup, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from the set of additive monoid homomorphisms of $M$ and $G$ to the set of additive monoid homomorphisms of the set of Grothendieck additive groups of $M$ and $G$.

Algebra.GrothendieckAddGroup.ofdefMathlib.GroupTheory.MonoidLocalization.GrothendieckGroup, function or constant

Wording

no wording

English

$\operatorname{of}$ is an additive monoid homomorphism of $M$ and the set of Grothendieck additive groups of $M$ defined as the additive monoid homomorphism of the additive monoid of the top.

Algebra.GrothendieckGroupdefMathlib.GroupTheory.MonoidLocalization.GrothendieckGroup, type

Wording

Grothendieck group of M (from the name)

English

Let $M$ be a set. Then a Grothendieck group of $M$ is an element of the function that maps $M$ to the set of localizations of the top.

Algebra.GrothendieckGroup.liftdefMathlib.GroupTheory.MonoidLocalization.GrothendieckGroup, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from the set of monoid homomorphisms of $M$ and $G$ to the set of monoid homomorphisms of the set of Grothendieck groups of $M$ and $G$.

Algebra.GrothendieckGroup.ofdefMathlib.GroupTheory.MonoidLocalization.GrothendieckGroup, function or constant

Wording

no wording

English

$\operatorname{of}$ is a monoid homomorphism of $M$ and the set of Grothendieck groups of $M$ defined as the monoid homomorphism of the monoid of the top.

Mathlib.GroupTheory.MonoidLocalization.Maps

AddLocalization.addEquivOfQuotientdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the additive equivalence of f (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Then the additive equivalence of $f$ is an additive equivalence of the set of additive localizations of $S$ and $N$ defined as the additive equivalence of the additive monoid of $S$ and $f$.

AddSubmonoid.LocalizationMap.addEquivOfAddEquivdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

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

English

Let $f$ be a localization map of $S$ and $N$. Let $k$ be a localization map of $T$ and $Q$. Assume that the map of the additive monoid homomorphism of $j$ and $S$ is equal to $T$. Then the additive equivalence of $f$ and $k$ is an additive equivalence of $N$ and $Q$ defined as the additive equivalence of $f$ and the localization map of $k$ and $H$.

AddSubmonoid.LocalizationMap.addEquivOfLocalizationsdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

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

English

Let $f$ be a localization map of $S$ and $N$. Let $k$ be a localization map of $S$ and $P$. Then the additive equivalence of $f$ and $k$ is an additive equivalence of $N$ and $P$.

AddSubmonoid.LocalizationMap.liftdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the lift of f and hg (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Assume that for all elements $y$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, $g$ applied to $y$ is an additive unit. Then the lift of $f$ and $\mathrm{hg}$ is an additive monoid homomorphism of $N$ and $P$.

AddSubmonoid.LocalizationMap.mapdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the map of f and k (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Assume that for all elements $y$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, $\MembershipmemMACRoT {T}{g (y)}$. Let $k$ be a localization map of $T$ and $Q$. Then the map of $f$ and $k$ is an additive monoid homomorphism of $N$ and $Q$.

AddSubmonoid.LocalizationMap.ofAddEquivOfDomdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

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

English

Let $f$ be a localization map of $S$ and $N$. Assume that the map of the additive monoid homomorphism of $k$ and $T$ is equal to $S$. Then the localization map of $f$ and $H$ is a localization map of $T$ and $N$.

AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizationsdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the localization map of f and k (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Let $k$ be an additive equivalence of $N$ and $P$. Then the localization map of $f$ and $k$ is a localization map of $S$ and $P$.

Localization.mulEquivOfQuotientdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the multiplicative equivalence of f (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Then the multiplicative equivalence of $f$ is a multiplicative equivalence of the set of localizations of $S$ and $N$ defined as the multiplicative equivalence of the monoid of $S$ and $f$.

Submonoid.LocalizationMap.liftdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the lift of f and hg (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Assume that for all elements $y$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, $g$ applied to $y$ is a unit. Then the lift of $f$ and $\mathrm{hg}$ is a monoid homomorphism of $N$ and $P$.

Submonoid.LocalizationMap.mapdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the map of f and k (from the name)

English

Submonoid.LocalizationMap.mulEquivOfLocalizationsdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

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

English

Let $f$ be a localization map of $S$ and $N$. Let $k$ be a localization map of $S$ and $P$. Then the multiplicative equivalence of $f$ and $k$ is a multiplicative equivalence of $N$ and $P$.

Submonoid.LocalizationMap.mulEquivOfMulEquivdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

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

English

Let $f$ be a localization map of $S$ and $N$. Let $k$ be a localization map of $T$ and $Q$. Assume that the map of the monoid homomorphism of $j$ and $S$ is equal to $T$. Then the multiplicative equivalence of $f$ and $k$ is a multiplicative equivalence of $N$ and $Q$ defined as the multiplicative equivalence of $f$ and the localization map of $k$ and $H$.

Submonoid.LocalizationMap.ofMulEquivOfDomdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

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

English

Let $f$ be a localization map of $S$ and $N$. Assume that the map of the monoid homomorphism of $k$ and $T$ is equal to $S$. Then the localization map of $f$ and $H$ is a localization map of $T$ and $N$.

Submonoid.LocalizationMap.ofMulEquivOfLocalizationsdefMathlib.GroupTheory.MonoidLocalization.Maps, function or constant

Wording

the localization map of f and k (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Let $k$ be a multiplicative equivalence of $N$ and $P$. Then the localization map of $f$ and $k$ is a localization map of $S$ and $P$.

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Submonoid.LocalizationMap.lift₀defMathlib.GroupTheory.MonoidLocalization.MonoidWithZero, function or constant

Wording

the lift of f and g (from the name)

English

Let $f$ be a localization map of $S$ and $N$. Let $g$ be a monoid with zero homomorphism of $M$ and $P$ such that for all elements $y$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, $g$ applied to $y$ is a unit. Then the lift of $f$ and $g$ is a monoid with zero homomorphism of $N$ and $P$.