Semifield structure on the type of nonnegative elements #
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 #
{x : α // 0 ≤ x}
is aCanonicallyLinearOrderedSemifield
ifα
is aLinearOrderedField
.
Equations
- Nonneg.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ⟨↑q, ⋯⟩ }
@[simp]
@[simp]