Idris2Doc : Algebra.Ring

Algebra.Ring

(source)
Definitions
0 LeftDistributive : Op2 a -> Op2 a -> Type
  Proposition that multiplication distributes over addition

  Totality: total
  Visibility: public export
0 MultZeroLeftAbsorbs : a -> Op2 a -> Type
  Proposition that multiplication by zero returns zero

  Totality: total
  Visibility: public export
0 MinusAssociative : Op2 a -> Op2 a -> Type
  Proposition that subtraction is associative with addition.

  Totality: total
  Visibility: public export
0 ZeroMinus : a -> Op2 a -> Op2 a -> Type
  Proposition that subtraction from zero is a left inverse.

  Totality: total
  Visibility: public export
record Rig : (a : Type) -> a -> a -> Op2 a -> Op2 a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRig : CommutativeMonoid a z p -> CommutativeMonoid a o m -> LeftDistributive p m -> MultZeroLeftAbsorbs z m -> Rig a z o p m

  Projections:
  
.leftDistributive : Rig a z o p m -> LeftDistributive p m
  
.mult : Rig a z o p m -> CommutativeMonoid a o m
  
.multZeroLeftAbsorbs : Rig a z o p m -> MultZeroLeftAbsorbs z m
  
0 .multZeroRightAbsorbs : Rig a z o p m -> x `m` z = z
  Zero is an absorbing element of multiplication.
  
.plus : Rig a z o p m -> CommutativeMonoid a z p
  
0 .rightDistributive : Rig a z o p m -> (y `p` v) `m` x = (y `m` x) `p` (v `m` x)
  Multiplication is distributive with respect to addition.
.plus : Rig a z o p m -> CommutativeMonoid a z p
  Totality: total
  Visibility: public export
plus : Rig a z o p m -> CommutativeMonoid a z p
  Totality: total
  Visibility: public export
.mult : Rig a z o p m -> CommutativeMonoid a o m
  Totality: total
  Visibility: public export
mult : Rig a z o p m -> CommutativeMonoid a o m
  Totality: total
  Visibility: public export
.leftDistributive : Rig a z o p m -> LeftDistributive p m
  Totality: total
  Visibility: public export
leftDistributive : Rig a z o p m -> LeftDistributive p m
  Totality: total
  Visibility: public export
.multZeroLeftAbsorbs : Rig a z o p m -> MultZeroLeftAbsorbs z m
  Totality: total
  Visibility: public export
multZeroLeftAbsorbs : Rig a z o p m -> MultZeroLeftAbsorbs z m
  Totality: total
  Visibility: public export
0 .multZeroRightAbsorbs : Rig a z o p m -> x `m` z = z
  Zero is an absorbing element of multiplication.

  Totality: total
  Visibility: export
0 .rightDistributive : Rig a z o p m -> (y `p` v) `m` x = (y `m` x) `p` (v `m` x)
  Multiplication is distributive with respect to addition.

  Totality: total
  Visibility: export
multZeroAbsorbs : Rig a z o p m -> Either (x = z) (y = z) -> x `m` y = z
  Zero is an absorbing element of multiplication.

  Totality: total
  Visibility: export
0 NatRig : Rig Nat 0 1 (+) (*)
  Totality: total
  Visibility: export
record Ring : (a : Type) -> a -> a -> Op2 a -> Op2 a -> Op2 a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRing : CommutativeMonoid a z p -> CommutativeMonoid a o m -> LeftDistributive p m -> MinusAssociative p sub -> ZeroMinus z p sub -> Ring a z o p m sub

  Projections:
  
.leftDistributive : Ring a z o p m sub -> LeftDistributive p m
  
.minusAssociative : Ring a z o p m sub -> MinusAssociative p sub
  
0 .minusIsPlusLeft : Ring a z o p m sub -> x `sub` y = (z `sub` y) `p` x
  
0 .minusIsPlusRight : Ring a z o p m sub -> x `sub` y = x `p` (z `sub` y)
  
0 .minusSelf : Ring a z o p m sub -> x `sub` x = z
  
.mult : Ring a z o p m sub -> CommutativeMonoid a o m
  
0 .multMinusOneLeft : Ring a z o p m sub -> (z `sub` o) `m` x = z `sub` x
  
0 .multMinusOneRight : Ring a z o p m sub -> x `m` (z `sub` o) = z `sub` x
  
0 .multNegLeft : Ring a z o p m sub -> (z `sub` x) `m` y = z `sub` (x `m` y)
  
0 .multNegRight : Ring a z o p m sub -> x `m` (z `sub` y) = z `sub` (x `m` y)
  
