Documentation

Mathlib.GroupTheory.Complement

Complements #

In this file we define the complement of a subgroup.

Main definitions #

Main results #

def Subgroup.IsComplement {G : Type u_1} [Group G] (S T : Set G) :

S and T are complements if (*) : S × T → G is a bijection. This notion generalizes left transversals, right transversals, and complementary subgroups.

Equations
def AddSubgroup.IsComplement {G : Type u_1} [AddGroup G] (S T : Set G) :

S and T are complements if (+) : S × T → G is a bijection

Equations
@[reducible, inline]
abbrev Subgroup.IsComplement' {G : Type u_1} [Group G] (H K : Subgroup G) :

H and K are complements if (*) : H × K → G is a bijection

Equations
@[reducible, inline]
abbrev AddSubgroup.IsComplement' {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :

H and K are complements if (+) : H × K → G is a bijection

Equations
@[deprecated Subgroup.IsComplement (since := "2024-12-18")]
def Subgroup.leftTransversals {G : Type u_1} [Group G] (T : Set G) :
Set (Set G)

The set of left-complements of T : Set G

Equations
@[deprecated Subgroup.IsComplement (since := "2024-12-18")]
def AddSubgroup.leftTransversals {G : Type u_1} [AddGroup G] (T : Set G) :
Set (Set G)

The set of left-complements of T : Set G

Equations
@[deprecated Subgroup.IsComplement (since := "2024-12-18")]
def Subgroup.rightTransversals {G : Type u_1} [Group G] (S : Set G) :
Set (Set G)

The set of right-complements of S : Set G

Equations
@[deprecated Subgroup.IsComplement (since := "2024-12-18")]
def AddSubgroup.rightTransversals {G : Type u_1} [AddGroup G] (S : Set G) :
Set (Set G)

The set of right-complements of S : Set G

