conj_mem' — Mathlib

English

Let H be a normal subgroup of G. Then for every n in H and every g in G, the conjugate g^{-1} n g lies in H.

Русский

Пусть H — нормальная подгруппа G. Тогда для любого n ∈ H и любого g ∈ G сопряжение g^{-1} n g принадлежит H.

LaTeX

$$$H \\trianglelefteq G \\Rightarrow \\forall n \\in H, \\forall g \\in G, g^{-1} n g \\in H$$$

Lean4

@[to_additive]
theorem conj_mem' (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) : g⁻¹ * n * g ∈ H :=
  by
  convert nH.conj_mem n hn g⁻¹
  rw [inv_inv]

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