Commit 2023-06-14 10:32 1ac8d430
View on Github →chore(*): fix @[to_additive, simp] to the correct order (#19169)
Whilst making some files, I noticed that there is some lemmas that have the wrong order for to_additive and simp.
chore(*): fix @[to_additive, simp] to the correct order (#19169)
Whilst making some files, I noticed that there is some lemmas that have the wrong order for to_additive and simp.