map_zero — Mathlib

English

The zero multilinear map is the identically zero map: for every input, the output is zero.

Русский

Нулевая много-линейная карта является тождественно нулевой: для любого входа выход равен нулю.

LaTeX

$$$\forall m: (0 : \text{MultilinearMap } R M_1 M_2)\, m = 0$$$

Lean4

@[simp]
theorem map_zero [Nonempty ι] : f 0 = 0 :=
  by
  obtain ⟨i, _⟩ : ∃ i : ι, i ∈ Set.univ := Set.exists_mem_of_nonempty ι
  exact map_coord_zero f i rfl

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