Theorem Int.fract_add_eq_add_sub_one_iff

Modification history

2026-10-17 13:25
Mathlib/Algebra/Order/Floor/Ring.lean
feat(Algebra/Order/Floor): floor-of-sum dichotomy via fractional parts (#41861) …
Added Int.fract_add_eq_add_sub_one_iffView on Github →