Commit 2023-01-17 03:57 aae0a577

View on Github →

feat: port Data.Matrix.DMatrix (#1605)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/DMatrix.lean

added def AddMonoidHom.mapDMatrix

added theorem AddMonoidHom.mapDMatrix_apply

added theorem DMatrix.add_apply

added def DMatrix.col

added theorem DMatrix.ext

added theorem DMatrix.ext_iff

added def DMatrix.map

added theorem DMatrix.map_add

added theorem DMatrix.map_apply

added theorem DMatrix.map_map

added theorem DMatrix.map_sub

added theorem DMatrix.map_zero

added theorem DMatrix.neg_apply

added def DMatrix.row

added theorem DMatrix.sub_apply

added def DMatrix.transpose

added theorem DMatrix.zero_apply

added def DMatrix