Idris2Doc : Algebra.Ring

Algebra.Ring

(source)
Definitions
neg : Neg a => a -> a
  Totality: total
  Visibility: public export
interface Ring : Type -> Type
  This interface is a witness that for a (primitive)
  integral type `a` the axioms of a commutative ring hold:
  
  1. `a` is an abelian group under addition:
     1. `+` is associative: `k + (m + n) = (k + m) + n` for all `k,m,n : a`.
     2. `+` is commutative: `m + n = n + m` for all `m,n : a`.
     3. 0 is the additive identity: `n + 0 = n` for all `n : a`.
     4. `neg n` is the additive inverse of `n`:
        `n + neg n = 0` for all `n : a`.
  
  2. `a` is a commutative monoid under multiplication:
     1. `*` is associative: `k * (m * n) = (k * m) * n` for all `k,m,n : a`.
     2. `*` is commutative: `m * n = n * m` for all `m,n : a`.
     3. 1 is the multiplicative identity: `n * 1 = n` for all `n : a`.
  
  3. Multiplication is distributive with respect to addition:
     `k * (m + n) = (k * m) + (k * n)` for all `k,m,n : a`.
  
  4. Subtraction syntax: `m - n = m + neg n` for all `m,n : a`.

  Parameters: a
Constraints: Neg a
Methods:
  
0 plusAssociative : k + (m + n) = (k + m) + n
  Addition is associative.
  
0 plusCommutative : m + n = n + m
  Addition is commutative.
  
0 plusZeroLeftNeutral : 0 + n = n
  0 is the additive identity.
  
0 plusNegLeftZero : neg n + n = 0
  `neg n` is the additive inverse of `n`.
  
0 multAssociative : k * (m * n) = (k * m) * n
  Multiplication is associative.
  
0 multCommutative : m * n = n * m
  Multiplication is commutative.
  
0 multOneLeftNeutral : 1 * n = n
  1 is the multiplicative identity.
  
0 leftDistributive : k * (m + n) = (k * m) + (k * n)
  Multiplication is distributive with respect to addition.
  
0 minusIsPlusNeg : m - n = m + neg n
  `m - n` is just "syntactic sugar" for `m + neg n`.

Implementations:
  
Ring Bits8
  
Ring Bits16
  
Ring Bits32
  
Ring Bits64
  
Ring Int8
  
Ring Int16
  
Ring Int32
  
Ring Int64
  
Ring Int
  
Ring Integer
0 plusAssociative : {auto __con : Ring a} -> k + (m + n) = (k + m) + n
  Addition is associative.

  Totality: total
  Visibility: public export
0 plusCommutative : {auto __con : Ring a} -> m + n = n + m
  Addition is commutative.

  Totality: total
  Visibility: public export
0 plusZeroLeftNeutral : {auto __con : Ring a} -> 0 + n = n
  0 is the additive identity.

  Totality: total
  Visibility: public export
0 plusNegLeftZero : {auto __con : Ring a} -> neg n + n = 0
  `neg n` is the additive inverse of `n`.

  Totality: total
  Visibility: public export
0 multAssociative : {auto __con : Ring a} -> k * (m * n) = (k * m) * n
  Multiplication is associative.

  Totality: total
  Visibility: public export
0 multCommutative : {auto __con : Ring a} -> m * n = n * m
  Multiplication is commutative.

  Totality: total
  Visibility: public export
0 multOneLeftNeutral : {auto __con : Ring a} -> 1 * n = n
  1 is the multiplicative identity.

  Totality: total
  Visibility: public export
0 leftDistributive : {auto __con : Ring a} -> k * (m + n) = (k * m) + (k * n)
  Multiplication is distributive with respect to addition.

  Totality: total
  Visibility: public export
0 minusIsPlusNeg : {auto __con : Ring a} -> m - n = m + neg n
  `m - n` is just "syntactic sugar" for `m + neg n`.

  Totality: total
  Visibility: public export
0 plusZeroRightNeutral : {auto {conArg:1571} : Ring a} -> n + 0 = n
  `n + 0 === n` for all `n : a`.

  Totality: total
  Visibility: export
0 plusNegRightZero : {auto {conArg:1661} : Ring a} -> n + neg n = 0
  `n + neg n === 0` for all `n : a`.

  Totality: total
  Visibility: export
0 minusSelfZero : {auto {conArg:1757} : Ring a} -> n - n = 0
  `n - n === 0` for all `n : a`.

  Totality: total
  Visibility: export
0 plusMinusAssociative : {auto {conArg:1841} : Ring a} -> k + (m - n) = (k + m) - n
  Law of associativity for subtraction.

  Totality: total
  Visibility: export
