Adjoining a top element to a LinearOrderedAddCommGroupWithTop.

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

Equations

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

instance WithTop.linearOrderedAddCommGroupWithTop {α : Type u_1} [LinearOrderedAddCommGroup α] : LinearOrderedAddCommGroupWithTop (WithTop α)

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