mathlib
0bb42725 - chore(*): to_additive related cleanup (#11559)

Commit
3 years ago
chore(*): to_additive related cleanup (#11559) A few to_additive related cleanups * Move measurability before to_additive to avoid having to manually do it later (or forget). * Ensure anything tagged to_additive, mono has the additive version also mono'd * Move simp before to_additive
Author
Parents
Loading