map_coord_zero — Mathlib

English

Let f be a multilinear map. If some coordinate i of the input function m is zero, then f(m) = 0.

Русский

Пусть f — много линейное отображение. Если какая-либо координата i входной функции m равна нулю, то f(m) = 0.

LaTeX

$$$ \exists i, m(i) = 0 \Rightarrow f(m) = 0 $$$

Lean4

theorem map_coord_zero {m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0 := by
  classical
  have : (0 : R) • (0 : M₁ i) = 0 := by simp
  rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]

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