Mathlib Changelog
v4
Changelog
About
Github
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