mathlib

eb55b1e9 - chore(algebra/order/floor): generalize lemmas about adding nat from rings to semirings (#15952)

chore(algebra/order/floor): generalize lemmas about adding nat from rings to semirings (#15952) This generalizes this typeclass argument of the following lemmas: * `nat.floor_add_nat` * `nat.floor_add_one` * `nat.ceil_add_nat` * `nat.ceil_add_one` * `nat.floor_sub_nat` These generalizations are useful for `nnreal` and a future `nnrat`.