mulVec_injective_of_isUnit — Mathlib

English

Let M be a square matrix over a semiring with finite index m. If M is a unit (invertible), then the map v ↦ vecMul v M is injective.

Русский

Пусть M — квадратная матрица над полем с конечным размером. Если M является обратимой (единичный), то отображение v ↦ vecMul v M инъективно.

LaTeX

$$IsUnit M → Function.Injective (v ↦ vecMul v M)$$

Lean4

theorem mulVec_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) :
    Function.Injective A.mulVec :=
  isLeftRegular_iff_mulVec_injective.1 ha.isRegular.left

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