Def FloorRing.ofFloor
Modification history
2026-10-10 12:26
Mathlib/Algebra/Order/Floor/Defs.lean
feat(Algebra/Order/Floor): weaken assumptions on theorems about `FloorRing` (#37964) …
Modified FloorRing.ofFloorView on Github →2026-04-06 13:59
Mathlib/Algebra/Order/Floor/Defs.lean
feat: weaken assumptions on lemmas about `FloorRing` (#37582) …
Modified FloorRing.ofFloorView on Github →2025-04-09 10:22
Mathlib/Algebra/Order/Floor/Defs.lean
chore: use mixin ordered algebraic typeclasses (part 2) (#20595)
Modified FloorRing.ofFloorView on Github →