Theorem exists_floor'

Modification history

2026-06-03 13:03
Mathlib/Algebra/Order/Floor/Defs.lean
feat(Algebra/Order/Floor/Defs): `Nat.cast` is strictly monotone in `FloorSemiring` and `FloorRing` (#37714) …
Modified exists_floor'View on Github →
2026-01-29 14:55
Mathlib/Algebra/Order/Floor/Defs.lean
feat: ring where elements are bounded by naturals is a floor ring (#34560) …
Added exists_floor'View on Github →