toLinearMap — Mathlib

English

The evaluation of a sum respects addition in the domain of functions, i.e., (f+g)(m) = f(m) + g(m) holds as a basic axiom of the additive structure.

Русский

Значение суммы отображений согласуется со сложением внутри области функций: (f+g)(m) = f(m) + g(m).

LaTeX

$$$ (f+g) m = f m + g m $$$

Lean4

/-- If `f` is a multilinear map, then `f.toLinearMap m i` is the linear map obtained by fixing all
coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate. -/
@[simps]
def toLinearMap [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : M₁ i →ₗ[R] M₂
    where
  toFun x := f (update m i x)
  map_add' x y := by simp
  map_smul' c x := by simp

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