feat(algebra/order/floor): fract_one (#15785)

This seems to be an appropriate `simp` lemma, but is currently missing.
leanprover-community · Aug 1, 2022 · 7dcf5c3 · 7dcf5c3
1 parent 2f1b313
commit 7dcf5c3
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/algebra/order/floor.lean b/src/algebra/order/floor.lean
@@ -521,6 +521,9 @@ lemma fract_lt_one (a : α) : fract a < 1 := sub_lt.1 $ sub_one_lt_floor _
 
 @[simp] lemma fract_zero : fract (0 : α) = 0 := by rw [fract, floor_zero, cast_zero, sub_self]
 
+@[simp] lemma fract_one : fract (1 : α) = 0 :=
+by simp [fract]
+
 @[simp] lemma fract_coe (z : ℤ) : fract (z : α) = 0 :=
 by { unfold fract, rw floor_coe, exact sub_self _ }