Structures · Algebra
FloorRing
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
- Shape
- One type argument · adds floor, ceil, gc_coe_floor, gc_ceil_coe
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Int
- Real
- Rat
- ArchimedeanClass.FiniteElement
How is a type an instance?
Loading the hierarchy index…
Assumed by424
- Int.floor
- Int.ceil
- Int.fract
- GenContFract.of
- round
- GenContFract.IntFractPair.stream
- Module.Basis.ofZLatticeBasis
- Int.floor_le
- Int.le_floor
- GenContFract.IntFractPair.of
- Int.fract_lt_one
- Int.ceil_le
- Int.fract_nonneg
- Int.floor_eq_iff
- Int.floor_intCast
- ZSpan.fract
- Int.le_ceil
- Int.lt_floor_add_one
- Module.Basis.ofZLatticeBasis_apply
- Int.ceil_intCast
- ZSpan.floor
- Rat.floor_cast
- Int.ceil_add_intCast
- Int.fract_intCast
- round_eq
- Int.ceil_eq_iff
- Int.floor_add_intCast
- GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
- Int.floor_lt
- Int.ceil_lt_add_one
- Int.floor_zero
- Int.fract_zero
- Module.Basis.ofZLatticeBasis_span
- Int.lt_ceil
- ZSpan.repr_fract_apply
- Int.sub_one_lt_floor
- GenContFract.IntFractPair.seq1
- Int.floor_mono
- ZSpan.fract_eq_self
- GenContFract.IntFractPair.stream_isSeq
- Int.floor_nonneg
- Int.ceil_mono
- ZLattice.rank
- GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none
- Module.Basis.ofZLatticeBasis_repr_apply
- Int.floor_add_fract
- GenContFract.of_partNum_eq_one
- GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one
- Int.fract_eq_iff
- GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some
Ancestors0
No ancestors.