Properties of group actions involving quotient groups #

This file proves properties of group actions which use the quotient group construction, notably

• the orbit-stabilizer theorem card_orbit_mul_card_stabilizer_eq_card_group
• the class formula card_eq_sum_card_group_div_card_stabilizer'
• Burnside's lemma sum_card_fixedBy_eq_card_orbits_mul_card_group
class MulAction.QuotientAction {α : Type u} (β : Type v) [] [] [] (H : ) :

A typeclass for when a MulAction β α descends to the quotient α ⧸ H.

• inv_mul_mem : ∀ (b : β) {a a' : α}, a⁻¹ * a' H(b a)⁻¹ * b a' H

The action fulfils a normality condition on products that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

Instances
theorem MulAction.QuotientAction.inv_mul_mem {α : Type u} {β : Type v} [] [] [] {H : } [self : ] (b : β) {a : α} {a' : α} :
a⁻¹ * a' H(b a)⁻¹ * b a' H

The action fulfils a normality condition on products that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

class AddAction.QuotientAction {α : Type u} (β : Type v) [] [] [] (H : ) :

A typeclass for when an AddAction β α descends to the quotient α ⧸ H.

• inv_mul_mem : ∀ (b : β) {a a' : α}, -a + a' H-(b +ᵥ a) + (b +ᵥ a') H

The action fulfils a normality condition on summands that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

Instances
theorem AddAction.QuotientAction.inv_mul_mem {α : Type u} {β : Type v} [] [] [] {H : } [self : ] (b : β) {a : α} {a' : α} :
-a + a' H-(b +ᵥ a) + (b +ᵥ a') H

The action fulfils a normality condition on summands that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

instance AddAction.left_quotientAction {α : Type u} [] (H : ) :
Equations
• =
instance MulAction.left_quotientAction {α : Type u} [] (H : ) :
Equations
• =
instance AddAction.right_quotientAction {α : Type u} [] (H : ) :
AddAction.QuotientAction { x : αᵃᵒᵖ // x H.normalizer.op } H
Equations
• =
instance MulAction.right_quotientAction {α : Type u} [] (H : ) :
MulAction.QuotientAction { x : αᵐᵒᵖ // x H.normalizer.op } H
Equations
• =
instance AddAction.right_quotientAction' {α : Type u} [] (H : ) [hH : H.Normal] :
Equations
• =
instance MulAction.right_quotientAction' {α : Type u} [] (H : ) [hH : H.Normal] :
Equations
• =
theorem AddAction.quotient.proof_2 {α : Type u_1} (β : Type u_2) [] [] [] (H : ) [] (q : α H) :
0 +ᵥ q = q
theorem AddAction.quotient.proof_3 {α : Type u_1} (β : Type u_2) [] [] [] (H : ) [] (b : β) (b' : β) (q : α H) :
b + b' +ᵥ q = b +ᵥ (b' +ᵥ q)
instance AddAction.quotient {α : Type u} (β : Type v) [] [] [] (H : ) [] :
Equations
theorem AddAction.quotient.proof_1 {α : Type u_1} (β : Type u_2) [] [] [] (H : ) [] (b : β) :
∀ (x x_1 : α), Setoid.r x x_1Setoid.r ((fun (x : α) => b +ᵥ x) x) ((fun (x : α) => b +ᵥ x) x_1)
instance MulAction.quotient {α : Type u} (β : Type v) [] [] [] (H : ) [] :
MulAction β (α H)
Equations
@[simp]
theorem AddAction.Quotient.vadd_mk {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b +ᵥ a = (b +ᵥ a)
@[simp]
theorem MulAction.Quotient.smul_mk {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b a = (b a)
@[simp]
theorem AddAction.Quotient.vadd_coe {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b +ᵥ a = (b +ᵥ a)
@[simp]
theorem MulAction.Quotient.smul_coe {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (a : α) :
b a = (b a)
@[simp]
theorem AddAction.Quotient.mk_vadd_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
(b +ᵥ ) = b +ᵥ q
@[simp]
theorem MulAction.Quotient.mk_smul_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
(b ) = b q
theorem AddAction.Quotient.coe_vadd_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
(b +ᵥ ) = b +ᵥ q
theorem MulAction.Quotient.coe_smul_out' {α : Type u} {β : Type v} [] [] [] (H : ) [] (b : β) (q : α H) :
(b ) = b q
theorem QuotientGroup.out'_conj_pow_minimalPeriod_mem {α : Type u} [] (H : ) (a : α) (q : α H) :
⁻¹ * a ^ Function.minimalPeriod (fun (x : α H) => a x) q * H
def MulActionHom.toQuotient {α : Type u} [] (H : ) :
α →ₑ[id] α H

The canonical map to the left cosets.

Equations
• = { toFun := QuotientGroup.mk, map_smul' := }
Instances For
@[simp]
theorem MulActionHom.toQuotient_apply {α : Type u} [] (H : ) (g : α) :
= g
instance AddAction.addLeftCosetsCompSubtypeVal {α : Type u} [] (H : ) (I : ) :
AddAction { x : α // x I } (α H)
Equations
instance MulAction.mulLeftCosetsCompSubtypeVal {α : Type u} [] (H : ) (I : ) :
MulAction { x : α // x I } (α H)
Equations
def AddAction.ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
β

The canonical map from the quotient of the stabilizer to the set.

Equations
Instances For
theorem AddAction.ofQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [] [] (x : β) (g1 : α) (g2 : α) (H : Setoid.r g1 g2) :
g1 +ᵥ x = g2 +ᵥ x
def MulAction.ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
β

The canonical map from the quotient of the stabilizer to the set.

Equations
Instances For
@[simp]
theorem AddAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [] [] (x : β) (g : α) :
= g +ᵥ x
@[simp]
theorem MulAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [] [] (x : β) (g : α) :
= g x
theorem AddAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
theorem MulAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [] [] (x : β) (g : ) :
theorem AddAction.ofQuotientStabilizer_vadd (α : Type u) {β : Type v} [] [] (x : β) (g : α) (g' : ) :
theorem MulAction.ofQuotientStabilizer_smul (α : Type u) {β : Type v} [] [] (x : β) (g : α) (g' : ) :
theorem AddAction.injective_ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) :
theorem MulAction.injective_ofQuotientStabilizer (α : Type u) {β : Type v} [] [] (x : β) :
noncomputable def AddAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [] [] (b : β) :

Orbit-stabilizer theorem.

Equations
Instances For
theorem AddAction.orbitEquivQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [] [] (b : β) :
(Function.Injective fun (g : ) => , ) Function.Surjective fun (g : ) => ,
noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [] [] (b : β) :
(MulAction.orbit α b)

Orbit-stabilizer theorem.

Equations
Instances For
noncomputable def AddAction.orbitProdStabilizerEquivAddGroup (α : Type u) {β : Type v} [] [] (b : β) :
(AddAction.orbit α b) × { x : α // } α

Orbit-stabilizer theorem.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MulAction.orbitProdStabilizerEquivGroup (α : Type u) {β : Type v} [] [] (b : β) :
(MulAction.orbit α b) × { x : α // } α

Orbit-stabilizer theorem.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup (α : Type u) {β : Type v} [] [] (b : β) [] [Fintype (AddAction.orbit α b)] [Fintype { x : α // }] :
Fintype.card (AddAction.orbit α b) * Fintype.card { x : α // } =

Orbit-stabilizer theorem.

theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group (α : Type u) {β : Type v} [] [] (b : β) [] [Fintype (MulAction.orbit α b)] [Fintype { x : α // }] :
Fintype.card (MulAction.orbit α b) * Fintype.card { x : α // } =

Orbit-stabilizer theorem.

@[simp]
theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [] [] (b : β) (a : α) :
(.symm a) = a +ᵥ b
@[simp]
theorem MulAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [] [] (b : β) (a : α) :
(.symm a) = a b
@[simp]
theorem AddAction.stabilizer_quotient {G : Type u_1} [] (H : ) :
= H
@[simp]
theorem MulAction.stabilizer_quotient {G : Type u_1} [] (H : ) :
= H
noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [] [] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
β (ω : ) × α AddAction.stabilizer α (φ ω)

Class formula : given G an additive group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be Quotient.out', so we provide AddAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [] [] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
β (ω : ) × α MulAction.stabilizer α (φ ω)

Class formula : given G a group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbitRel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be Quotient.out', so we provide MulAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' (α : Type u) (β : Type v) [] [] [] [] [Fintype (Quotient )] [(b : β) → Fintype { x : α // }] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
= ω : , / Fintype.card { x : α // x AddAction.stabilizer α (φ ω) }

Class formula for a finite group acting on a finite type. See AddAction.card_eq_sum_card_addGroup_div_card_stabilizer for a specialized version using Quotient.out'.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [] [] [] [] [Fintype (Quotient )] [(b : β) → Fintype { x : α // }] {φ : β} (hφ : Function.LeftInverse Quotient.mk'' φ) :
= ω : , / Fintype.card { x : α // x MulAction.stabilizer α (φ ω) }

Class formula for a finite group acting on a finite type. See MulAction.card_eq_sum_card_group_div_card_stabilizer for a specialized version using Quotient.out'.

noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [] [] :
β (ω : ) × α AddAction.stabilizer α ω.out'

Class formula. This is a special case of AddAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out'.

Equations
Instances For
theorem AddAction.selfEquivSigmaOrbitsQuotientStabilizer.proof_1 (α : Type u_2) (β : Type u_1) [] [] (q : ) :
Quotient.mk'' q.out' = q
noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [] [] :
β (ω : ) × α MulAction.stabilizer α ω.out'

Class formula. This is a special case of MulAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out'.

Equations
Instances For
theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer (α : Type u) (β : Type v) [] [] [] [] [Fintype (Quotient )] [(b : β) → Fintype { x : α // }] :
= ω : , / Fintype.card { x : α // x AddAction.stabilizer α ω.out' }

Class formula for a finite group acting on a finite type.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [] [] [] [] [Fintype (Quotient )] [(b : β) → Fintype { x : α // }] :
= ω : , / Fintype.card { x : α // x MulAction.stabilizer α ω.out' }

Class formula for a finite group acting on a finite type.

noncomputable def AddAction.sigmaFixedByEquivOrbitsProdAddGroup (α : Type u) (β : Type v) [] [] :
(a : α) × × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is an additive group acting on X and X/Gdenotes the quotient of X by the relation orbitRel G X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.sigmaFixedByEquivOrbitsProdAddGroup.proof_1 (α : Type u_1) (β : Type u_2) [] [] :
∀ (x : α × β), x.1 +ᵥ x.2 = x.2 x.1 +ᵥ x.2 = x.2
noncomputable def MulAction.sigmaFixedByEquivOrbitsProdGroup (α : Type u) (β : Type v) [] [] :
(a : α) × × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is a group acting on X and X/G denotes the quotient of X by the relation orbitRel G X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup (α : Type u) (β : Type v) [] [] [] [(a : α) → Fintype ] [Fintype (Quotient )] :
a : α, =

Burnside's lemma : given a finite additive group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group (α : Type u) (β : Type v) [] [] [] [(a : α) → Fintype ] [Fintype (Quotient )] :
a : α, =

Burnside's lemma : given a finite group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

Equations
• =
Equations
• =
instance AddAction.finite_quotient_of_pretransitive_of_finite_quotient {α : Type u} (β : Type v) [] [] {H : } [Finite (α H)] :
Finite (AddAction.orbitRel.Quotient { x : α // x H } β)
Equations
• =
instance MulAction.finite_quotient_of_pretransitive_of_finite_quotient {α : Type u} (β : Type v) [] [] {H : } [Finite (α H)] :
Finite (MulAction.orbitRel.Quotient { x : α // x H } β)
Equations
• =
theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_4 {α : Type u_2} {β : Type u_1} [] [] (H : ) (ω : ) (a : { x : β // x ⁻¹' {ω} }) (b : { x : β // x ⁻¹' {ω} }) (h : Setoid.r a b) :
(fun (x : { x : β // x ⁻¹' {ω} }) => x, ) a = (fun (x : { x : β // x ⁻¹' {ω} }) => x, ) b
theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_1 {α : Type u_2} {β : Type u_1} [] [] (ω : ) (x : ) :
x ⁻¹' {ω}
noncomputable def AddAction.equivAddSubgroupOrbitsSetoidComap {α : Type u} {β : Type v} [] [] (H : ) (ω : ) :
AddAction.orbitRel.Quotient { x : α // x H } Quotient (Setoid.comap Subtype.val (AddAction.orbitRel { x : α // x H } β))

A bijection between the quotient of the action of an additive subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_3 {α : Type u_2} {β : Type u_1} [] [] (ω : ) (x : { x : β // x ⁻¹' {ω} }) :
theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_5 {α : Type u_2} {β : Type u_1} [] [] (H : ) (ω : ) :
Function.LeftInverse (fun (q : Quotient (Setoid.comap Subtype.val (AddAction.orbitRel { x : α // x H } β))) => q.liftOn' (fun (x : { x : β // x ⁻¹' {ω} }) => x, ) ) fun (q : AddAction.orbitRel.Quotient { x : α // x H } ) => Quotient.liftOn' q (fun (x : ) => x, )
theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_6 {α : Type u_2} {β : Type u_1} [] [] (H : ) (ω : ) :
Function.RightInverse (fun (q : Quotient (Setoid.comap Subtype.val (AddAction.orbitRel { x : α // x H } β))) => q.liftOn' (fun (x : { x : β // x ⁻¹' {ω} }) => x, ) ) fun (q : AddAction.orbitRel.Quotient { x : α // x H } ) => Quotient.liftOn' q (fun (x : ) => x, )
theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_2 {α : Type u_2} {β : Type u_1} [] [] (H : ) (ω : ) (a : ) (b : ) (h : Setoid.r a b) :
(fun (x : ) => x, ) a = (fun (x : ) => x, ) b
noncomputable def MulAction.equivSubgroupOrbitsSetoidComap {α : Type u} {β : Type v} [] [] (H : ) (ω : ) :
MulAction.orbitRel.Quotient { x : α // x H } Quotient (Setoid.comap Subtype.val (MulAction.orbitRel { x : α // x H } β))

A bijection between the quotient of the action of a subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def AddAction.equivAddSubgroupOrbits {α : Type u} (β : Type v) [] [] (H : ) :
AddAction.orbitRel.Quotient { x : α // x H } β (ω : ) × AddAction.orbitRel.Quotient { x : α // x H }

A bijection between the orbits under the action of an additive subgroup H on β, and the orbits under the action of H on each orbit under the action of G.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MulAction.equivSubgroupOrbits {α : Type u} (β : Type v) [] [] (H : ) :
MulAction.orbitRel.Quotient { x : α // x H } β (ω : ) × MulAction.orbitRel.Quotient { x : α // x H }

A bijection between the orbits under the action of a subgroup H on β, and the orbits under the action of H on each orbit under the action of G.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance AddAction.finite_quotient_of_finite_quotient_of_finite_quotient {α : Type u} {β : Type v} [] [] {H : } [] [Finite (α H)] :
Finite (AddAction.orbitRel.Quotient { x : α // x H } β)
Equations
• =
instance MulAction.finite_quotient_of_finite_quotient_of_finite_quotient {α : Type u} {β : Type v} [] [] {H : } [] [Finite (α H)] :
Finite (MulAction.orbitRel.Quotient { x : α // x H } β)
Equations
• =
noncomputable def AddAction.equivAddSubgroupOrbitsQuotientAddGroup {α : Type u} {β : Type v} [] [] (x : β) (free : ∀ (y : β), ) (H : ) :
AddAction.orbitRel.Quotient { x : α // x H } β α H

Given an additive group acting freely and transitively, an equivalence between the orbits under the action of an additive subgroup and the quotient group.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_3 {α : Type u_1} {β : Type u_2} [] [] (x : β) (H : ) (g₁ : α) (g₂ : α) (h : Setoid.r g₁ g₂) :
(fun (g : α) => -g +ᵥ x) g₁ = (fun (g : α) => -g +ᵥ x) g₂
theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_4 {α : Type u_1} {β : Type u_2} [] [] (x : β) (free : ∀ (y : β), ) (H : ) (y : AddAction.orbitRel.Quotient { x : α // x H } β) :
(fun (q : α H) => Quotient.liftOn' q (fun (g : α) => -g +ᵥ x) ) ((fun (q : AddAction.orbitRel.Quotient { x : α // x H } β) => Quotient.liftOn' q (fun (y : β) => .choose) ) y) = y
theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_5 {α : Type u_1} {β : Type u_2} [] [] (x : β) (free : ∀ (y : β), ) (H : ) (g : α H) :
(fun (q : AddAction.orbitRel.Quotient { x : α // x H } β) => Quotient.liftOn' q (fun (y : β) => .choose) ) ((fun (q : α H) => Quotient.liftOn' q (fun (g : α) => -g +ᵥ x) ) g) = g
theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_2 {α : Type u_2} {β : Type u_1} [] [] (x : β) (free : ∀ (y : β), ) (H : ) (y₁ : β) (y₂ : β) (h : Setoid.r y₁ y₂) :
(fun (y : β) => .choose) y₁ = (fun (y : β) => .choose) y₂
theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_1 {α : Type u_1} {β : Type u_2} [] [] (x : β) (y : β) :
∃ (m : α), m +ᵥ y = x
noncomputable def MulAction.equivSubgroupOrbitsQuotientGroup {α : Type u} {β : Type v} [] [] (x : β) (free : ∀ (y : β), ) (H : ) :
MulAction.orbitRel.Quotient { x : α // x H } β α H

Given a group acting freely and transitively, an equivalence between the orbits under the action of a subgroup and the quotient group.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ConjClasses.card_carrier {G : Type u_1} [] [] (g : G) [Fintype .carrier] [Fintype { x : // x }] :
Fintype.card .carrier = / Fintype.card { x : // x }
theorem Subgroup.normalCore_eq_ker {G : Type u_1} [] (H : ) :
H.normalCore = (MulAction.toPermHom G (G H)).ker
noncomputable def Subgroup.quotientCentralizerEmbedding {G : Type u_1} [] (g : G) :

Cosets of the centralizer of an element embed into the set of commutators.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Subgroup.quotientCentralizerEmbedding_apply {G : Type u_1} [] (g : G) (x : G) :
= x, g,
noncomputable def Subgroup.quotientCenterEmbedding {G : Type u_1} [] {S : Set G} (hS : ) :
S

If G is generated by S, then the quotient by the center embeds into S-indexed sequences of commutators.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Subgroup.quotientCenterEmbedding_apply {G : Type u_1} [] {S : Set G} (hS : ) (g : G) (s : S) :
(↑g) s = g, s,