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 (x1 x2 : α) => x1 ≤ x2
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- 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 (x1 x2 : α) => x1 ≤ x2
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- 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
- Function.Injective.linearOrderedCommMonoidWithZero f hf zero one mul npow hsup hinf = LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯
Instances For
Equations
- instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual = LinearOrderedAddCommMonoidWithTop.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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 = { toEquiv := Equiv.mulLeft₀ a ha, 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 = { toEquiv := Equiv.mulRight₀ a ha, map_rel_iff' := ⋯ }
Instances For
Equations
- instLinearOrderedAddCommGroupWithTopAdditiveOrderDual = LinearOrderedAddCommGroupWithTop.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯
Alias of pow_lt_pow_right₀
.
Equations
- instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual = LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯
Equations
- instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop = LinearOrderedCommGroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- WithZero.partialOrder = WithBot.partialOrder
Equations
- ⋯ = ⋯
Equations
- WithZero.linearOrder = WithBot.linearOrder
Equations
- WithZero.orderedCommMonoid = OrderedCommMonoid.mk ⋯
If 0
is the least element in α
, then WithZero α
is an OrderedAddCommMonoid
.
Equations
Instances For
Adding a new zero to a canonically ordered additive monoid produces another one.
Equations
- WithZero.canonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
Equations
- WithZero.canonicallyLinearOrderedAddCommMonoid = CanonicallyLinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
Equations
- WithZero.instLinearOrderedCommMonoidWithZero = LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯
Equations
- WithZero.instLinearOrderedCommGroupWithZero = LinearOrderedCommGroupWithZero.mk ⋯ CommGroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯
Notation for WithZero (Multiplicative ℕ)
Equations
- Multiplicative.termℕₘ₀ = Lean.ParserDescr.node `Multiplicative.termℕₘ₀ 1024 (Lean.ParserDescr.symbol "ℕₘ₀")
Instances For
Notation for WithZero (Multiplicative ℤ)
Equations
- Multiplicative.termℤₘ₀ = Lean.ParserDescr.node `Multiplicative.termℤₘ₀ 1024 (Lean.ParserDescr.symbol "ℤₘ₀")