normal_op — Mathlib

English

A subgroup of G has its opposite normal if and only if the original subgroup is normal; normality is preserved by taking opposites.

Русский

Подгруппа G имеет нормальную противоположную подпогруппу ⇔ исходная подпгруппа нормальна; нормальность сохраняется при переходе кOpposite.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem normal_op {H : Subgroup G} : H.op.Normal ↔ H.Normal := by
  simp only [← normalizer_eq_top_iff, ← op_normalizer, op_eq_top]

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