Equations
theorem Subgroup.isComplement'_def {G : Type u_1} [Group G] {H K : Subgroup G} :
theorem Subgroup.isComplement_iff_existsUnique {G : Type u_1} [Group G] {S T : Set G} :
IsComplement S T ∀ (g : G), ∃! x : S × T, x.1 * x.2 = g
theorem AddSubgroup.isComplement_iff_existsUnique {G : Type u_1} [AddGroup G] {S T : Set G} :
IsComplement S T ∀ (g : G), ∃! x : S × T, x.1 + x.2 = g
theorem Subgroup.IsComplement.existsUnique {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) (g : G) :
∃! x : S × T, x.1 * x.2 = g
theorem AddSubgroup.IsComplement.existsUnique {G : Type u_1} [AddGroup G] {S T : Set G} (h : IsComplement S T) (g : G) :
∃! x : S × T, x.1 + x.2 = g
theorem Subgroup.IsComplement'.symm {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) :
theorem Subgroup.isComplement_univ_left {G : Type u_1} [Group G] {S : Set G} :
IsComplement Set.univ S ∃ (g : G), S = {g}
theorem AddSubgroup.isComplement_univ_left {G : Type u_1} [AddGroup G] {S : Set G} :
IsComplement Set.univ S ∃ (g : G), S = {g}
theorem Subgroup.isComplement_univ_right {G : Type u_1} [Group G] {S : Set G} :
IsComplement S Set.univ ∃ (g : G), S = {g}
theorem AddSubgroup.isComplement_univ_right {G : Type u_1} [AddGroup G] {S : Set G} :
IsComplement S Set.univ ∃ (g : G), S = {g}
theorem Subgroup.IsComplement.mul_eq {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) :
theorem AddSubgroup.IsComplement.add_eq {G : Type u_1} [AddGroup G] {S T : Set G} (h : IsComplement S T) :
theorem Subgroup.IsComplement.nonempty_left {G : Type u_1} [Group G] {S T : Set G} (hst : IsComplement S T) :
theorem Subgroup.IsComplement.nonempty_right {G : Type u_1} [Group G] {S T : Set G} (hst : IsComplement S T) :
theorem Subgroup.IsComplement.pairwiseDisjoint_smul {G : Type u_1} [Group G] {S T : Set G} (hst : IsComplement S T) :
S.PairwiseDisjoint fun (x : G) => x T
theorem AddSubgroup.IsComplement.pairwiseDisjoint_vadd {G : Type u_1} [AddGroup G] {S T : Set G} (hst : IsComplement S T) :
S.PairwiseDisjoint fun (x : G) => x +ᵥ T
theorem Subgroup.IsComplement.card_mul_card {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) :
theorem Subgroup.isComplement_iff_existsUnique_inv_mul_mem {G : Type u_1} [Group G] {S T : Set G} :
IsComplement S T ∀ (g : G), ∃! s : S, (↑s)⁻¹ * g T
theorem AddSubgroup.isComplement_iff_existsUnique_neg_add_mem {G : Type u_1} [AddGroup G] {S T : Set G} :
IsComplement S T ∀ (g : G), ∃! s : S, -s + g T
@[deprecated Subgroup.isComplement_iff_existsUnique_inv_mul_mem (since := "2024-12-18")]
theorem Subgroup.mem_leftTransversals_iff_existsUnique_inv_mul_mem {G : Type u_1} [Group G] {S T : Set G} :
S leftTransversals T ∀ (g : G), ∃! s : S, (↑s)⁻¹ * g T
@[deprecated Subgroup.isComplement_iff_existsUnique_inv_mul_mem (since := "2024-12-18")]
theorem AddSubgroup.mem_leftTransversals_iff_existsUnique_neg_add_mem {G : Type u_1} [AddGroup G] {S T : Set G} :
S leftTransversals T ∀ (g : G), ∃! s : S, -s + g T
theorem Subgroup.isComplement_iff_existsUnique_mul_inv_mem {G : Type u_1} [Group G] {S T : Set G} :
IsComplement S T ∀ (g : G), ∃! t : T, g * (↑t)⁻¹ S
theorem AddSubgroup.isComplement_iff_existsUnique_add_neg_mem {G : Type u_1} [AddGroup G] {S T : Set G} :
IsComplement S T ∀ (g : G), ∃! t : T, g + -t S
@[deprecated Subgroup.isComplement_iff_existsUnique_mul_inv_mem (since := "2024-12-18")]
theorem Subgroup.mem_rightTransversals_iff_existsUnique_mul_inv_mem {G : Type u_1} [Group G] {S T : Set G} :
S rightTransversals T ∀ (g : G), ∃! s : S, g * (↑s)⁻¹ T
@[deprecated Subgroup.isComplement_iff_existsUnique_mul_inv_mem (since := "2024-12-18")]
theorem AddSubgroup.mem_rightTransversals_iff_existsUnique_add_neg_mem {G : Type u_1} [AddGroup G] {S T : Set G} :
S rightTransversals T ∀ (g : G), ∃! s : S, g + -s T
theorem Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} :
IsComplement S H ∀ (q : G H), ∃! s : S, s = q
@[deprecated Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'' (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'' (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_right_iff_bijective (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_right_iff_bijective (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_left_iff_bijective (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_subgroup_left_iff_bijective (since := "2024-12-18")]
theorem Subgroup.IsComplement.card_left {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : IsComplement S H) :
theorem AddSubgroup.IsComplement.card_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : IsComplement S H) :
@[deprecated Subgroup.IsComplement.card_left (since := "2024-12-18")]
theorem Subgroup.card_left_transversal {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S leftTransversals H) :
@[deprecated Subgroup.IsComplement.card_left (since := "2024-12-18")]
theorem AddSubgroup.card_left_transversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S leftTransversals H) :
theorem Subgroup.IsComplement.card_right {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (h : IsComplement (↑H) T) :
theorem AddSubgroup.IsComplement.card_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (h : IsComplement (↑H) T) :
@[deprecated Subgroup.IsComplement.card_right (since := "2024-12-18")]
theorem Subgroup.card_right_transversal {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S rightTransversals H) :
@[deprecated Subgroup.IsComplement.card_right (since := "2024-12-18")]
theorem AddSubgroup.card_right_transversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S rightTransversals H) :
theorem Subgroup.isComplement_range_left {G : Type u_1} [Group G] {H : Subgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
theorem AddSubgroup.isComplement_range_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
@[deprecated Subgroup.isComplement_range_left (since := "2024-12-18")]
theorem Subgroup.range_mem_leftTransversals {G : Type u_1} [Group G] {H : Subgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
@[deprecated Subgroup.isComplement_range_left (since := "2024-12-18")]
theorem AddSubgroup.range_mem_leftTransversals {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
@[deprecated Subgroup.isComplement_range_right (since := "2024-12-18")]
@[deprecated Subgroup.isComplement_range_right (since := "2024-12-18")]
theorem Subgroup.exists_isComplement_left {G : Type u_1} [Group G] (H : Subgroup G) (g : G) :
∃ (S : Set G), IsComplement S H g S
theorem AddSubgroup.exists_isComplement_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) :
∃ (S : Set G), IsComplement S H g S
@[deprecated Subgroup.exists_isComplement_left (since := "2024-12-18")]
theorem Subgroup.exists_left_transversal {G : Type u_1} [Group G] (H : Subgroup G) (g : G) :
SleftTransversals H, g S
@[deprecated Subgroup.exists_isComplement_left (since := "2024-12-18")]
theorem AddSubgroup.exists_left_transversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) :
SleftTransversals H, g S
theorem Subgroup.exists_isComplement_right {G : Type u_1} [Group G] (H : Subgroup G) (g : G) :
∃ (T : Set G), IsComplement (↑H) T g T
theorem AddSubgroup.exists_isComplement_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) :
∃ (T : Set G), IsComplement (↑H) T g T
@[deprecated Subgroup.exists_isComplement_right (since := "2024-12-18")]
theorem Subgroup.exists_right_transversal {G : Type u_1} [Group G] (H : Subgroup G) (g : G) :
SrightTransversals H, g S
@[deprecated Subgroup.exists_isComplement_right (since := "2024-12-18")]
theorem AddSubgroup.exists_right_transversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) :
SrightTransversals H, g S
theorem Subgroup.exists_left_transversal_of_le {G : Type u_1} [Group G] {H' H : Subgroup G} (h : H' H) :
∃ (S : Set G), S * H' = H Nat.card S * Nat.card H' = Nat.card H

Given two subgroups H' ⊆ H, there exists a left transversal to H' inside H.

theorem AddSubgroup.exists_left_transversal_of_le {G : Type u_1} [AddGroup G] {H' H : AddSubgroup G} (h : H' H) :
∃ (S : Set G), S + H' = H Nat.card S * Nat.card H' = Nat.card H

Given two subgroups H' ⊆ H, there exists a transversal to H' inside H

theorem Subgroup.exists_right_transversal_of_le {G : Type u_1} [Group G] {H' H : Subgroup G} (h : H' H) :
∃ (S : Set G), H' * S = H Nat.card H' * Nat.card S = Nat.card H

Given two subgroups H' ⊆ H, there exists a right transversal to H' inside H.

theorem AddSubgroup.exists_right_transversal_of_le {G : Type u_1} [AddGroup G] {H' H : AddSubgroup G} (h : H' H) :
∃ (S : Set G), H' + S = H Nat.card H' * Nat.card S = Nat.card H

Given two subgroups H' ⊆ H, there exists a transversal to H' inside H

noncomputable def Subgroup.IsComplement.equiv {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) :
G S × T

The equivalence G ≃ S × T, such that the inverse is (*) : S × T → G

Equations
@[simp]
theorem Subgroup.IsComplement.equiv_symm_apply {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (x : S × T) :
hST.equiv.symm x = x.1 * x.2
@[simp]
theorem Subgroup.IsComplement.equiv_fst_mul_equiv_snd {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (g : G) :
(hST.equiv g).1 * (hST.equiv g).2 = g
theorem Subgroup.IsComplement.equiv_fst_eq_mul_inv {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (g : G) :
(hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹
theorem Subgroup.IsComplement.equiv_snd_eq_inv_mul {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (g : G) :
(hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g
theorem Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S K) {g₁ g₂ : G} :
(hSK.equiv g₁).1 = (hSK.equiv g₂).1 LeftCosetEquivalence (↑K) g₁ g₂
theorem Subgroup.IsComplement.equiv_snd_eq_iff_rightCosetEquivalence {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) {g₁ g₂ : G} :
(hHT.equiv g₁).2 = (hHT.equiv g₂).2 RightCosetEquivalence (↑H) g₁ g₂
theorem Subgroup.IsComplement.leftCosetEquivalence_equiv_fst {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S K) (g : G) :
LeftCosetEquivalence (↑K) g (hSK.equiv g).1
theorem Subgroup.IsComplement.rightCosetEquivalence_equiv_snd {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) (g : G) :
RightCosetEquivalence (↑H) g (hHT.equiv g).2
theorem Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 T) (hg : g S) :
(hST.equiv g).1 = g, hg
theorem Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 S) (hg : g T) :
(hST.equiv g).2 = g, hg
theorem Subgroup.IsComplement.equiv_snd_eq_one_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 T) (hg : g S) :
(hST.equiv g).2 = 1, h1
theorem Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 S) (hg : g T) :
(hST.equiv g).1 = 1, h1
theorem Subgroup.IsComplement.equiv_mul_right {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S K) (g : G) (k : K) :
hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
theorem Subgroup.IsComplement.equiv_mul_right_of_mem {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S K) {g k : G} (h : k K) :
hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k, h)
theorem Subgroup.IsComplement.equiv_mul_left {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) (h : H) (g : G) :
hHT.equiv (h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)
theorem Subgroup.IsComplement.equiv_mul_left_of_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) {h g : G} (hh : h H) :
hHT.equiv (h * g) = (h, hh * (hHT.equiv g).1, (hHT.equiv g).2)
theorem Subgroup.IsComplement.equiv_one {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (hs1 : 1 S) (ht1 : 1 T) :
hST.equiv 1 = (1, hs1, 1, ht1)
theorem Subgroup.IsComplement.equiv_fst_eq_self_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 T) :
(hST.equiv g).1 = g g S
theorem Subgroup.IsComplement.equiv_snd_eq_self_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 S) :
(hST.equiv g).2 = g g T
theorem Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 S) :
(hST.equiv g).1 = 1 g T
theorem Subgroup.IsComplement.coe_equiv_snd_eq_one_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 T) :
(hST.equiv g).2 = 1 g S
noncomputable def Subgroup.IsComplement.leftQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) :
G H S

