isLeftRegular_iff_mulVec_injective

English

For A ∈ M(l m; α) with a nonempty index set, left multiplication B ↦ B A is injective if and only if the map v ↦ A.vecMul is injective.

Русский

Для A ∈ M(l×m; α) левого умножения B ↦ B A инъективно тогда и только тогда, когда vecMul A инъективно.

LaTeX

$$Injective( B ↦ B A ) iff Injective( v ↦ v A )$$

Lean4

theorem isLeftRegular_iff_mulVec_injective [Fintype m] {A : Matrix m m α} :
    IsLeftRegular A ↔ Function.Injective A.mulVec :=
  by
  cases isEmpty_or_nonempty m
  · simp [IsLeftRegular, Function.injective_of_subsingleton]
  exact mul_right_injective_iff_mulVec_injective

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