Commit 2021-01-20 11:50 9ae33174
View on Github →feat(data/fin): add_comm_monoid and simp lemmas (#5010)
Provide add_comm_monoid for fin (n + 1), which makes proofs that have to do with bit0, bit1, and nat.cast and related happy. Provide the specialized lemmas as simp lemmas. Also provide various simp lemmas about multiplication, but without the associated comm_monoid.