A left transversal is in bijection with left cosets.

Equations
noncomputable def AddSubgroup.IsComplement.leftQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S H) :
G H S

A left transversal is in bijection with left cosets.

Equations
@[deprecated Subgroup.IsComplement.leftQuotientEquiv (since := "2024-12-28")]
def Subgroup.MemLeftTransversals.toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) :
G H S

Alias of Subgroup.IsComplement.leftQuotientEquiv.


A left transversal is in bijection with left cosets.

Equations
theorem Subgroup.IsComplement.finite_left_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : IsComplement S H) :

A left transversal is finite iff the subgroup has finite index.

theorem AddSubgroup.IsComplement.finite_left_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : IsComplement S H) :

A left transversal is finite iff the subgroup has finite index.

@[deprecated Subgroup.IsComplement.finite_left_iff (since := "2024-12-28")]
theorem Subgroup.MemLeftTransversals.finite_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : IsComplement S H) :

Alias of Subgroup.IsComplement.finite_left_iff.


A left transversal is finite iff the subgroup has finite index.

theorem Subgroup.IsComplement.finite_left {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} [H.FiniteIndex] (hS : IsComplement S H) :
theorem AddSubgroup.IsComplement.finite_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} [H.FiniteIndex] (hS : IsComplement S H) :
@[deprecated Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv (since := "2024-12-28")]
theorem Subgroup.MemLeftTransversals.mk''_toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) (q : G H) :

