English
The rank of A equals the finrank over R of the span of its columns.
Русский
Ранг A равен конечной размерности пространства, порождаемого its столбцами.
LaTeX
$$$\operatorname{rank}(A) = \operatorname{finrank}_R\bigl( \operatorname{span}_R(\operatorname{range}(A.col)) \bigr)$$$
Lean4
theorem rank_eq_finrank_range_toLin [Finite m] [DecidableEq n] {M₁ M₂ : Type*} [AddCommGroup M₁] [AddCommGroup M₂]
[Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁) (v₂ : Basis n R M₂) :
A.rank = finrank R (LinearMap.range (toLin v₂ v₁ A)) :=
by
cases nonempty_fintype m
let e₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl _)
let e₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl _)
have range_e₂ : LinearMap.range e₂ = ⊤ := by
rw [LinearMap.range_eq_top]
exact e₂.surjective
refine LinearEquiv.finrank_eq (e₁.ofSubmodules _ _ ?_)
rw [← LinearMap.range_comp, ← LinearMap.range_comp_of_range_eq_top (toLin v₂ v₁ A) range_e₂]
congr 1
apply LinearMap.pi_ext'
rintro i
apply LinearMap.ext_ring
have aux₁ := toLin_self (Pi.basisFun R n) (Pi.basisFun R m) A i
have aux₂ := Basis.equiv_apply (Pi.basisFun R n) i v₂
rw [toLin_eq_toLin', toLin'_apply'] at aux₁
rw [Pi.basisFun_apply] at aux₁ aux₂
simp only [e₁, e₂, LinearMap.comp_apply, LinearEquiv.coe_coe, Equiv.refl_apply, aux₁, aux₂, LinearMap.coe_single,
toLin_self, map_sum, LinearEquiv.map_smul, Basis.equiv_apply]
