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_2} [Zero β] [One β] [Mul β] [Pow β ] [Max β] [Min β] (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) = f x f y) (hinf : ∀ (x y : β), f (x y) = 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
        @[deprecated mul_inv_le_of_le_mul₀]
        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
        @[deprecated mul_lt_mul_of_le_of_lt_of_nonneg_of_pos]
        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
        @[deprecated mul_lt_mul'']
        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
        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 div_le_div_iff_of_pos_right]
        theorem div_le_div_right₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a b c : α} (hc : c 0) :
        a / c b / c a b
        @[deprecated div_le_div_iff_of_pos_left]
        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
        @[deprecated OrderIso.mulLeft₀]
        def OrderIso.mulLeft₀' {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) :
        α ≃o α

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

        Equations
        Instances For
          @[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 : α) :
          @[deprecated OrderIso.mulLeft₀_symm]
          @[deprecated OrderIso.mulRight₀]
          def OrderIso.mulRight₀' {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) :
          α ≃o α

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

          Equations
          Instances For
            @[simp]
            theorem OrderIso.mulRight₀'_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) (x : α) :
            @[simp]
            theorem OrderIso.mulRight₀'_toEquiv {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a 0) :
            @[deprecated OrderIso.mulRight₀_symm]
            Equations
            Equations
            @[deprecated pow_lt_pow_right₀]
            theorem pow_lt_pow_succ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {n : } (ha : 1 < a) :
            a ^ n < a ^ n.succ
            @[simp]
            theorem ofAdd_toDual_eq_zero_iff {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (x : α) :
            Multiplicative.ofAdd (OrderDual.toDual x) = 0 x =
            @[simp]
            theorem ofDual_toAdd_eq_top_iff {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (x : Multiplicative αᵒᵈ) :
            OrderDual.ofDual (Multiplicative.toAdd x) = x = 0
            @[simp]
            theorem ofAdd_bot {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] :
            Multiplicative.ofAdd = 0
            @[simp]
            theorem ofDual_toAdd_zero {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] :
            OrderDual.ofDual (Multiplicative.toAdd 0) =
            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
            @[simp]
            theorem WithZero.unzero_le_unzero {α : Type u_1} [Preorder α] {a b : WithZero α} (ha : a 0) (hb : b 0) :
            theorem WithZero.addLeftMono {α : Type u_1} [Preorder α] [AddZeroClass α] [AddLeftMono α] (h : ∀ (a : α), 0 a) :
            Equations
            • WithZero.partialOrder = WithBot.partialOrder
            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 b c a b c
            theorem WithZero.min_le_iff {α : Type u_1} [LinearOrder α] {a b c : α} :
            a b c 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