to_le — Mathlib

English

If K is a larger subgroup and H ≤ K, then p-group property passes from K to H.

Русский

Если H ≤ K и K — p-группа, то H — p-группа.

LaTeX

$$$\IsPGroup(p,K) \rightarrow H \le K \rightarrow \IsPGroup(p,H)$$$

Lean4

theorem to_le {H K : Subgroup G} (hK : IsPGroup p K) (hHK : H ≤ K) : IsPGroup p H :=
  hK.of_injective (Subgroup.inclusion hHK) fun a b h =>
    Subtype.ext
      (by
        change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b
        apply Subtype.ext_iff.mp h)

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