Commit 2023-04-28 05:58 88894f5e

View on Github →

feat: port LinearAlgebra.Matrix.Basis (#3691)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.coord_unitsSMul

deleted theorem Basis.coord_unitsSmul

added def Basis.isUnitSMul

added theorem Basis.isUnitSMul_apply

deleted def Basis.isUnitSmul

deleted theorem Basis.isUnitSmul_apply

added theorem Basis.repr_unitsSMul

deleted theorem Basis.repr_unitsSmul

added def Basis.unitsSMul

added theorem Basis.unitsSMul_apply

deleted def Basis.unitsSmul

deleted theorem Basis.unitsSmul_apply

Created Mathlib/LinearAlgebra/Matrix/Basis.lean

added theorem Basis.coePiBasisFun.toMatrix_eq_transpose

added def Basis.invertibleToMatrix

added theorem Basis.sum_toMatrix_smul_self

added theorem Basis.toLin_toMatrix

added def Basis.toMatrix

added def Basis.toMatrixEquiv

added theorem Basis.toMatrix_apply

added theorem Basis.toMatrix_eq_toMatrix_constr

added theorem Basis.toMatrix_isUnitSMul

added theorem Basis.toMatrix_map

added theorem Basis.toMatrix_map_vecMul

added theorem Basis.toMatrix_mul_toMatrix

added theorem Basis.toMatrix_mul_toMatrix_flip

added theorem Basis.toMatrix_reindex'

added theorem Basis.toMatrix_reindex

added theorem Basis.toMatrix_self

added theorem Basis.toMatrix_transpose_apply

added theorem Basis.toMatrix_unitsSMul

added theorem Basis.toMatrix_update

added theorem LinearMap.toMatrix_id_eq_basis_toMatrix

added theorem basis_toMatrix_basisFun_mul

added theorem basis_toMatrix_mul

added theorem basis_toMatrix_mul_linearMap_toMatrix

added theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix

added theorem linearMap_toMatrix_mul_basis_toMatrix

added theorem mul_basis_toMatrix