Theorem FloorRing.intCast_strictMono

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) …

Added FloorRing.intCast_strictMono View on Github →