coe_add — Mathlib

English

Let f, g be Lie module homomorphisms M → N. The underlying function of their sum is the pointwise sum: (f+g)(m) = f(m) + g(m) for all m ∈ M.

Русский

Пусть f, g — гомоморфизмы модулей Ли M → N. Виток функции f+g равен сумме значений по точкам: (f+g)(m) = f(m) + g(m) для всех m ∈ M.

LaTeX

$$$\forall m \in M:\ (f+g)(m) = f(m) + g(m)$$$

Lean4

@[norm_cast, simp]
theorem coe_add (f g : M →ₗ⁅R,L⁆ N) : ⇑(f + g) = f + g :=
  rfl

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