op_normalizer — Mathlib

English

The normalizer commutes with taking opposites: for any H ≤ G, H.normalizer^{op} = H^{op}.normalizer.

Русский

Нормализатор коммутирует с операцией противоположности: для любой подгруппы H ⊆ G выполняется H.normalizer^{op} = H^{op}.normalizer.

LaTeX

$$H.normalizer^{op} = H^{op}.normalizer$$

Lean4

@[to_additive]
theorem op_normalizer (H : Subgroup G) : H.normalizer.op = H.op.normalizer :=
  by
  ext x
  simp [mem_normalizer_iff', iff_comm]

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