Theorem FloorSemiring.natCast_lt_iff

Modification history

2026-10-10 12:26
Mathlib/Algebra/Order/Floor/Defs.lean
feat(Algebra/Order/Floor): weaken assumptions on theorems about `FloorRing` (#37964) …
Added FloorSemiring.natCast_lt_iffView on Github →