Commit 2022-01-09 07:58 ad4ea538
View on Github →chore(*): miscellaneous to_additive related cleanup (#11316) A few cleanup changes related to to_additive:
- After https://github.com/leanprover-community/lean/pull/618 was merged, we no longer need to add namespaces manually in filtered_colimits and open subgroup
- to_additive can now generate some more lemmas in big_operators/fin
- to_additive now handles a proof in measure/haar better than it used to so remove a workaround there