normal_unop

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

URI: https://scilib.ai/kg/mathlib#Subgroup.normal_unop

English

A normal subgroup of the opposite group yields a normal subgroup when taking unop, and vice versa.

Русский

Нормальная подпгруппа в G^{op} имеет нормальность при применении unop и обратно.

LaTeX

$$$H^{unop}.Normal \iff H.Normal$$$

Lean4

@[to_additive (attr := simp)]
theorem normal_unop {H : Subgroup Gᵐᵒᵖ} : H.unop.Normal ↔ H.Normal := by rw [← normal_op, op_unop]

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

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

Разделы

Аффилиация

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