-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/ordered_monoid): add_eq_bot_iff #8474
Conversation
bot addition is saturating on the bottom. On the way, typeclass arguments were relaxed to just `[add_monoid α]`, and helper simp lemmas added for `bot`.
Should this be called |
I think the naming convention is that |
bors d+ |
✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
bot addition is saturating on the bottom. On the way, typeclass arguments were relaxed to just `[add_semigroup α]`, and helper simp lemmas added for `bot`. The iff lemma added (`add_eq_bot`) is not exactly according to the naming convention, but matches the top lemma and related ones in the naming style, so the style is kept consistent. There is an API proof available, but the defeq proof (using the top equivalent) was used based on suggestions.
Pull request successfully merged into master. Build succeeded: |
bot addition is saturating on the bottom. On the way, typeclass arguments were relaxed to just `[add_semigroup α]`, and helper simp lemmas added for `bot`. The iff lemma added (`add_eq_bot`) is not exactly according to the naming convention, but matches the top lemma and related ones in the naming style, so the style is kept consistent. There is an API proof available, but the defeq proof (using the top equivalent) was used based on suggestions.
bot addition is saturating on the bottom. On the way, typeclass arguments
were relaxed to just
[add_semigroup α]
, and helper simp lemmasadded for
bot
.The iff lemma added (
add_eq_bot
) is not exactly according to the naming convention, but matches the top lemma and related ones in the naming style, so the style is kept consistent.There is an API proof available, but the defeq proof (using the top equivalent) was used based on suggestions.