lie_zsmul — Mathlib

English

Let x ∈ L, m ∈ M and a ∈ Z. Then the adjoint action of x on a·m commutes with integer scaling: [x, a·m] = a·[x, m].

Русский

Пусть x ∈ L, m ∈ M и a ∈ Z. Тогда действие соседствия x на a·m коммутирует с целочисленным умножением: [x, a·m] = a·[x, m].

LaTeX

$$$[x, a \cdot m] = a \cdot [x, m]$$$

Lean4

theorem lie_zsmul (a : ℤ) : ⁅x, a • m⁆ = a • ⁅x, m⁆ :=
  AddMonoidHom.map_zsmul { toFun := fun m : M => ⁅x, m⁆, map_zero' := lie_zero x, map_add' := fun _ _ => lie_add _ _ _ }
    _ _

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