independent_of_coprime_order — Mathlib

English

If pairwise the orders of H_i are coprime and the images mutually commute, then iSupIndep H holds.

Русский

Если попарно порядки подгрупп H_i взаимно просты и образы коммутируют, то iSupIndep H.

LaTeX

$$$ iSupIndep H $ under coprime orders.$$

Lean4

@[to_additive]
theorem independent_of_coprime_order (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
    [Finite ι] [∀ i, Fintype (H i)]
    (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) : iSupIndep H := by
  simpa using
    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype) (commute_subtype_of_commute hcomm) hcoprime

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