isComplement'_stabilizer_of_coprime

English

For coprime coprime parameters, the stabilizer of α is complemented by a subgroup.

Русский

При взаимно простых параметрах стабилизатор α имеет дополнение-подгруппу.

LaTeX

$$IsComplement' H (stabilizer G α)$$

Lean4

theorem isComplement'_stabilizer_of_coprime {α : H.QuotientDiff} (hH : Nat.Coprime (Nat.card H) H.index) :
    IsComplement' H (stabilizer G α) :=
  isComplement'_stabilizer α (eq_one_of_smul_eq_one hH α) fun g => exists_smul_eq hH (g • α) α

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