mulVec_surjective_of_invertible — Mathlib

English

Applying vecMul to vectors from m to n is surjective when vecMul is invertible.

Русский

Применение vecMul к векторам из m в n является сюрьективным, когда vecMul обратна.

LaTeX

$$Function.Surjective (\lambda v, v A) or VecMul surjective$$

Lean4

theorem mulVec_surjective_of_invertible (A : Matrix m m R) [Invertible A] : Function.Surjective A.mulVec :=
  mulVec_surjective_iff_isUnit.2 <| isUnit_of_invertible A

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