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`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
