vec_inj

Mathlib.LinearAlgebra.Matrix.Vec

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

English

Vectorization is injective: if vec(A) = vec(B) then A = B, and conversely.

Русский

Векторизация инъективна: если vec(A) = vec(B), то A = B.

LaTeX

$$$$\operatorname{vec}(A) = \operatorname{vec}(B) \iff A = B$$$$

Lean4

theorem vec_inj {A B : Matrix m n R} : A.vec = B.vec ↔ A = B := by
  simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]

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

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

Разделы

Аффилиация

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