map_insertNth_add — Mathlib

English

Scaling the inserted element commutes with f: f(p.insertNth (c•x) m) = c•f(p.insertNth x m).

Русский

Умножение вставляемого элемента на скаляр коммутирует с f: f(p.insertNth (c•x) m) = c•f(p.insertNth x m).

LaTeX

$$$ f( p.insertNth (c \cdot x) m ) = c \cdot f( p.insertNth x m ) $$$

Lean4

theorem map_insertNth_add (f : MultilinearMap R M M₂) (p : Fin (n + 1)) (m : ∀ i, M (p.succAbove i)) (x y : M p) :
    f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m) := by
  simpa using f.map_update_add (p.insertNth 0 m) p x y

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