Commit 2026-10-10 12:26 993089ff

View on Github →

feat(Algebra/Order/Floor): weaken assumptions on theorems about FloorRing (#37964) This PR weakens as much assumptions as possible on theorems about FloorSemiring and FloorRing. Mainly, IsOrderedRing and IsStrictOrderedRing are weakened to just IsOrderedAddMonoid or removed completely from the assumptions on the theorems. Most theorems can be generalized as is or only requires a minor modification of replacing lemmas about casting naturals/integers preserving order (the likes of Nat.cast_le, Int.cast_lt, etc.) with the corresponding version for FloorRing. Some other lemmas require modification in the proofs, but these changes shorten the proofs. The new proof of the theorem Int.mul_cast_floor_div_cancel_of_pos requires an extra import. The assumption IsOrderedAddMonoid is required on lemmas that involve comparison + addition, and IsOrderedRing is required only on lemmas that involve comparison + multiplication of two non-integer elements.

Estimated changes

modified def FloorRing.ofCeil
modified def FloorRing.ofFloor
modified theorem Int.fract_eq_self
modified theorem Int.fract_eq_zero_iff
modified theorem Nat.ceil_intCast
modified theorem Nat.floor_add_natCast
modified theorem Nat.floor_congr
modified theorem Nat.floor_sub_natCast
modified theorem Nat.floor_sub_ofNat
modified theorem Nat.floor_sub_one
modified theorem Nat.map_floor
modified theorem Rat.isInt_intCeil
modified theorem Rat.isInt_intFloor
modified theorem Rat.isInt_round
modified theorem Rat.isNat_intCeil
modified theorem Rat.isNat_intFloor
modified theorem Rat.isNat_round
modified theorem Measurable.fract
modified theorem Measurable.nat_floor
modified theorem MeasurableSet.image_fract
modified theorem Nat.measurable_floor
modified theorem measurable_fract
modified theorem Nat.cast_mem_Ioc_iff'
modified theorem Nat.cast_mem_Ioc_iff