0 solvePlusRight : {auto {conArg:2012} : Ring a} -> k + m = n -> k = n - m
  We can solve equations involving addition.

  Totality: total
  Visibility: export
0 solvePlusLeft : {auto {conArg:2180} : Ring a} -> k + m = n -> m = n - k
  We can solve equations involving addition.

  Totality: total
  Visibility: export
0 plusLeftInjective : {auto {conArg:2279} : Ring a} -> k + n = m + n -> k = m
  Addition from the left is injective.

  Totality: total
  Visibility: export
0 plusRightInjective : {auto {conArg:2441} : Ring a} -> n + k = n + m -> k = m
  Addition from the right is injective.

  Totality: total
  Visibility: export
0 solvePlusNegRight : {auto {conArg:2569} : Ring a} -> m + n = 0 -> n = neg m
  From `m + n === 0` follows that `n` is the
  additive inverse of `m`.

  Totality: total
  Visibility: export
0 solvePlusNegLeft : {auto {conArg:2634} : Ring a} -> m + n = 0 -> m = neg n
  From `m + n === 0` follows that `m` is the
  additive inverse of `n`.

  Totality: total
  Visibility: export
0 solvePlusZeroRight : {auto {conArg:2738} : Ring a} -> m + n = m -> n = 0
  From `m + n === m` follows `n === 0`.

  Totality: total
  Visibility: export
0 solvePlusZeroLeft : {auto {conArg:2828} : Ring a} -> n + m = m -> n = 0
  From `n + m === m` follows `n === 0`.

  Totality: total
  Visibility: export
0 negInvolutory : {auto {conArg:2921} : Ring a} -> neg (neg n) = n
  Negation is involutory.

  Totality: total
  Visibility: export
0 solveNegZero : {auto {conArg:2960} : Ring a} -> neg n = 0 -> n = 0
  From `neg n === 0` follows `n === 0`.

  Totality: total
  Visibility: export
0 negZero : {auto {conArg:3085} : Ring a} -> neg 0 = 0
  `neg 0 === 0`

  Totality: total
  Visibility: export
0 negDistributes : {auto {conArg:3120} : Ring a} -> neg (m + n) = neg m + neg n
  Totality: total
  Visibility: export
0 multOneRightNeutral : {auto {conArg:3495} : Ring a} -> n * 1 = n
  `n * 1 === n` for all `n : a`.

  Totality: total
  Visibility: export
0 multZeroRightAbsorbs : {auto {conArg:3585} : Ring a} -> n * 0 = 0
  Zero is an absorbing element of multiplication.

  Totality: total
  Visibility: export
0 multZeroLeftAbsorbs : {auto {conArg:3743} : Ring a} -> 0 * n = 0
  Zero is an absorbing element of multiplication.

  Totality: total
  Visibility: export
0 multZeroAbsorbs : {auto {conArg:3845} : Ring a} -> Either (m = 0) (n = 0) -> m * n = 0
  Zero is an absorbing element of multiplication.

  Totality: total
  Visibility: export
0 multNegRight : {auto {conArg:4055} : Ring a} -> m * neg n = neg (m * n)
  `m * (-n) = - (m * n)`.

  Totality: total
  Visibility: export
0 negMultNegRight : {auto {conArg:4225} : Ring a} -> neg (m * neg n) = m * n
  `- (m * (-n)) = m * n`.

  Totality: total
  Visibility: export
0 multNegLeft : {auto {conArg:4348} : Ring a} -> neg m * n = neg (m * n)
  `(- m) * n = - (m * n)`.

  Totality: total
  Visibility: export
0 negMultNegLeft : {auto {conArg:4496} : Ring a} -> neg (neg m * n) = m * n
  `- ((-m) * n) = m * n`.

  Totality: total
  Visibility: export
0 multMinusOneRight : {auto {conArg:4619} : Ring a} -> n * neg 1 = neg n
  Multiplication with `(-1)` is negation.

  Totality: total
  Visibility: export
0 multMinusOneLeft : {auto {conArg:4740} : Ring a} -> neg 1 * n = neg n
  Multiplication with `(-1)` is negation.

  Totality: total
  Visibility: export
0 negMultNeg : {auto {conArg:4861} : Ring a} -> neg m * neg n = m * n
  Multiplication of two negations removes negations.

  Totality: total
  Visibility: export
0 rightDistributive : {auto {conArg:5014} : Ring a} -> (m + n) * k = (m * k) + (n * k)
  Multiplication is distributive with respect to addition.

  Totality: total
  Visibility: export
0 multPlusSelf : {auto {conArg:5262} : Ring a} -> (m * n) + m = m * (n + 1)
  Totality: total
  Visibility: export