Documentation

Mathlib.Algebra.Order.AddGroupWithTop

Linearly ordered commutative additive groups and monoids with a top element adjoined #

This file sets up a special class of linearly ordered commutative additive 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 additive group Γ and formally adjoining a top element: Γ ∪ {⊤}.

The disadvantage is that a type such as ENNReal 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 an additively absorbing element. Instances should include number systems with an infinite element adjoined.

  • add : ααα
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : αα
  • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
  • add_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
  • add_le_add_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
  • top : α
  • le_top : ∀ (a : α), a
  • top_add' : ∀ (x : α), + x =

    In a LinearOrderedAddCommMonoidWithTop, the element is invariant under addition.

Instances

    In a LinearOrderedAddCommMonoidWithTop, the element is invariant under addition.

    A linearly ordered commutative group with an additively absorbing element. Instances should include number systems with an infinite element adjoined.

    Instances
      @[simp]
      theorem top_add {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) :
      @[simp]
      theorem add_top {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) :
      Equations
      • WithTop.LinearOrderedAddCommGroup.instNeg = { neg := Option.map fun (a : α) => -a }

      If α has subtraction, we can extend the subtraction to WithTop α, by setting x - ⊤ = ⊤ and ⊤ - x = ⊤. This definition is only registered as an instance on linearly ordered additive commutative groups, to avoid conflicting with the instance WithTop.instSub on types with a bottom element.

      Equations
      Instances For
        Equations
        • WithTop.LinearOrderedAddCommGroup.instSub = { sub := WithTop.LinearOrderedAddCommGroup.sub }
        @[simp]
        theorem WithTop.LinearOrderedAddCommGroup.coe_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) :
        (-a) = -a
        @[simp]
        theorem WithTop.LinearOrderedAddCommGroup.coe_sub {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} :
        (a - b) = a - b
        Equations