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.

  • mul : ααα
  • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : αα
  • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
  • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
  • min : ααα
  • max : ααα
  • compare : ααOrdering
  • le_total : ∀ (a b : α), a b b a
  • decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2
  • decidableEq : DecidableEq α
  • decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
  • min_def : ∀ (a b : α), min a b = if a b then a else b
  • max_def : ∀ (a b : α), max a b = if a b then b else a
  • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
  • zero : α
  • zero_mul : ∀ (a : α), 0 * a = 0

    Zero is a left absorbing element for multiplication

  • mul_zero : ∀ (a : α), a * 0 = 0

    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.

    Instances
      @[reducible, inline]
      abbrev Function.Injective.linearOrderedCommMonoidWithZero {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {β : Type u_2} [Zero β] [One β] [Mul β] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : Function.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 (x y) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

      Pullback a LinearOrderedCommMonoidWithZero under an injective map. See note [reducible non-instances].

      Equations
      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
        theorem pow_pos_iff {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} {n : } [NoZeroDivisors α] (hn : n 0) :
        0 < a ^ n 0 < a
        @[instance 100]
        Equations
        • =
        @[instance 100]
        Equations
        • =
        @[deprecated mul_le_one']
        theorem mul_le_one₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} (ha : a 1) (hb : b 1) :
        a * b 1

        Alias of mul_le_one' for unification.

        @[deprecated one_le_mul]
        theorem one_le_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
        1 a * b

        Alias of one_le_mul' for unification.

        @[deprecated mul_le_mul_right]
        theorem le_of_le_mul_right {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (h : c 0) (hab : a * c b * c) :
        a b
        @[deprecated le_mul_inv_iff₀]
        theorem le_mul_inv_of_mul_le {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (h : c 0) (hab : a * c b) :
        a b * c⁻¹
        theorem mul_inv_le_of_le_mul {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (hab : a b * c) :
        a * c⁻¹ b
        @[simp]
        theorem Units.zero_lt {α : Type u_1} [LinearOrderedCommGroupWithZero α] (u : αˣ) :
        0 < u
        theorem mul_lt_mul_of_lt_of_le₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hb : b 0) (hcd : c < d) :
        a * c < b * d
        theorem mul_lt_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) :
        a * c < b * d
        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
        @[deprecated mul_lt_mul_of_pos_right]
        theorem mul_lt_right₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} (c : α) (h : a < b) (hc : c 0) :
        a * c < b * c
        theorem inv_lt_inv₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} (ha : a 0) (hb : b 0) :
        a⁻¹ < b⁻¹ b < a
        theorem inv_le_inv₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} (ha : a 0) (hb : b 0) :
        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
        @[deprecated mul_le_mul_right]
        theorem mul_le_mul_right₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (hc : c 0) :
        a * c b * c a b
        @[deprecated mul_le_mul_left]
        theorem mul_le_mul_left₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (ha : a 0) :
        a * b a * c b c
        theorem div_le_div_right₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (hc : c 0) :
        a / c b / c a b
        theorem div_le_div_left₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (ha : a 0) (hb : b 0) (hc : c 0) :
        a / b a / c c b
        @[simp]
        theorem OrderIso.mulLeft₀'_toEquiv {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) :
        @[simp]
        theorem OrderIso.mulLeft₀'_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) (x : α) :
        def OrderIso.mulLeft₀' {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) :
        α ≃o α

        Equiv.mulLeft₀ as an OrderIso on a LinearOrderedCommGroupWithZero..

        Note that OrderIso.mulLeft₀ refers to the LinearOrderedField version.

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem OrderIso.mulRight₀'_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) (x : α) :
          def OrderIso.mulRight₀' {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) :
          α ≃o α

          Equiv.mulRight₀ as an OrderIso on a LinearOrderedCommGroupWithZero..

          Note that OrderIso.mulRight₀ refers to the LinearOrderedField version.

          Equations
          Instances For
            Equations
            theorem pow_lt_pow_succ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {n : } (ha : 1 < a) :
            a ^ n < a ^ n.succ
            theorem pow_lt_pow_right₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {m : } {n : } (ha : 1 < a) (hmn : m < n) :
            a ^ m < a ^ n
            @[deprecated pow_lt_pow_right₀]
            theorem pow_lt_pow₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {m : } {n : } (ha : 1 < a) (hmn : m < n) :
            a ^ m < a ^ n

            Alias of pow_lt_pow_right₀.

            Equations
            instance WithZero.preorder {α : Type u_1} [Preorder α] :
            Equations
            • WithZero.preorder = WithBot.preorder
            instance WithZero.orderBot {α : Type u_1} [Preorder α] :
            Equations
            • WithZero.orderBot = WithBot.orderBot
            theorem WithZero.zero_le {α : Type u_1} [Preorder α] (a : WithZero α) :
            0 a
            theorem WithZero.zero_lt_coe {α : Type u_1} [Preorder α] (a : α) :
            0 < a
            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
            instance WithZero.covariantClass_mul_le {α : Type u_1} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
            CovariantClass (WithZero α) (WithZero α) (fun (x1 x2 : WithZero α) => x1 * x2) fun (x1 x2 : WithZero α) => x1 x2
            Equations
            • =
            theorem WithZero.covariantClass_add_le {α : Type u_1} [Preorder α] [AddZeroClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : ∀ (a : α), 0 a) :
            CovariantClass (WithZero α) (WithZero α) (fun (x1 x2 : WithZero α) => x1 + x2) fun (x1 x2 : WithZero α) => x1 x2
            Equations
            • =
            Equations
            • WithZero.partialOrder = WithBot.partialOrder
            instance WithZero.contravariantClass_mul_lt {α : Type u_1} [PartialOrder α] [Mul α] [ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
            ContravariantClass (WithZero α) (WithZero α) (fun (x1 x2 : WithZero α) => x1 * x2) fun (x1 x2 : WithZero α) => x1 < x2
            Equations
            • =
            instance WithZero.lattice {α : Type u_1} [Lattice α] :
            Equations
            • WithZero.lattice = WithBot.lattice
            Equations
            • WithZero.linearOrder = WithBot.linearOrder
            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
            Equations
            @[reducible, inline]
            abbrev WithZero.orderedAddCommMonoid {α : Type u_1} [OrderedAddCommMonoid α] (zero_le : ∀ (a : α), 0 a) :

            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
              Equations
              Equations
              Equations

              Notation for WithZero (Multiplicative ℕ)

              Equations
              Instances For

                Notation for WithZero (Multiplicative ℤ)

                Equations
                Instances For