Theorems · Inductive type · order theory

FloorSemiring

(α : Type u_4) → [Semiring α] → [PartialOrder α] → Type u_4

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

Cited by

179 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

SemiringPartialOrder