-
Notifications
You must be signed in to change notification settings - Fork 259
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
Inequality functionality for norm_num
#1567
Comments
Thanks for opening this issue @thorimur, indeed this is very important functionality. I removed the Github link between this issue and #1568 because if they're linked then Github will "close" this issue when #1568 is merged, whereas we want the issue to stay open until the Edit: What goes around, comes around. It looks like the new version of #1568 will indeed knock off the whole issue. |
This PR gives `norm_num` basic inequality (and equality) functionality (towards #1567), including the following: ``` example {α} [DivisionRing α] [CharZero α] : (-1:α) ≠ 2 := by norm_num ``` We implement basic logical extensions to handle `=` and `≠` together, namely `¬`, `True`, and `False`. `≠` is not given an extension, as it is handled by `=` and `¬`. For now we only can prove `≠` for numbers given a `CharZero α` instance. - [x] depends on: #1578 Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Fixed in #1568 |
This is an issue for tracking inequality functionality needed in
norm_num
, including≤
,<
, and≠
.For
≠
, the following example should work:The text was updated successfully, but these errors were encountered: