unop_normalizer — Mathlib

English

The normalizer of an opposite subgroup, when unop, equals the unop of the normalizer: (H^{op}).normalizer.unop = H.normalizer.unop.

Русский

Нормализатор противоположной подгруппы при преобразовании обратно равен нормализатору исходной подгруппы: (H^{op}).normalizer.unop = H.normalizer.unop.

LaTeX

$$H.normalizer.unop = H.unop.normalizer$$

Lean4

@[to_additive]
theorem unop_normalizer (H : Subgroup Gᵐᵒᵖ) : H.normalizer.unop = H.unop.normalizer := by
  rw [← op_inj, op_unop, op_normalizer, op_unop]

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