coe_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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