range_toLin_eq_top — Mathlib

English

If A has nonzero determinant, the range of toLin(b,b,A) is the whole module, i.e., surjective.

Русский

Если det(A) ≠ 0, образ toLin(b,b,A) равен всему модулю, т.е. отображение сюръективно.

LaTeX

$$$\\operatorname{range}(\\operatorname{toLin}(b,b,A)) = \\top$$$

Lean4

theorem range_toLin_eq_top [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) : LinearMap.range (toLin b b A) = ⊤ :=
  range_eq_top.mpr (toLinearEquiv b A hA).surjective

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