op_bot

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

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

English

Taking opposites preserves the bottom subgroup: (⊥ in G)^{op} = ⊥ in G^{op}.

Русский

Противоположная подгруппа к нулевой (нижней) подгруппе совпадает с нулевой подгруппой противоположной группы.

LaTeX

$$ (⊥ : Subgroup G).op = ⊥ $$

Lean4

@[to_additive (attr := simp)]
theorem op_bot : (⊥ : Subgroup G).op = ⊥ :=
  opEquiv.map_bot

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

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

Разделы

Аффилиация

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