Structures · Algebra
FloorSemiring
A FloorSemiring is an ordered semiring over α with a function
floor : α → ℕ satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x).
Note that many lemmas require a LinearOrder. Please see the above TODO.
- Defined in
- Mathlib.Algebra.Order.Floor.Defs
- Shape
- One type argument · adds floor, ceil, floor_of_neg, gc_floor, gc_ceil
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Nat
- NNReal
- NNRat
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by189
- Nat.floor
- Nat.ceil
- Nat.le_ceil
- Int.log
- Nat.le_floor_iff
- Int.clog
- Nat.floor_le
- Nat.floor_natCast
- Nat.lt_floor_add_one
- Nat.ceil_le
- Nat.le_floor
- Nat.ceil_lt_add_one
- Nat.lt_ceil
- Nat.floor_lt
- Nat.floor_of_nonpos
- Int.log_of_right_le_one
- Int.log_of_one_le_right
- Nat.floor_mono
- Nat.le_floor_iff'
- Nat.floor_zero
- Nat.ceil_eq_zero
- tendsto_nat_floor_atTop
- Nat.floor_one
- Nat.ceil_natCast
- Nat.floor_eq_zero
- Nat.ceil_one
- Nat.sub_one_lt_floor
- Int.neg_log_inv_eq_clog
- Nat.floor_eq_iff
- Nat.floor_add_natCast
- FloorSemiring.floor
- tendsto_smul_comp_nat_floor_of_tendsto_mul
- Nat.ceil_add_natCast
- Nat.ceil_pos
- Nat.ceil_sub_natCast
- Int.clog_of_right_le_zero
- Nat.one_le_floor_iff
- Nat.lt_of_floor_lt
- Mathlib.Meta.Positivity.nat_ceil_pos
- Int.clog_of_one_le_right
- Int.log_of_right_le_zero
- Nat.ceil_mono
- Int.log_natCast
- Nat.ceil_le_floor_add_one
- FloorSemiring.gc_ceil
- Nat.ceil_zero
- Nat.floor_lt'
- Nat.floor_pos
- Nat.ceil_eq_iff
- Nat.floor_le_floor
Ancestors0
No ancestors.