replicateRow_inj

Mathlib.LinearAlgebra.Matrix.RowCol

URI: https://scilib.ai/kg/mathlib#Matrix.replicateRow_inj

English

There exists an equivalence: replicateRow ι v = replicateRow ι w iff v = w.

Русский

Существует равносильность: replicateRow ι v = replicateRow ι w iff v = w.

LaTeX

$$$ \ replicateRow\ ι v = replicateRow\ ι w \iff v = w $$$

Lean4

@[simp]
theorem replicateRow_inj [Nonempty ι] {v w : n → α} : replicateRow ι v = replicateRow ι w ↔ v = w :=
  replicateRow_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru