Commit 2023-05-19 05:32 2d3cfc54

View on Github →

feat: port RingTheory.MatrixAlgebra (#4063)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MatrixAlgebra.lean

added def MatrixEquivTensor.equiv

added def MatrixEquivTensor.invFun

added theorem MatrixEquivTensor.invFun_add

added theorem MatrixEquivTensor.invFun_algebraMap

added theorem MatrixEquivTensor.invFun_smul

added theorem MatrixEquivTensor.invFun_zero

added theorem MatrixEquivTensor.left_inv

added theorem MatrixEquivTensor.right_inv

added def MatrixEquivTensor.toFunAlgHom

added theorem MatrixEquivTensor.toFunAlgHom_apply

added def MatrixEquivTensor.toFunBilinear

added theorem MatrixEquivTensor.toFunBilinear_apply

added def MatrixEquivTensor.toFunLinear

added def matrixEquivTensor

added theorem matrixEquivTensor_apply

added theorem matrixEquivTensor_apply_std_basis

added theorem matrixEquivTensor_apply_symm