Alias of Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv.

theorem Subgroup.IsComplement.leftQuotientEquiv_apply {G : Type u_1} [Group G] {H : Subgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
(.leftQuotientEquiv q) = f q
theorem AddSubgroup.IsComplement.leftQuotientEquiv_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
(.leftQuotientEquiv q) = f q
@[deprecated Subgroup.IsComplement.leftQuotientEquiv_apply (since := "2024-12-28")]
theorem Subgroup.MemLeftTransversals.toEquiv_apply {G : Type u_1} [Group G] {H : Subgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
(.leftQuotientEquiv q) = f q

Alias of Subgroup.IsComplement.leftQuotientEquiv_apply.

noncomputable def Subgroup.IsComplement.toLeftFun {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) :
GS

A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

Equations
noncomputable def AddSubgroup.IsComplement.toLeftFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S H) :
GS

A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

Equations
@[deprecated Subgroup.IsComplement.toLeftFun (since := "2024-12-28")]
def Subgroup.MemLeftTransversals.toFun {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) :
GS

Alias of Subgroup.IsComplement.toLeftFun.


A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

Equations
theorem Subgroup.IsComplement.inv_toLeftFun_mul_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) (g : G) :
(↑(hS.toLeftFun g))⁻¹ * g H
theorem AddSubgroup.IsComplement.neg_toLeftFun_add_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S H) (g : G) :
-(hS.toLeftFun g) + g H
@[deprecated Subgroup.IsComplement.inv_toLeftFun_mul_mem (since := "2024-12-28")]
theorem Subgroup.MemLeftTransversals.inv_toFun_mul_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) (g : G) :
(↑(hS.toLeftFun g))⁻¹ * g H

