vecMul_surjective_of_invertible — Mathlib

English

For vecMul, surjectivity is equivalent to the existence of a right inverse for A.

Русский

Для vecMul существование правого обратного эквивалентно существованию правого обратного для A.

LaTeX

$$Surjective (A.vecMul) ↔ ∃ B, A * B = 1$$

Lean4

theorem vecMul_surjective_of_invertible (A : Matrix m m R) [Invertible A] : Function.Surjective A.vecMul :=
  vecMul_surjective_iff_isUnit.2 <| isUnit_of_invertible A

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