Canonically ordered semifields

class CanonicallyLinearOrderedSemifield (α : Type u_2) extends CanonicallyOrderedCommSemiring , LinearOrderedSemifield , CanonicallyOrderedAddCommMonoid , LinearOrderedCommSemiring , Semifield , StrictOrderedCommSemiring , LinearOrderedSemiring , StrictOrderedSemiring , CommSemiring , LinearOrderedAddCommMonoid , DivisionSemiring , CommGroupWithZero , OrderedAddCommMonoid , OrderBot , Semiring , OrderedCancelAddCommMonoid , CommMonoidWithZero , GroupWithZero , Nontrivial , CommMonoid , NNRatCast , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , DivInvMonoid , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , CommSemigroup , Inv , Div , MulOneClass , AddMonoidWithOne , LinearOrder , AddCommMonoid , PartialOrder , Distrib , Semigroup , MulZeroClass , NatCast , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , CommMagma , Mul , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT , Bot : Type u_2

A canonically linear ordered field is a linear ordered field in which a ≤ b iff there exists c with b = a + c.

@[instance 100]

instance CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero {α : Type u_1} [CanonicallyLinearOrderedSemifield α] : LinearOrderedCommGroupWithZero α

Equations

• CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero = LinearOrderedCommGroupWithZero.mk ⋯ CanonicallyLinearOrderedSemifield.zpow ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 100]

instance CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid {α : Type u_1} [CanonicallyLinearOrderedSemifield α] : CanonicallyLinearOrderedAddCommMonoid α

Equations

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