conj_smul_subgroupOf — Mathlib

English

Conjugating a subgroup of H by h corresponds to taking the subgroup of H generated by the conjugate: conj h • P.subgroupOf H = (conj h • P).subgroupOf H.

Русский

Сопряжение подгруппы P, вложенной в H, конъюгацией по h соответствует подгруппе H, образованной конъюгированием P: conj h • P.subgroupOf H = (conj h • P).subgroupOf H.

LaTeX

$$$ (\mathrm{MulAut.conj}(h)) \cdot (P.\mathrm{subgroupOf }H) = ((\mathrm{MulAut.conj}(h) \cdot P).\mathrm{subgroupOf }H) $$$

Lean4

theorem conj_smul_subgroupOf {P H : Subgroup G} (hP : P ≤ H) (h : H) :
    MulAut.conj h • P.subgroupOf H = (MulAut.conj (h : G) • P).subgroupOf H :=
  by
  refine le_antisymm ?_ ?_
  · rintro - ⟨g, hg, rfl⟩
    exact ⟨g, hg, rfl⟩
  · rintro p ⟨g, hg, hp⟩
    exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩

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