Adjoining a top element to a LinearOrderedAddCommGroupWithTop.

ink

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

Equations

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

ink

@[simp]

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