-
Notifications
You must be signed in to change notification settings - Fork 299
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
abs_diff_lt_one_of_floor_eq_floor #693
Conversation
@@ -5,7 +5,7 @@ Authors: Mario Carneiro | |||
|
|||
Archimedean groups and fields. | |||
-/ | |||
import algebra.group_power data.rat | |||
import algebra.group_power data.rat tactic.linarith | |||
|
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.
So I did not want to change the import graph when I was writing the theory of fractional parts a few days ago, because I was scared that linarith, or something it imported, might use this stuff, and I didn't really know how to check that it didn't.
This PR might conflict with mine, but only in a trivial way -- I think we might both have written new functions in about the same place.
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.
To check that the import did not break anything, I did the import, saved the file, and then I compiled the library. It went fine.
@@ -67,6 +67,17 @@ eq_of_forall_le_iff $ λ a, by rw [le_floor, | |||
theorem floor_sub_int (x : α) (z : ℤ) : ⌊x - z⌋ = ⌊x⌋ - z := | |||
eq.trans (by rw [int.cast_neg]; refl) (floor_add_int _ _) | |||
|
|||
lemma abs_diff_lt_one_of_floor_eq_floor {α : Type*} [decidable_linear_ordered_comm_ring α] [floor_ring α] | |||
{x y : α} (h : floor x = floor y) : abs (x - y) < 1 := |
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.
Should be called abs_sub_lt_one_of_floor_eq_floor
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.
Indeed, thanks.
* abs_diff_lt_one_of_floor_eq_floor * better name
No description provided.