mem_comm_iff

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#Subgroup.Normal.mem_comm_iff

English

If H is normal in G, then a b ∈ H if and only if b a ∈ H for any a,b ∈ G.

Русский

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

LaTeX

$$$H \\trianglelefteq G \\Rightarrow (a b \\in H \\iff b a \\in H)$$$

Lean4

@[to_additive]
theorem mem_comm_iff (nH : H.Normal) {a b : G} : a * b ∈ H ↔ b * a ∈ H :=
  ⟨nH.mem_comm, nH.mem_comm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru