mathlib documentation


Nonnegative elements are archimedean #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[protected, instance]
@[protected, instance]
theorem nonneg.nat_floor_coe {α : Type u_1} [ordered_semiring α] [floor_semiring α] (a : {r // 0 r}) :
theorem nonneg.nat_ceil_coe {α : Type u_1} [ordered_semiring α] [floor_semiring α] (a : {r // 0 r}) :