Commit 2021-05-01 06:41 e3de4e30
View on Github →fix(algebra/direct_sum_graded): replace badly-stated and slow simps lemmas with manual ones (#7403)
Zulip. The simps mul attribute on direct_sum.ghas_mul.of_add_subgroups was taking 44s, only to produce a lemma that wasn't very useful anyway.