lie_eq_smul — Mathlib

English

In a module M over a ring A, the Lie bracket with a scalar from A corresponds to the scalar action: for a ∈ A and m ∈ M, ⁅a, m⁆ = a · m.

Русский

Для элемента скаляра a ∈ A и вектора m ∈ M имеем ⁅a, m⁆ = a · m, т. е. скалярное действие задаёт Ли-действие.

LaTeX

$$$[a,m] = a\cdot m \quad (a \in A, \ m \in M).$$$

Lean4

theorem lie_eq_smul (a : A) (m : M) : ⁅a, m⁆ = a • m :=
  rfl

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