smul_le — Mathlib

English

If P ≤ H are subgroups of G and h ∈ G, then h · P ≤ H whenever P ≤ H; i.e., conjugation by h preserves inclusion of subgroups.

Русский

Если P ≤ H — подгруппы G и h ∈ G, то h · P ≤ H при P ≤ H; т.е. сопряжение сохраняет вложение подгрупп.

LaTeX

$$$h P h^{-1} \\le H \\quad\\text{whenever } P \\le H.$$$

Lean4

theorem smul_le {P : Sylow p G} {H : Subgroup G} (hP : P ≤ H) (h : H) : ↑(h • P) ≤ H :=
  Subgroup.conj_smul_le_of_le hP h

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