Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-01-19 11:40
c37c64fb
View on Github →
chore(data/matrix/notation): Add some missing simp lemmas for sub, head, and tail (
#5807
)
Estimated changes
Modified
src/data/matrix/notation.lean
added
theorem
matrix.cons_sub
added
theorem
matrix.empty_sub_empty
added
theorem
matrix.head_add
added
theorem
matrix.head_neg
added
theorem
matrix.head_sub
added
theorem
matrix.sub_cons
added
theorem
matrix.tail_add
added
theorem
matrix.tail_neg
added
theorem
matrix.tail_sub
Modified
test/matrix.lean