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 LinearOrderedAddCommGroup
s 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
.
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 }
Equations
- One or more equations did not get rendered due to their size.