instAdd — Mathlib

English

There exists a zero element in the type of left-invariant derivations, acting as the additive identity.

Русский

Существует нулевой элемент в типе левых инвариантных выводов, служащий нулём по сложению.

LaTeX

$$$0_{\,\\text{LID}} \\in \\text{LeftInvariantDerivation } I G$$$

Lean4

instance : Add (LeftInvariantDerivation I G) where add X Y := ⟨X + Y, fun g => by simp only [map_add, left_invariant']⟩

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