Adjoining a top element to a `LinearOrderedAddCommGroup`. #

This file defines a negation on WithTop α when α is a linearly ordered additive commutative group, by setting -⊤ = ⊤. This corresponds to the additivization of the usual multiplicative convention 0⁻¹ = 0, and is relevant in valuation theory.

Note that there is another subtraction on objects of the form WithTop α in the file Mathlib.Algebra.Order.Sub.WithTop, setting -⊤ = ⊥ when α has a bottom element. This is the right convention for ℕ∞ or ℝ≥0∞. Since LinearOrderedAddCommGroups don't have a bottom element (unless they are trivial), this shouldn't create diamonds.

To avoid conflicts between the two notions, we put everything in the current file in the namespace WithTop.LinearOrderedAddCommGroup.

source

instance WithTop.LinearOrderedAddCommGroup.instNeg {α : Type u_1} [LinearOrderedAddCommGroup α] :

Neg (WithTop α)

Equations

WithTop.LinearOrderedAddCommGroup.instNeg = { neg := Option.map fun (a : α) => -a }

source

def WithTop.LinearOrderedAddCommGroup.sub {α : Type u_1} [LinearOrderedAddCommGroup α] :

WithTop α → WithTop α → WithTop α

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