def conjugate {G : Type u_1} [Group G] (x : G) (H : Subgroup G) : Subgroup G

Equations

• conjugate x H = { carrier := {a : G | ∃ h ∈ H, a = x * h * x⁻¹}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem eq_bot_iff_card {G : Type u_1} [Group G] {H : Subgroup G} : H = ⊥ ↔ Nat.card ↥H = 1

theorem inf_bot_of_coprime {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (h : (Nat.card ↥H).Coprime (Nat.card ↥K)) : H ⊓ K = ⊥

inductive S : Type

• a: S
• b: S
• c: S

def myElement : FreeGroup S

Equations

• myElement = FreeGroup.of S.a * (FreeGroup.of S.b)⁻¹

def myMorphism : FreeGroup S →* Equiv.Perm (Fin 5)

Equations

• One or more equations did not get rendered due to their size.

def myGroup : Type

Equations

• myGroup = PresentedGroup {FreeGroup.of () ^ 3}

def myMap : Unit → Equiv.Perm (Fin 5)

Equations

• myMap x = (↑[1, 2, 3]).formPerm myMap.proof_2

theorem compat_myMap (r : FreeGroup Unit) : r ∈ {FreeGroup.of () ^ 3} → (FreeGroup.lift myMap) r = 1

def myNewMorphism : myGroup →* Equiv.Perm (Fin 5)

Equations

• myNewMorphism = PresentedGroup.toGroup compat_myMap

def CayleyIsoMorphism (G : Type u_1) [Group G] : G ≃* ↥(MulAction.toPermHom G G).range

Equations

• CayleyIsoMorphism G = Equiv.Perm.subgroupOfMulAction G G

theorem conjugate_one {G : Type u_1} [Group G] (H : Subgroup G) : conjugate 1 H = H

instance instMulActionSubgroup_leanCourse {G : Type u_1} [Group G] : MulAction G (Subgroup G)

Equations

• instMulActionSubgroup_leanCourse = MulAction.mk ⋯ ⋯

theorem aux_card_eq {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Finite G] (h' : Nat.card G = Nat.card ↥H * Nat.card ↥K) : Nat.card (G ⧸ H) = Nat.card ↥K

def iso₁ {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [H.Normal] [Fintype G] (h : Disjoint H K) (h' : Nat.card G = Nat.card ↥H * Nat.card ↥K) : ↥K ≃* G ⧸ H

Equations

• iso₁ h h' = sorryAx (↥K ≃* G ⧸ H)

def iso₂ {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [H.Normal] [K.Normal] : G ≃* (G ⧸ K) × G ⧸ H

Equations

• iso₂ = sorryAx (G ≃* (G ⧸ K) × G ⧸ H)

def finalIso {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} : G ≃* ↥H × ↥K

Equations

• finalIso = sorryAx (G ≃* ↥H × ↥K)