mathlib
b566cd5a - chore(*): fix some to_additive orders (#17297)

Commit

3 years ago

chore(*): fix some to_additive orders (#17297) To additive should come after simp and other attributes where possible

Author

alexjbest

Parents