Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes