vecMul_injective_of_isUnit — Mathlib

English

Similarly, for matrices over a semiring, if A is a unit, then the right action by vecMul is injective: v ↦ v A is injective.

Русский

Аналогично: если A единичная, то правая операция vecMul на векторе по матрице инъективна: v ↦ v A.

LaTeX

$$IsUnit A → Function.Injective (v ↦ v A)$$

Lean4

theorem vecMul_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) :
    Function.Injective A.vecMul :=
  isRightRegular_iff_vecMul_injective.1 ha.isRegular.right

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