0 .multZeroLeftAbsorbs : Ring a z o p m sub -> z `m` x = z
  
0 .multZeroRightAbsorbs : Ring a z o p m sub -> x `m` z = z
  
0 .negMultNeg : Ring a z o p m sub -> (z `sub` x) `m` (z `sub` y) = x `m` y
  
0 .negMultNegLeft : Ring a z o p m sub -> z `sub` ((z `sub` x) `m` y) = x `m` y
  
0 .negMultNegRight : Ring a z o p m sub -> z `sub` (x `m` (z `sub` y)) = x `m` y
  
0 .plus : Ring a z o p m sub -> AbelianGroup a z (\{arg:0} => z `sub` {arg:0}) p
  
.plusMon : Ring a z o p m sub -> CommutativeMonoid a z p
  
0 .rig : Ring a z o p m sub -> Rig a z o p m
  
.zeroMinus : Ring a z o p m sub -> ZeroMinus z p sub
.plusMon : Ring a z o p m sub -> CommutativeMonoid a z p
  Totality: total
  Visibility: public export
plusMon : Ring a z o p m sub -> CommutativeMonoid a z p
  Totality: total
  Visibility: public export
.mult : Ring a z o p m sub -> CommutativeMonoid a o m
  Totality: total
  Visibility: public export
mult : Ring a z o p m sub -> CommutativeMonoid a o m
  Totality: total
  Visibility: public export
.leftDistributive : Ring a z o p m sub -> LeftDistributive p m
  Totality: total
  Visibility: public export
leftDistributive : Ring a z o p m sub -> LeftDistributive p m
  Totality: total
  Visibility: public export
.minusAssociative : Ring a z o p m sub -> MinusAssociative p sub
  Totality: total
  Visibility: public export
minusAssociative : Ring a z o p m sub -> MinusAssociative p sub
  Totality: total
  Visibility: public export
.zeroMinus : Ring a z o p m sub -> ZeroMinus z p sub
  Totality: total
  Visibility: public export
zeroMinus : Ring a z o p m sub -> ZeroMinus z p sub
  Totality: total
  Visibility: public export
0 .plus : Ring a z o p m sub -> AbelianGroup a z (\{arg:0} => z `sub` {arg:0}) p
  Totality: total
  Visibility: export
0 .multZeroRightAbsorbs : Ring a z o p m sub -> x `m` z = z
  Totality: total
  Visibility: export
0 .multZeroLeftAbsorbs : Ring a z o p m sub -> z `m` x = z
  Totality: total
  Visibility: export
0 .rig : Ring a z o p m sub -> Rig a z o p m
  Totality: total
  Visibility: export
0 .minusSelf : Ring a z o p m sub -> x `sub` x = z
  Totality: total
  Visibility: export
0 .minusIsPlusRight : Ring a z o p m sub -> x `sub` y = x `p` (z `sub` y)
  Totality: total
  Visibility: export
0 .minusIsPlusLeft : Ring a z o p m sub -> x `sub` y = (z `sub` y) `p` x
  Totality: total
  Visibility: export
0 .multNegRight : Ring a z o p m sub -> x `m` (z `sub` y) = z `sub` (x `m` y)
  Totality: total
  Visibility: export
0 .negMultNegRight : Ring a z o p m sub -> z `sub` (x `m` (z `sub` y)) = x `m` y
  Totality: total
  Visibility: export
0 .multNegLeft : Ring a z o p m sub -> (z `sub` x) `m` y = z `sub` (x `m` y)
  Totality: total
  Visibility: export
0 .negMultNegLeft : Ring a z o p m sub -> z `sub` ((z `sub` x) `m` y) = x `m` y
  Totality: total
  Visibility: export
0 .multMinusOneRight : Ring a z o p m sub -> x `m` (z `sub` o) = z `sub` x
  Totality: total
  Visibility: export
0 .multMinusOneLeft : Ring a z o p m sub -> (z `sub` o) `m` x = z `sub` x
  Totality: total
  Visibility: export
0 .negMultNeg : Ring a z o p m sub -> (z `sub` x) `m` (z `sub` y) = x `m` y
  Totality: total
  Visibility: export
0 ring_bits8 : Ring Bits8 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_bits16 : Ring Bits16 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_bits32 : Ring Bits32 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_bits64 : Ring Bits64 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_int8 : Ring Int8 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_int16 : Ring Int16 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_int32 : Ring Int32 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_int64 : Ring Int64 0 1 (+) (*) (-)
  Totality: total
  Visibility: export
0 ring_integer : Ring Integer 0 1 (+) (*) (-)
  Totality: total
  Visibility: export