lie_nsmul — Mathlib

English

Bracket is compatible with n-fold scalar action on the second argument: [x, n • m] = n [x, m].

Русский

Скобка совместима с n-разовым действием на втором аргументе: [x, n • m] = n [x, m].

LaTeX

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

Lean4

@[simp]
theorem lie_nsmul (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆ :=
  AddMonoidHom.map_nsmul { toFun := fun m : M => ⁅x, m⁆, map_zero' := lie_zero x, map_add' := fun _ _ => lie_add _ _ _ }
    _ _

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