mathlib
ce17b657 - feat(topology/algebra/monoid): to_additivize some lemmas (#11310)

Commit
4 years ago
feat(topology/algebra/monoid): to_additivize some lemmas (#11310) Uncomment a commented out to additive line that looks like its been there for 3 years (since https://github.com/leanprover-community/mathlib/commit/581cf19bf1885ef874c39c9902a93f579bc8c22d) The changes to to_additive in the past few years now make the generated lemma useful. Also to_additivize a bunch of other lemmas in this file.
Author
Parents
Loading