ext_of_mulVec_single — Mathlib

English

If two matrices have the same action on all standard basis vectors (Pi.single i 1), then the matrices are equal.

Русский

Если две матрицы действуют одинаково на все базисные векторы, то они равны.

LaTeX

$$If ∀ i, M ·ᵥ e_i = N ·ᵥ e_i then M = N, where e_i = Pi.single i 1.$$

Lean4

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

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