Adjoining a top element to a LinearOrderedAddCommGroupWithTop.

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WithTop.coe_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) : ↑(-a) = -↑a