Canonically ordered semifields #
- toMin : Min α
- toMax : Max α
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1The minimum function is equivalent to the one you get from
minOfLe
.The minimum function is equivalent to the one you get from
maxOfLe
.- toInv : Inv α
- toDiv : Div α
a / b := a * b⁻¹⁻¹
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹
(n
times)zpow : ℤ → α → αa ^ 0 = 1
a ^ (n + 1) = a * a ^ n
a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
A canonically linear ordered field is a linear ordered field in which a ≤ b≤ b
iff there exists
c
with b = a + c
.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.