normalCore_idempotent — Mathlib

English

Normal core is idempotent: applying normalCore twice yields the same as once.

Русский

Нормальное ядро идемпотентно: повторное применение нормального ядра даёт то же, что и одно применение.

LaTeX

$$$ \\operatorname{normalCore}(\\operatorname{normalCore}(H)) = \\operatorname{normalCore}(H) $$$

Lean4

theorem normalCore_idempotent (H : Subgroup G) : H.normalCore.normalCore = H.normalCore :=
  H.normalCore.normalCore_eq_self

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