ker_transferSylow_disjoint — Mathlib

English

For any p-subgroup Q of G, the kernel of the transferSylow map is disjoint from Q.

Русский

Для любой p-подгруппы Q группы G ядро переноса Sylow дистинктно относительно Q.

LaTeX

$$Disjoint (\ker(\operatorname{transferSylow}(P,hP))) Q$$

Lean4

theorem ker_transferSylow_disjoint (Q : Subgroup G) (hQ : IsPGroup p Q) : Disjoint (transferSylow P hP).ker Q :=
  disjoint_iff.mpr <|
    card_eq_one.mp <|
      (hQ.to_le inf_le_right).card_eq_or_dvd.resolve_right fun h =>
        not_dvd_card_ker_transferSylow P hP <| h.trans <| card_dvd_of_le inf_le_left

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