instZero — Mathlib

English

There is a distinguished zero element in LieDerivation, whose associated linear map is the zero map and which satisfies a Leibniz rule with respect to the bracket equal to zero.

Русский

Существует нулевой элемент в пространстве LieDerivation, соответствующий нулевому линейному отображению и удовлетворяющий нулевому правилу Лейбница относительно скобки.

LaTeX

$$$0_{\text{LieDerivation } R\, L\, M} \text{ is the element with } (toLinearMap = 0, \; leibniz' = \text{fun } a b \mapsto 0)$$$

Lean4

instance instZero : Zero (LieDerivation R L M) where
  zero :=
    { toLinearMap := 0
      leibniz' := fun a b => by simp only [LinearMap.zero_apply, lie_zero, sub_self] }

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