mem_comm — Mathlib

English

Let H be a normal subgroup of G. If ab ∈ H, then ba ∈ H for all a,b ∈ G.

Русский

Пусть H — нормальная подгруппа G. Если ab ∈ H, то ba ∈ H для всех a,b ∈ G.

LaTeX

$$$H \\trianglelefteq G \\Rightarrow \\forall a,b \\in G, ab \\in H \\Rightarrow ba \\in H$$$

Lean4

@[to_additive]
theorem mem_comm (nH : H.Normal) {a b : G} (h : a * b ∈ H) : b * a ∈ H :=
  by
  have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
  simpa

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