add_apply — Mathlib

English

Evaluation of the sum of two multilinear maps at a point equals the sum of their evaluations: (f+g)(m) = f(m) + g(m).

Русский

Значение суммы двух мультилнейных отображений в точке равно сумме их значений: (f+g)(m) = f(m) + g(m).

LaTeX

$$$\forall f,g: MultilinearMap R M_1 M_2, \forall m, (f+g)(m) = f(m) + g(m)$$$

Lean4

@[simp]
theorem add_apply (m : ∀ i, M₁ i) : (f + f') m = f m + f' m :=
  rfl

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