Canonically ordered semifields

@[reducible, inline]

abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero {α : Type u_1} [Semifield α] [LinearOrder α] [CanonicallyOrderedAdd α] : LinearOrderedCommGroupWithZero α

Construct a LinearOrderedCommGroupWithZero from a canonically linear ordered semifield.

Equations

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

theorem tsub_div {α : Type u_1} [Semifield α] [LinearOrder α] [CanonicallyOrderedAdd α] [IsStrictOrderedRing α] [Sub α] [OrderedSub α] (a b c : α) : (a - b) / c = a / c - b / c