mulVec_surjective_iff_isUnit — Mathlib

English

For any A, surjectivity of mulVec is equivalent to A being a unit.

Русский

Для любой матрицы A сюрьективность умножения слева эквивалентна тому, что A является единицей.

LaTeX

$$Surjective A.mulVec ↔ IsUnit A$$

Lean4

theorem mulVec_surjective_iff_isUnit {A : Matrix m m R} : Function.Surjective A.mulVec ↔ IsUnit A := by
  rw [mulVec_surjective_iff_exists_right_inverse, exists_right_inverse_iff_isUnit]

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