smul_subtype — Mathlib

English

For P ≤ H and h ∈ G, the induced action on the inclusion P ↪ H matches the inclusion h · P ↪ h · H; i.e., h · (P.subtype hP) = (h · P).subtype (smul_le hP h).

Русский

Для P ≤ H и h ∈ G равенство между отображением смул на вложение P ↪ H и вложением h · P ↪ h · H.

LaTeX

$$$h \\cdot (P \\hookrightarrow H) = (h \\cdot P) \\hookrightarrow (h \\cdot H).$$$

Lean4

theorem smul_subtype {P : Sylow p G} {H : Subgroup G} (hP : P ≤ H) (h : H) :
    h • P.subtype hP = (h • P).subtype (smul_le hP h) :=
  ext (Subgroup.conj_smul_subgroupOf hP h)

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