mathlib
1aee8a8d - chore(*): Put `simp` attribute before `to_additive` (#11488)

Commit
3 years ago
chore(*): Put `simp` attribute before `to_additive` (#11488) A few lemmas were tagged in the wrong order. As tags are applied from left to right, `@[to_additive, simp]` only marks the multiplicative lemma as `simp`. The correct order is thus `@[simp, to_additive]`.
Author
Parents
Loading