Documentation

Mathlib.Algebra.Order.GroupWithZero.Canonical

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.

Instances

    A linearly ordered commutative group with a zero element.

    Instances
      @[reducible, inline]
      abbrev Function.Injective.linearOrderedCommMonoidWithZero {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {β : Type u_3} [Zero β] [Bot β] [One β] [Mul β] [Pow β ] [Max β] [Min β] (f : βα) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (hsup : ∀ (x y : β), f (xy) = max (f x) (f y)) (hinf : ∀ (x y : β), f (xy) = min (f x) (f y)) (bot : f = ) :

      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
        @[simp]
        theorem zero_le' {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} :
        0 a
        @[simp]
        theorem not_lt_zero' {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} :
        ¬a < 0
        @[simp]
        theorem le_zero_iff {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} :
        a 0 a = 0
        theorem zero_lt_iff {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} :
        0 < a a 0
        theorem ne_zero_of_lt {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a b : α} (h : b < a) :
        a 0

        See also bot_eq_zero and bot_eq_zero' for canonically ordered monoids.

        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.
        theorem pow_pos_iff {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} {n : } [NoZeroDivisors α] (hn : n 0) :
        0 < a ^ n 0 < a
        @[simp]
        theorem Units.zero_lt {α : Type u_1} [LinearOrderedCommGroupWithZero α] (u : αˣ) :
        0 < u
        theorem mul_inv_lt_of_lt_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a b c : α} (h : a < b * c) :
        a * c⁻¹ < b
        theorem inv_mul_lt_of_lt_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a b c : α} (h : a < b * c) :
        b⁻¹ * a < c
        theorem lt_of_mul_lt_mul_of_le₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a b c d : α} (h : a * b < c * d) (hc : 0 < c) (hh : c a) :
        b < d
        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.
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem WithZero.zero_le {α : Type u_1} [Preorder α] (a : WithZero α) :
        0 a
        @[simp]
        theorem WithZero.zero_lt_coe {α : Type u_1} [Preorder α] (a : α) :
        0 < a
        @[simp]
        theorem WithZero.not_coe_le_zero {α : Type u_1} [Preorder α] {a : α} :
        ¬a 0
        @[simp]
        theorem WithZero.not_lt_zero {α : Type u_1} [Preorder α] {x : WithZero α} :
        ¬x < 0
        theorem WithZero.zero_eq_bot {α : Type u_1} [Preorder α] :
        0 =
        @[simp]
        theorem WithZero.coe_lt_coe {α : Type u_1} [Preorder α] {a b : α} :
        a < b a < b
        @[simp]
        theorem WithZero.coe_le_coe {α : Type u_1} [Preorder α] {a b : α} :
        a b a b
        @[simp]
        theorem WithZero.one_lt_coe {α : Type u_1} [Preorder α] {a : α} [One α] :
        1 < a 1 < a
        @[simp]
        theorem WithZero.one_le_coe {α : Type u_1} [Preorder α] {a : α} [One α] :
        1 a 1 a
        @[simp]
        theorem WithZero.coe_lt_one {α : Type u_1} [Preorder α] {a : α} [One α] :
        a < 1 a < 1
        @[simp]
        theorem WithZero.coe_le_one {α : Type u_1} [Preorder α] {a : α} [One α] :
        a 1 a 1
        theorem WithZero.coe_le_iff {α : Type u_1} [Preorder α] {a : α} {x : WithZero α} :
        a x (b : α), x = b a b
        @[simp]
        theorem WithZero.unzero_le_unzero {α : Type u_1} [Preorder α] {a b : WithZero α} (ha : a 0) (hb : b 0) :
        unzero ha unzero hb a b
        theorem WithZero.addLeftMono {α : Type u_1} [Preorder α] [AddZeroClass α] [AddLeftMono α] (h : ∀ (a : α), 0 a) :
        theorem WithZero.map'_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : Monotone f) :
        Monotone (map' f)
        theorem WithZero.map'_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : StrictMono f) :
        theorem WithZero.le_max_iff {α : Type u_1} [LinearOrder α] {a b c : α} :
        a max b c a max b c
        theorem WithZero.min_le_iff {α : Type u_1} [LinearOrder α] {a b c : α} :
        min a b c min a b c
        theorem WithZero.isOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (zero_le : ∀ (a : α), 0 a) :

        If 0 is the least element in α, then WithZero α is an ordered AddMonoid.

        Adding a new zero to a canonically ordered additive monoid produces another one.

        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.

        Exponential and logarithm #

        @[simp]
        theorem WithZero.exp_le_exp {G : Type u_3} [Preorder G] {a b : G} :
        exp a exp b a b
        @[simp]
        theorem WithZero.exp_lt_exp {G : Type u_3} [Preorder G] {a b : G} :
        exp a < exp b a < b
        @[simp]
        theorem WithZero.exp_pos {G : Type u_3} [Preorder G] {a : G} :
        0 < exp a
        @[simp]
        theorem WithZero.log_le_log {G : Type u_3} [Preorder G] [AddGroup G] {x y : WithZero (Multiplicative G)} (hx : x 0) (hy : y 0) :
        x.log y.log x y
        @[simp]
        theorem WithZero.log_lt_log {G : Type u_3} [Preorder G] [AddGroup G] {x y : WithZero (Multiplicative G)} (hx : x 0) (hy : y 0) :
        x.log < y.log x < y
        theorem WithZero.log_le_iff_le_exp {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x 0) :
        x.log a x exp a
        theorem WithZero.log_lt_iff_lt_exp {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x 0) :
        x.log < a x < exp a
        theorem WithZero.le_log_iff_exp_le {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x 0) :
        a x.log exp a x
        theorem WithZero.lt_log_iff_exp_lt {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x 0) :
        a < x.log exp a < x
        theorem WithZero.le_exp_of_log_le {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hxa : x.log a) :
        x exp a
        theorem WithZero.lt_exp_of_log_lt {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hxa : x.log < a) :
        x < exp a
        theorem WithZero.le_log_of_exp_le {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hax : exp a x) :
        a x.log
        theorem WithZero.lt_log_of_exp_lt {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hax : exp a < x) :
        a < x.log

        The exponential map as an order isomorphism between G and Gᵐ⁰ˣ.

        Equations
        Instances For
          @[simp]
          theorem WithZero.val_inv_expOrderIso_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) :
          @[simp]
          theorem WithZero.val_expOrderIso_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) :
          (expOrderIso a✝) = (Multiplicative.ofAdd a✝)

          The logarithm as an order isomorphism between Gᵐ⁰ˣ and G.

          Equations
          Instances For
            @[simp]
            theorem WithZero.val_logOrderIso_symm_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) :
            theorem WithZero.lt_mul_exp_iff_le {x y : WithZero (Multiplicative )} (hy : y 0) :
            x < y * exp 1 x y