Commit 2020-06-08 16:39 2caf479d
View on Github →feat(data/matrix/basic): add bit0, bit1 lemmas (#2987)
Based on a conversation in
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matrix.20equality.20by.20extensionality
we define simp lemmas for matrices represented by numerals.
This should result in better representation of scalar multiples of
one_val : matrix n n a.