Commit 2021-04-14 18:40 f444128f

chore(algebra/direct_sum_graded): golf proofs (#7029) Simplify the proofs of mul_assoc and mul_comm, and speed up all the proofs that were slow. Total elaboration time for this file is reduced from 12.9s to 1.7s (on my machine), and total CPU time is reduced from 19.8s to 6.8s. All the remaining elaboration times are under 200ms. The main idea is to explicitly construct bundled homomorphisms corresponding to λ a b c, a * b * c and λ a b c, a * (b * c) respectively. Then in proving the equality between those, we can unpack all the arguments immediately, and the remaining rewrites needed become simpler.