Alias of Subgroup.IsComplement.inv_toLeftFun_mul_mem.

theorem Subgroup.IsComplement.inv_mul_toLeftFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) (g : G) :
g⁻¹ * (hS.toLeftFun g) H
theorem AddSubgroup.IsComplement.neg_add_toLeftFun_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S H) (g : G) :
-g + (hS.toLeftFun g) H
@[deprecated Subgroup.IsComplement.inv_mul_toLeftFun_mem (since := "2024-12-28")]
theorem Subgroup.MemLeftTransversals.inv_mul_toFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S H) (g : G) :
g⁻¹ * (hS.toLeftFun g) H

Alias of Subgroup.IsComplement.inv_mul_toLeftFun_mem.

noncomputable def Subgroup.IsComplement.rightQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) :

A right transversal is in bijection with right cosets.

Equations
noncomputable def AddSubgroup.IsComplement.rightQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) :

A right transversal is in bijection with right cosets.

Equations
@[deprecated Subgroup.IsComplement.rightQuotientEquiv (since := "2024-12-28")]
def Subgroup.MemRightTransversals.toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) :

Alias of Subgroup.IsComplement.rightQuotientEquiv.


A right transversal is in bijection with right cosets.

Equations
theorem Subgroup.IsComplement.finite_right_iff {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (h : IsComplement (↑H) T) :

A right transversal is finite iff the subgroup has finite index.

theorem AddSubgroup.IsComplement.finite_right_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (h : IsComplement (↑H) T) :

A right transversal is finite iff the subgroup has finite index.

@[deprecated Subgroup.IsComplement.finite_right_iff (since := "2024-12-28")]
theorem Subgroup.MemRightTransversals.finite_iff {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (h : IsComplement (↑H) T) :

Alias of Subgroup.IsComplement.finite_right_iff.


A right transversal is finite iff the subgroup has finite index.

theorem Subgroup.IsComplement.finite_right {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} [H.FiniteIndex] (hT : IsComplement (↑H) T) :
theorem AddSubgroup.IsComplement.finite_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} [H.FiniteIndex] (hT : IsComplement (↑H) T) :
@[deprecated Subgroup.IsComplement.mk''_rightQuotientEquiv (since := "2024-12-28")]

Alias of Subgroup.IsComplement.mk''_rightQuotientEquiv.

@[deprecated Subgroup.IsComplement.rightQuotientEquiv_apply (since := "2024-12-28")]

Alias of Subgroup.IsComplement.rightQuotientEquiv_apply.

noncomputable def Subgroup.IsComplement.toRightFun {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) :
GT

A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

Equations
noncomputable def AddSubgroup.IsComplement.toRightFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) :
GT

A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

Equations
@[deprecated Subgroup.IsComplement.toRightFun (since := "2024-12-28")]
def Subgroup.MemRightTransversals.toFun {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) :
GT

Alias of Subgroup.IsComplement.toRightFun.


A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

