Adjoining a top element to a LinearOrderedAddCommGroupWithTop
. #
instance
WithTop.linearOrderedAddCommGroupWithTop
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]