Documentation

Mathlib.Algebra.Order.Group.WithTop

Adjoining a top element to a LinearOrderedAddCommGroupWithTop. #

Equations
Equations
  • WithTop.linearOrderedAddCommGroupWithTop = let __spread.0 := WithTop.linearOrderedAddCommMonoidWithTop; let __spread.1 := ; LinearOrderedAddCommGroupWithTop.mk zsmulRec
@[simp]
theorem WithTop.coe_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) :
(-a) = -a