instLieRingModuleSubtypeMem — Mathlib

English

The zero element maps to zero under the submodule inclusion.

Русский

Ноль отображается в ноль при вложении подмодуля.

LaTeX

$$$ ((0 : N) : M) = (0 : M) $$$

Lean4

instance : LieRingModule L N
    where
  bracket (x : L) (m : N) := ⟨⁅x, m.val⁆, N.lie_mem m.property⟩
  add_lie := by intro x y m; apply SetCoe.ext; apply add_lie
  lie_add := by intro x m n; apply SetCoe.ext; apply lie_add
  leibniz_lie := by intro x y m; apply SetCoe.ext; apply leibniz_lie

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