replicateCol_inj — Mathlib

English

For any nonempty ι, replicateCol ι v = replicateCol ι w if and only if v = w.

Русский

Для любого непустого ι копирование столбца сохраняет однозначность: replicateCol ι v = replicateCol ι w тогда и только тогда, когда v = w.

LaTeX

$$$$ \\mathrm{replicateCol}_{ι}(v) = \\mathrm{replicateCol}_{ι}(w) \\;\\Longleftrightarrow\\; v = w $$$$

Lean4

@[simp]
theorem replicateCol_inj [Nonempty ι] {v w : m → α} : replicateCol ι v = replicateCol ι w ↔ v = w :=
  replicateCol_injective.eq_iff

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