Equations
theorem Subgroup.IsComplement.mul_inv_toRightFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) :
g * (↑(hT.toRightFun g))⁻¹ H
theorem AddSubgroup.IsComplement.add_neg_toRightFun_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) :
g + -(hT.toRightFun g) H
@[deprecated Subgroup.IsComplement.mul_inv_toRightFun_mem (since := "2024-12-28")]
theorem Subgroup.MemRighTransversals.mul_inv_toFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) :
g * (↑(hT.toRightFun g))⁻¹ H

Alias of Subgroup.IsComplement.mul_inv_toRightFun_mem.

theorem Subgroup.IsComplement.toRightFun_mul_inv_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) :
(hT.toRightFun g) * g⁻¹ H
theorem AddSubgroup.IsComplement.toRightFun_add_neg_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) :
(hT.toRightFun g) + -g H
@[deprecated Subgroup.IsComplement.toRightFun_mul_inv_mem (since := "2024-12-28")]
theorem Subgroup.MemRighTransversals.toFun_mul_inv_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) :
(hT.toRightFun g) * g⁻¹ H

Alias of Subgroup.IsComplement.toRightFun_mul_inv_mem.

@[reducible, inline]
abbrev Subgroup.LeftTransversal {G : Type u_1} [Group G] (H : Subgroup G) :
Type u_1

The collection of left transversals of a subgroup

Equations
@[reducible, inline]
abbrev AddSubgroup.LeftTransversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
Type u_1

The collection of left transversals of a subgroup.

Equations
@[reducible, inline]
abbrev Subgroup.RightTransversal {G : Type u_1} [Group G] (H : Subgroup G) :
Type u_1

The collection of right transversals of a subgroup

Equations
@[reducible, inline]
abbrev AddSubgroup.RightTransversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
Type u_1

The collection of right transversals of a subgroup.

Equations
noncomputable instance Subgroup.instMulActionLeftTransversal {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] :
Equations
Equations
theorem Subgroup.smul_toLeftFun {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (g : G) :
f (.toLeftFun g) = (.toLeftFun (f g))
theorem AddSubgroup.vadd_toLeftFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (g : G) :
f +ᵥ (.toLeftFun g) = (.toLeftFun (f +ᵥ g))
theorem Subgroup.smul_leftQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G H) :
f (.leftQuotientEquiv q) = (.leftQuotientEquiv (f q))
theorem AddSubgroup.vadd_leftQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G H) :
f +ᵥ (.leftQuotientEquiv q) = (.leftQuotientEquiv (f +ᵥ q))
theorem Subgroup.smul_apply_eq_smul_apply_inv_smul {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G H) :
(.leftQuotientEquiv q) = f (.leftQuotientEquiv (f⁻¹ q))
theorem AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G H) :
(.leftQuotientEquiv q) = f +ᵥ (.leftQuotientEquiv (-f +ᵥ q))
theorem Subgroup.IsComplement'.isCompl {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) :
theorem Subgroup.IsComplement'.sup_eq_top {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) :
HK =
theorem Subgroup.IsComplement'.disjoint {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) :
noncomputable def Subgroup.IsComplement'.QuotientMulEquiv {G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) :
G K ≃* H

If H and K are complementary with K normal, then G ⧸ K is isomorphic to H.

Equations
@[simp]
theorem Subgroup.IsComplement.card_mul {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) :
theorem Subgroup.IsComplement'.card_mul {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) :
theorem Subgroup.isComplement'_of_disjoint_and_mul_eq_univ {G : Type u_1} [Group G] {H K : Subgroup G} (h1 : Disjoint H K) (h2 : H * K = Set.univ) :
theorem Subgroup.isComplement'_of_card_mul_and_disjoint {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] (h1 : Nat.card H * Nat.card K = Nat.card G) (h2 : Disjoint H K) :
theorem Subgroup.isComplement'_of_coprime {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] (h1 : Nat.card H * Nat.card K = Nat.card G) (h2 : (Nat.card H).Coprime (Nat.card K)) :
theorem Subgroup.isComplement'_stabilizer {G : Type u_1} [Group G] {H : Subgroup G} {α : Type u_2} [MulAction G α] (a : α) (h1 : ∀ (h : H), h a = ah = 1) (h2 : ∀ (g : G), ∃ (h : H), h g a = a) :