Commit 2020-06-09 05:24 24ce416a

View on Github →

chore(data/matrix/basic): clean up of new lemmas on matrix numerals (#2996) Generalise and improve use of @[simp] for some newly added lemmas about matrix numerals.

Estimated changes

Modified src/data/matrix/basic.lean

deleted theorem matrix.bit0_apply_apply

added theorem matrix.bit0_val

deleted theorem matrix.bit1_apply_apply

added theorem matrix.bit1_val

added theorem matrix.bit1_val_eq

added theorem matrix.bit1_val_ne