Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-10 14:25 c25122bb

View on Github →

feat(algebra/archimedean): add fractional parts of floor_rings (#709)

Estimated changes

added theorem floor_add_fract
added theorem floor_eq_iff
added theorem floor_fract
added def fract
added theorem fract_add
added theorem fract_add_floor
added theorem fract_coe
added theorem fract_eq_fract
added theorem fract_eq_iff
added theorem fract_floor
added theorem fract_fract
added theorem fract_lt_one
added theorem fract_mul_nat
added theorem fract_nonneg
added theorem fract_zero