Theorem Int.fract_eq_self

Modification history

2026-10-10 12:26
Mathlib/Algebra/Order/Floor/Ring.lean
feat(Algebra/Order/Floor): weaken assumptions on theorems about `FloorRing` (#37964) …
Modified Int.fract_eq_selfView on Github →
2025-04-13 02:25
Mathlib/Algebra/Order/Floor/Ring.lean
chore(*): rename ring type variables (#23939) …
Modified Int.fract_eq_selfView on Github →
2023-01-10 17:53
Mathlib/Algebra/Order/Floor.lean
feat: port `Algebra.Order.Floor` (#1304) …
Added Int.fract_eq_selfView on Github →