Commit 2023-11-05 21:55 ce4b7e4c

View on Github →

feat(Data/Matrix/Basic): add missing lemmas about natCast and intCast (#8088)

feat(Data/Matrix/Basic): add missing lemmas about natCast and intCast This also gives the intCast instance a nicer defeq. This remains unopinionated about which side of diagonal 37 = 37 is the simp-normal form.
lintfix

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.diagonal_intCast'

added theorem Matrix.diagonal_intCast

added theorem Matrix.diagonal_natCast'

added theorem Matrix.diagonal_natCast

modified theorem Matrix.diagonal_neg

added theorem Matrix.diagonal_ofNat'

added theorem Matrix.diagonal_ofNat

added theorem Matrix.diagonal_sub