conjugates_subset_normal — Mathlib

English

Let N be a normal subgroup of G and a ∈ N. Then every conjugate of a lies in N.

Русский

Пусть N — нормальная подгруппа G и a ∈ N. Тогда каждый конъюгат a принадлежит N.

LaTeX

$$$ N \trianglelefteq G, \ a \in N \Rightarrow \mathrm{conjugatesOf}(a) \subseteq N $$$

Lean4

theorem conjugates_subset_normal {N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) : conjugatesOf a ⊆ N :=
  by
  rintro a hc
  obtain ⟨c, rfl⟩ := isConj_iff.1 hc
  exact tn.conj_mem a h c

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