English
For a matrix A over a field, the rank of A equals the finite rank of the subspace spanned by its row set.
Русский
Для матрицы A над полем ранг A равен конечному рангу подпространства, порождённого множеством её строк.
LaTeX
$$$ A.\mathrm{rank} = \mathrm{finrank}_{R}\left( \mathrm{span}_{R}(\mathrm{Set.range}(A.row)) \right). $$$
Lean4
/-- For square matrices with coefficients in an algebra over a commutative semiring, the natural
map that reindexes a matrix's rows and columns with equivalent types,
`Matrix.reindex`, is an equivalence of algebras. -/
def reindexAlgEquiv (e : m ≃ n) : Matrix m m A ≃ₐ[R] Matrix n n A :=
{ reindexLinearEquiv A A e e with
toFun := reindex e e
map_mul' := fun a b => (reindexLinearEquiv_mul A A e e e a b).symm
commutes' := fun r => by simp [algebraMap, Algebra.algebraMap] }
