Theorems · Inductive type · order theory
FloorRing
(α : Type u_4) → [Ring α] → [LinearOrder α] → Type u_4
A FloorRing is a linear ordered ring over α with a function
floor : α → ℤ satisfying ∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a).
- Defined in
- Mathlib.Algebra.Order.Floor.Defs
- Cited by
- 405 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- RingLinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement · cited by 8,572
- Ringstatement · cited by 7,463
Cited by434
Results whose statement or proof uses this declaration.
- Int.floorstatement and proof · cited by 225
- Int.ceilstatement and proof · cited by 138
- Int.fractstatement and proof · cited by 114
- GenContFract.ofstatement and proof · cited by 53
- roundstatement and proof · cited by 49
- GenContFract.IntFractPair.streamstatement and proof · cited by 37
- Module.Basis.ofZLatticeBasisstatement and proof · cited by 36
- Int.floor_lestatement and proof · cited by 30
- Int.le_floorstatement and proof · cited by 22
- GenContFract.IntFractPair.ofstatement and proof · cited by 22
- Int.fract_lt_onestatement and proof · cited by 20
- Int.ceil_lestatement and proof · cited by 17
Showing the 200 most cited of 434.