Algebra.OrderedRing

Definitions

record OrderedRing : (a : Type) -> (a -> a -> Type) -> a -> a -> Op2 a -> Op2 a -> Op2 a -> Type

Totality: total
Visibility: public export
Constructor: 

MkOR : Ring a z o p m sub -> Strict a lt -> (lt u v -> lt (u `p` w) (v `p` w)) -> (lt u v -> lt z w -> lt (u `m` w) (v `m` w)) -> OrderedRing a lt z o p m sub

Projections:

.add : OrderedRing a lt z o p m sub -> lt u v -> lt (u `p` w) (v `p` w)

.mult : OrderedRing a lt z o p m sub -> lt u v -> lt z w -> lt (u `m` w) (v `m` w)

.ring : OrderedRing a lt z o p m sub -> Ring a z o p m sub

.strict : OrderedRing a lt z o p m sub -> Strict a lt

.ring : OrderedRing a lt z o p m sub -> Ring a z o p m sub

Totality: total
Visibility: public export

ring : OrderedRing a lt z o p m sub -> Ring a z o p m sub

Totality: total
Visibility: public export

.strict : OrderedRing a lt z o p m sub -> Strict a lt

Totality: total
Visibility: public export

strict : OrderedRing a lt z o p m sub -> Strict a lt

Totality: total
Visibility: public export

.add : OrderedRing a lt z o p m sub -> lt u v -> lt (u `p` w) (v `p` w)

Totality: total
Visibility: public export

add : OrderedRing a lt z o p m sub -> lt u v -> lt (u `p` w) (v `p` w)

Totality: total
Visibility: public export

.mult : OrderedRing a lt z o p m sub -> lt u v -> lt z w -> lt (u `m` w) (v `m` w)

Totality: total
Visibility: public export

mult : OrderedRing a lt z o p m sub -> lt u v -> lt z w -> lt (u `m` w) (v `m` w)

Totality: total
Visibility: public export

0 plusRight : (0 _ : OrderedRing a lt z o p m sub) -> lt u v -> lt (u `p` w) (v `p` w)

  Adding a value on the right does not affect an inequality.

Totality: total
Visibility: export

0 plusLeft : (0 _ : OrderedRing a lt z o p m sub) -> lt u v -> lt (w `p` u) (w `p` v)

  Adding a value on the left does not affect an inequality.

Totality: total
Visibility: export

0 plusPosRight : (0 _ : OrderedRing a lt z o p m sub) -> lt z v -> lt u (u `p` v)

  The result of adding a positive value is greater than
  the original.

Totality: total
Visibility: export

0 plusPosLeft : (0 _ : OrderedRing a lt z o p m sub) -> lt z v -> lt u (v `p` u)

  The result of adding a positive value is greater than
  the original.

Totality: total
Visibility: export

0 plusNonNegRight : (0 _ : OrderedRing a lt z o p m sub) -> ReflexiveClosure lt z u -> ReflexiveClosure lt v (v `p` u)

  The result of adding a non-negative value is not less than
  the original.

Totality: total
Visibility: export

0 plusNonNegLeft : (0 _ : OrderedRing a lt z o p m sub) -> ReflexiveClosure lt z u -> ReflexiveClosure lt v (u `p` v)

  The result of adding a non-negative value is not less than
  the original.

Totality: total
Visibility: export

0 plusNegRight : (0 _ : OrderedRing a lt z o p m sub) -> lt v z -> lt (u `p` v) u

  The result of adding a negative value is less than
  the original.

Totality: total
Visibility: export

0 plusNegLeft : (0 _ : OrderedRing a lt z o p m sub) -> lt v z -> lt (v `p` u) u

  The result of adding a negative value is less than
  the original.

Totality: total
Visibility: export

0 plusNonPosRight : (0 _ : OrderedRing a lt z o p m sub) -> ReflexiveClosure lt u z -> ReflexiveClosure lt (v `p` u) v

  The result of adding a non-positive value is not greater than
  the original.

Totality: total
Visibility: export

0 plusNonPosLeft : (0 _ : OrderedRing a lt z o p m sub) -> ReflexiveClosure lt u z -> ReflexiveClosure lt (u `p` v) v

  The result of adding a non-positive value is not greater than
  the original.

Totality: total
Visibility: export

0 solvePlusRight : (0 _ : OrderedRing a lt z o p m sub) -> lt (u `p` w) (v `p` w) -> lt u v

  We can solve (in)equalities, where the same value has
  been added on both sides.

Totality: total
Visibility: export