commutator_characteristic — Mathlib

English

If H1 and H2 are characteristic, then [H1,H2] is characteristic.

Русский

Если H1 и H2 характеристичны, то их коммутатор характеристичен.

LaTeX

$$$$ [H_1, H_2] \\text{ is characteristic} $$$$

Lean4

instance commutator_characteristic [h₁ : Characteristic H₁] [h₂ : Characteristic H₂] : Characteristic ⁅H₁, H₂⁆ :=
  characteristic_iff_le_map.mpr fun ϕ =>
    commutator_le_map_commutator (characteristic_iff_le_map.mp h₁ ϕ) (characteristic_iff_le_map.mp h₂ ϕ)

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