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 : α
- min : α → α → α
- max : α → α → α
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- zero : α
- zero_le_one : 0 ≤ 1
0 ≤ 1
in any linearly ordered commutative monoid.
Instances
A linearly ordered commutative group with a zero element.
- mul : α → α → α
- one : α
- min : α → α → α
- max : α → α → α
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- zero : α
- zero_le_one : 0 ≤ 1
- inv : α → α
- div : α → α → α
- zpow_succ' (n : ℕ) (a : α) : LinearOrderedCommGroupWithZero.zpow (↑n.succ) a = LinearOrderedCommGroupWithZero.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : α) : LinearOrderedCommGroupWithZero.zpow (Int.negSucc n) a = (LinearOrderedCommGroupWithZero.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
Instances
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
- instLinearOrderedAddCommMonoidWithTopOrderDualAdditive = LinearOrderedAddCommMonoidWithTop.mk ⋯
Equiv.mulLeft₀
as an OrderIso
on a LinearOrderedCommGroupWithZero.
.
Equations
- OrderIso.mulLeft₀' ha = OrderIso.mulLeft₀ a ⋯
Instances For
Equiv.mulRight₀
as an OrderIso
on a LinearOrderedCommGroupWithZero.
.
Equations
Instances For
Equations
- instLinearOrderedAddCommGroupWithTopAdditiveOrderDual = LinearOrderedAddCommGroupWithTop.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- instLinearOrderedAddCommGroupWithTopOrderDualAdditive = LinearOrderedAddCommGroupWithTop.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual = LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯
Equations
- instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop = LinearOrderedCommGroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- WithZero.partialOrder = WithBot.partialOrder
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 "ℤₘ₀")