-
Notifications
You must be signed in to change notification settings - Fork 297
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
feat(order/bounded_lattice): with_top.cases #3135
Conversation
Adding the case of integers.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've changed the title of the PR to follow the style guide
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
@@ -730,6 +730,35 @@ lemma lt_iff_exists_coe_btwn [partial_order α] [densely_ordered α] [no_top_ord | |||
⟨λ h, let ⟨y, hy⟩ := dense h, ⟨x, hx⟩ := (lt_iff_exists_coe _ _).1 hy.2 in ⟨x, hx.1 ▸ hy⟩, | |||
λ ⟨x, hx⟩, lt_trans hx.1 hx.2⟩ | |||
|
|||
/-- Lemma shows that a in with_top Z is either the maximal element or some integer n. -/ | |||
lemma with_top.cases (a : with_top ℤ) : a = ⊤ ∨ ∃ n : ℤ, a = n := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is true for any with_top α
. And I would prefer to have with_top.cases_on
with the same signature as option.cases_on
but using coercion and top
instead of some
and none
(with proof := option.cases_on a
).
end | ||
|
||
/-- Shows that for a in with_top, a+a = 0 is equivalent to a=0. -/ | ||
lemma (a : with_top ℤ) : a + a = 0 ↔ a = 0 := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should have instance with_top.char_zero
, instance with_top.mul_zero_class
, and instance with_top.no_zero_divisors
instead. Then one can use add_self_eq_zero
directly. Two out of three are now in #3157
I've PRed an instance that implies this lemma, closing the PR. Thank you for pointing at a hole in the library! |
Motivated by #3135. * Use `R` as a `Type*` variable; * Add `add_monoid_hom.map_nat_cast` and `with_top.coe_add_hom`; * Drop versions of `char_zero_of_inj_zero`, use `[add_left_cancel_monoid R]` instead.
Sorry about that, I completely forgot about it. Thank you for completing it! |
Adding the case of integers.