map_update_zero — Mathlib

English

Let f be a multilinear map in finitely many coordinates. If we fix all coordinates except the i-th one and replace the i-th coordinate by 0, the value of f is 0. In particular, substituting any coordinate by zero annihilates the output.

Русский

Пусть f — многолинейное отображение в конечном числе координат. Если зафиксировать все координаты кроме i-й и заменить i-ю координату на 0, результат f равен 0. В частности, если любая координата равна нулю, выходное значение равно нулю.

LaTeX

$$$\forall i,\forall m: (m_j)_{j\in ι}\, ,\; f(\text{update}(m,i,0)) = 0$$$

Lean4

@[simp]
theorem map_update_zero [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : f (update m i 0) = 0 :=
  f.map_coord_zero i (update_self i 0 m)

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