Linearly ordered commutative groups and monoids with a zero element adjoined #
This file sets up a special class of linearly ordered commutative monoids that show up as the target of so-called “valuations” in algebraic number theory.
Usually, in the informal literature, these objects are constructed by taking a linearly ordered commutative group Γ and formally adjoining a zero element: Γ ∪ {0}.
The disadvantage is that a type such as NNReal
is not of that form,
whereas it is a very common target for valuations.
The solutions is to use a typeclass, and that is exactly what we do in this file.
A linearly ordered commutative monoid with a zero element.
- mul : α → α → α
- one : α
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
- compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
- zero : α
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
- zero_le_one : 0 ≤ 1
0 ≤ 1
in any linearly ordered commutative monoid.
Instances
0 ≤ 1
in any linearly ordered commutative monoid.
A linearly ordered commutative group with a zero element.
- mul : α → α → α
- one : α
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
- compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
- zero : α
- zero_le_one : 0 ≤ 1
- inv : α → α
- div : α → α → α
a / b := a * b⁻¹
- zpow : ℤ → α → α
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : α), LinearOrderedCommGroupWithZero.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedCommGroupWithZero.zpow (Int.ofNat n.succ) a = LinearOrderedCommGroupWithZero.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedCommGroupWithZero.zpow (Int.negSucc n) a = (LinearOrderedCommGroupWithZero.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Pullback a LinearOrderedCommMonoidWithZero
under an injective map.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual = let __src := Additive.orderedAddCommMonoid; let __src_1 := Additive.linearOrder; LinearOrderedAddCommMonoidWithTop.mk ⋯
Alias of mul_le_one'
for unification.
Alias of one_le_mul'
for unification.
Equiv.mulLeft₀
as an OrderIso
on a LinearOrderedCommGroupWithZero.
.
Note that OrderIso.mulLeft₀
refers to the LinearOrderedField
version.
Equations
- OrderIso.mulLeft₀' ha = let __src := Equiv.mulLeft₀ a ha; { toEquiv := __src, map_rel_iff' := ⋯ }
Instances For
Equiv.mulRight₀
as an OrderIso
on a LinearOrderedCommGroupWithZero.
.
Note that OrderIso.mulRight₀
refers to the LinearOrderedField
version.
Equations
- OrderIso.mulRight₀' ha = let __src := Equiv.mulRight₀ a ha; { toEquiv := __src, map_rel_iff' := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Alias of pow_lt_pow_right₀
.
Equations
- instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual = let __src := Multiplicative.orderedCommMonoid; let __src_1 := Multiplicative.linearOrder; LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- WithZero.partialOrder = WithBot.partialOrder
Equations
- ⋯ = ⋯
Equations
- WithZero.linearOrder = WithBot.linearOrder
Equations
- WithZero.orderedCommMonoid = let __src := CommMonoidWithZero.toCommMonoid; let __src_1 := WithZero.partialOrder; OrderedCommMonoid.mk ⋯
If 0
is the least element in α
, then WithZero α
is an OrderedAddCommMonoid
.
Equations
- WithZero.orderedAddCommMonoid zero_le = let __src := WithZero.partialOrder; let __src_1 := WithZero.addCommMonoid; OrderedAddCommMonoid.mk ⋯
Instances For
Adding a new zero to a canonically ordered additive monoid produces another one.
Equations
- WithZero.canonicallyOrderedAddCommMonoid = let __src := WithZero.orderBot; let __src_1 := WithZero.orderedAddCommMonoid ⋯; let __src_2 := ⋯; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- WithZero.instLinearOrderedCommMonoidWithZero = let __src := WithZero.linearOrder; let __src_1 := WithZero.commMonoidWithZero; LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.