replicateCol_eq_zero — Mathlib

English

For any v, replicateCol ι v = 0 iff v = 0, assuming a zero-type and a nonempty index set.

Русский

Для любого v: если replicateCol ι v = 0, то v = 0 и наоборот (при наличии нулевого типа и ненулевого множества индексов).

LaTeX

$$$ \ replicateCol\ ι v = 0 \iff v = 0 $$$

Lean4

@[simp]
theorem replicateCol_eq_zero [Zero α] [Nonempty ι] (v : m → α) : replicateCol ι v = 0 ↔ v = 0 :=
  replicateCol_inj

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