Skip to main content

OrderedField

typeclass F: OrderedField extends Field, AddOrderedGroup {
    mul_preserves_nonnegativity(a: F, b: F) {
        F.0 <= a and F.0 <= b implies F.0 <= a * b
    }
}

A field with a total order compatible with the field operations.

GitHub

add​

Inherited from Add.

add_associative​

Inherited from AddSemigroup.

add_commutative​

Inherited from AddCommSemigroup.

add_identity_left​

Inherited from AddMonoid.

add_identity_right​

Inherited from AddMonoid.

antisymmetric​

Inherited from PartialOrder.

commutative​

Inherited from CommSemigroup.

distrib_left​

Inherited from Semiring.

distrib_right​

Inherited from Semiring.

field_inverse​

Inherited from Field.

field_inverse_zero​

Inherited from Field.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

inverse​

Inherited from Inverse.

inverse_right​

Inherited from AddGroup.

left_invariance​

Inherited from AddLeftOrderedGroup.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

max​

Inherited from LinearOrder.

min​

Inherited from LinearOrder.

mul​

Inherited from Mul.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

Inherited from Monoid.

mul_identity_right​

Inherited from Monoid.

mul_preserves_nonnegativity​

mul_preserves_nonnegativity(a: F, b: F) {
    F.0 <= a and F.0 <= b implies F.0 <= a * b
}

product of non-negative elements is non-negative

mul_zero_left​

Inherited from Semiring.

mul_zero_right​

Inherited from Semiring.

neg​

Inherited from Neg.

pow​

Inherited from Monoid.

reflexive​

Inherited from PartialOrder.

right_invariance​

Inherited from AddOrderedGroup.

sub​

Inherited from AddGroup.

totality​

Inherited from LinearOrder.

transitive​

Inherited from PartialOrder.

zero_and_one_are_distinct​

Inherited from Field.

zpow​

Inherited from Field.