conj_smul_le_of_le — Mathlib

English

If P ≤ H and h ∈ H, then the conjugation by h sends P into H: (conj h) · P ≤ H.

Русский

Если P≤H и h∈H, то сопряжение на P помещает P внутри H: (conj h) · P ≤ H.

LaTeX

$$$ (\mathrm{MulAut.conj}(h)) \cdot P \le H \quad \text{for } h \in H $$$

Lean4

theorem conj_smul_le_of_le {P H : Subgroup G} (hP : P ≤ H) (h : H) : MulAut.conj (h : G) • P ≤ H :=
  by
  rintro - ⟨g, hg, rfl⟩
  exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

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