Documentation

Mathlib.Algebra.Order.Nonneg.Floor

Nonnegative elements are archimedean #

This file defines instances and prove some properties about the nonnegative elements {x : α // 0 ≤ x} of an arbitrary type α.

This is used to derive algebraic structures on ℝ≥0 and ℚ≥0 automatically.

Main declarations #

Equations
theorem Nonneg.nat_floor_coe {α : Type u_1} [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 r }) :
theorem Nonneg.nat_ceil_coe {α : Type u_1} [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 r }) :