isRightRegular_iff_vecMul_injective

English

For a square matrix A, A is right regular if and only if the map v ↦ A.vecMul is injective.

Русский

Для квадратной матрицы A правая регулярность эквивалентна тому, что отображение v ↦ A.vecMul инъективно.

LaTeX

$$IsRightRegular(A) ⇔ Injective( v ↦ v A )$$

Lean4

theorem isRightRegular_iff_vecMul_injective [Fintype m] {A : Matrix m m α} :
    IsRightRegular A ↔ Function.Injective A.vecMul :=
  by
  cases isEmpty_or_nonempty m
  · simp [IsRightRegular, Function.injective_of_subsingleton]
  exact mul_left_injective_iff_vecMul_injective

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