Commit 2025-12-30 23:17 47ede36f

View on Github →

feat: a few Int.floor/Int.fract lemmas (#33408) From sphere-eversion.

Estimated changes

added theorem Int.floor_lt_self_iff
added theorem Int.fract_eq_zero_iff
added theorem Int.fract_ne_zero_iff