ext_of_single_vecMul — Mathlib

English

If vecMul applied to standard basis vectors yields the same results for two matrices, then the matrices are equal.

Русский

Если vecMul по базисным вектором даёт одинаковые результаты для двух матриц, матрицы равны.

LaTeX

$$If ∀ i, vecMul(Pi.single i 1) M = vecMul(Pi.single i 1) N then M = N.$$

Lean4

theorem ext_of_single_vecMul [DecidableEq m] [Fintype m] {M N : Matrix m n α}
    (h : ∀ i, Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N) : M = N :=
  by
  ext i j
  simp_rw [single_one_vecMul] at h
  exact congrFun (h i) j

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