Commit 2023-04-28 03:54 499a196e

View on Github →

feat: port LinearAlgebra.Matrix.ToLin (#3552)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Created Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Algebra.leftMulMatrix_apply

added theorem Algebra.leftMulMatrix_eq_repr_mul

added theorem Algebra.leftMulMatrix_injective

added theorem Algebra.leftMulMatrix_mulVec_repr

added theorem Algebra.smul_leftMulMatrix

added theorem Algebra.smul_leftMulMatrix_algebraMap

added theorem Algebra.smul_leftMulMatrix_algebraMap_eq

added theorem Algebra.smul_leftMulMatrix_algebraMap_ne

added theorem Algebra.toMatrix_lmul'

added theorem Algebra.toMatrix_lmul_eq

added theorem Algebra.toMatrix_lsmul

added def LinearEquiv.algConj

added def LinearMap.toMatrix'

added theorem LinearMap.toMatrix'_algebraMap

added theorem LinearMap.toMatrix'_apply

added theorem LinearMap.toMatrix'_comp

added theorem LinearMap.toMatrix'_id

added theorem LinearMap.toMatrix'_mul

added theorem LinearMap.toMatrix'_symm

added theorem LinearMap.toMatrix'_toLin'

added def LinearMap.toMatrix

added def LinearMap.toMatrixAlgEquiv'

added theorem LinearMap.toMatrixAlgEquiv'_apply

added theorem LinearMap.toMatrixAlgEquiv'_comp

added theorem LinearMap.toMatrixAlgEquiv'_id

added theorem LinearMap.toMatrixAlgEquiv'_mul

added theorem LinearMap.toMatrixAlgEquiv'_symm

added theorem LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv'

added def LinearMap.toMatrixAlgEquiv

added theorem LinearMap.toMatrixAlgEquiv_apply'

added theorem LinearMap.toMatrixAlgEquiv_apply

added theorem LinearMap.toMatrixAlgEquiv_comp

added theorem LinearMap.toMatrixAlgEquiv_id

added theorem LinearMap.toMatrixAlgEquiv_mul

added theorem LinearMap.toMatrixAlgEquiv_reindexRange

added theorem LinearMap.toMatrixAlgEquiv_symm

added theorem LinearMap.toMatrixAlgEquiv_toLinAlgEquiv

added theorem LinearMap.toMatrixAlgEquiv_transpose_apply'

added theorem LinearMap.toMatrixAlgEquiv_transpose_apply

added def LinearMap.toMatrixRight'

added theorem LinearMap.toMatrix_algebraMap

added theorem LinearMap.toMatrix_apply'

added theorem LinearMap.toMatrix_apply

added theorem LinearMap.toMatrix_basis_equiv

added theorem LinearMap.toMatrix_comp

added theorem LinearMap.toMatrix_eq_toMatrix'

added theorem LinearMap.toMatrix_id

added theorem LinearMap.toMatrix_mul

added theorem LinearMap.toMatrix_mulVec_repr

added theorem LinearMap.toMatrix_one

added theorem LinearMap.toMatrix_reindexRange

added theorem LinearMap.toMatrix_symm

added theorem LinearMap.toMatrix_toLin

added theorem LinearMap.toMatrix_transpose_apply'

added theorem LinearMap.toMatrix_transpose_apply

added theorem Matrix.ker_mulVecLin_eq_bot_iff

added theorem Matrix.ker_toLin'_eq_bot_iff

added def Matrix.mulVecLin

added theorem Matrix.mulVecLin_add

added theorem Matrix.mulVecLin_apply

added theorem Matrix.mulVecLin_mul

added theorem Matrix.mulVecLin_one

added theorem Matrix.mulVecLin_reindex

added theorem Matrix.mulVecLin_submatrix

added theorem Matrix.mulVecLin_zero

added theorem Matrix.mulVec_stdBasis

added theorem Matrix.mulVec_stdBasis_apply

added theorem Matrix.range_mulVecLin

added theorem Matrix.range_toLin'

added def Matrix.toLin'

added def Matrix.toLin'OfInv

added theorem Matrix.toLin'_apply'

added theorem Matrix.toLin'_apply

added theorem Matrix.toLin'_mul

added theorem Matrix.toLin'_mul_apply

added theorem Matrix.toLin'_one

added theorem Matrix.toLin'_reindex

added theorem Matrix.toLin'_submatrix

added theorem Matrix.toLin'_symm

added theorem Matrix.toLin'_toMatrix'

added def Matrix.toLin

added def Matrix.toLinAlgEquiv'

added theorem Matrix.toLinAlgEquiv'_apply

added theorem Matrix.toLinAlgEquiv'_mul

added theorem Matrix.toLinAlgEquiv'_one

added theorem Matrix.toLinAlgEquiv'_symm

added theorem Matrix.toLinAlgEquiv'_toMatrixAlgEquiv'

added def Matrix.toLinAlgEquiv

added theorem Matrix.toLinAlgEquiv_apply

added theorem Matrix.toLinAlgEquiv_mul

added theorem Matrix.toLinAlgEquiv_one

added theorem Matrix.toLinAlgEquiv_self

added theorem Matrix.toLinAlgEquiv_symm

added theorem Matrix.toLinAlgEquiv_toMatrixAlgEquiv

added def Matrix.toLinOfInv

added theorem Matrix.toLin_apply

added theorem Matrix.toLin_eq_toLin'

added theorem Matrix.toLin_finTwoProd

added theorem Matrix.toLin_finTwoProd_apply

added theorem Matrix.toLin_mul

added theorem Matrix.toLin_mul_apply

added theorem Matrix.toLin_one

added theorem Matrix.toLin_self

added theorem Matrix.toLin_symm

added theorem Matrix.toLin_toMatrix

added def Matrix.toLinearEquivRight'OfInv

added theorem Matrix.toLinearMapRight'_apply

added theorem Matrix.toLinearMapRight'_mul

added theorem Matrix.toLinearMapRight'_mul_apply

added theorem Matrix.toLinearMapRight'_one

added def Matrix.vecMulLinear

added theorem Matrix.vecMul_stdBasis

added def algEquivMatrix'

added def algEquivMatrix

added theorem toMatrix_distrib_mul_action_toLinearMap