Theorem FloorSemiring.natCast_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 FloorSemiring.natCast_strictMono View on Github →