map_insertNth_smul — Mathlib

English

A different presentation of the same property: scaling the inserted coordinate commutes with the multilinear map evaluation.

Русский

Другая формулировка того же свойства: масштабирование вставляемой координаты коммутирует с оценкой мультилейного отображения.

LaTeX

$$$ f( p.insertNth (instHSMul.hSMul c x) m ) = instHSMul.hSMul c ( f( p.insertNth x m ) ) $$$

Lean4

theorem map_insertNth_smul (f : MultilinearMap R M M₂) (p : Fin (n + 1)) (m : ∀ i, M (p.succAbove i)) (c : R)
    (x : M p) : f (p.insertNth (c • x) m) = c • f (p.insertNth x m) := by
  simpa using f.map_update_smul (p.insertNth 0 m) p c x

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