Commit 2024-10-25 13:43 a1cf0e3b

View on Github →

feat: Matrices over finite free modules are finite modules (#18098) The titular result is trivial, but to state the lemmas about the basis this uses, we need to generalize many results about stdBasisMatrix.

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

modified theorem Matrix.matrix_eq_sum_stdBasisMatrix

modified theorem Matrix.mulVec_stdBasisMatrix

modified def Matrix.stdBasisMatrix

modified theorem Matrix.stdBasisMatrix_add

modified theorem Matrix.stdBasisMatrix_eq_single_vecMulVec_single

modified theorem Matrix.std_basis_eq_basis_mul_basis

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem rank_matrix_module'

added theorem rank_matrix_module

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/StdBasis.lean

added theorem Basis.matrix_apply

Modified Mathlib/RingTheory/MatrixAlgebra.lean