exists_right_complement'_of_coprime

English

A group with finite commutator set has a finite commutator subgroup.

Русский

Группа с конечным множеством коммутаторов имеет конечную коммутаторную подгруппу.

LaTeX

$$Finite(card(commutatorSet G)) → Finite(commutator G)$$

Lean4

/-- **Schur-Zassenhaus** for normal subgroups:
  If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
  subgroup `K` which is a (right) complement of `H`. -/
theorem exists_right_complement'_of_coprime {N : Subgroup G} [N.Normal] (hN : Nat.Coprime (Nat.card N) N.index) :
    ∃ H : Subgroup G, IsComplement' N H := by
  by_cases hN1 : Nat.card N = 0
  · rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN
    rw [hN]
    exact ⟨⊥, isComplement'_top_bot⟩
  by_cases hN2 : N.index = 0
  · rw [hN2, Nat.coprime_zero_right] at hN
    haveI := (Cardinal.toNat_eq_one_iff_unique.mp hN).1
    rw [N.eq_bot_of_subsingleton]
    exact ⟨⊤, isComplement'_bot_top⟩
  have hN3 : Nat.card G ≠ 0 := by
    rw [← N.card_mul_index]
    exact mul_ne_zero hN1 hN2
  haveI := (Cardinal.lt_aleph0_iff_fintype.mp (lt_of_not_ge (mt Cardinal.toNat_apply_of_aleph0_le hN3))).some
  exact exists_right_complement'_of_coprime_aux' rfl hN

Похожие утверждения