Algebra.Semiring

Definitions

interface Semiring : Type -> Type

  This interface is a witness that for a
  numeric type `a` the axioms of a commutative semiring hold:
  
  1. `a` is a commutative monoid 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`.
  
  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`.
  

Parameters: a
Constraints: Num 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 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 multZeroLeftAbsorbs : 0 * n = 0

  Zero is an absorbing element of multiplication.

Implementation: 

Semiring Nat

0 plusAssociative : {auto __con : Semiring a} -> k + (m + n) = (k + m) + n

  Addition is associative.

Totality: total
Visibility: public export

0 plusCommutative : {auto __con : Semiring a} -> m + n = n + m

  Addition is commutative.

Totality: total
Visibility: public export

0 plusZeroLeftNeutral : {auto __con : Semiring a} -> 0 + n = n

  0 is the additive identity.

Totality: total
Visibility: public export

0 multAssociative : {auto __con : Semiring a} -> k * (m * n) = (k * m) * n

  Multiplication is associative.

Totality: total
Visibility: public export

0 multCommutative : {auto __con : Semiring a} -> m * n = n * m

  Multiplication is commutative.

Totality: total
Visibility: public export

0 multOneLeftNeutral : {auto __con : Semiring a} -> 1 * n = n

  1 is the multiplicative identity.

Totality: total
Visibility: public export

0 leftDistributive : {auto __con : Semiring a} -> k * (m + n) = (k * m) + (k * n)

  Multiplication is distributive with respect to addition.

Totality: total
Visibility: public export

0 multZeroLeftAbsorbs : {auto __con : Semiring a} -> 0 * n = 0

  Zero is an absorbing element of multiplication.

Totality: total
Visibility: public export

0 plusZeroRightNeutral : {auto {conArg:1382} : Semiring a} -> n + 0 = n

  `n + 0 === n` for all `n : a`.

Totality: total
Visibility: export

0 multOneRightNeutral : {auto {conArg:1462} : Semiring a} -> n * 1 = n

  `n * 1 === n` for all `n : a`.

Totality: total
Visibility: export

0 multZeroRightAbsorbs : {auto {conArg:1542} : Semiring a} -> n * 0 = 0

  Zero is an absorbing element of multiplication.

Totality: total
Visibility: export

multZeroAbsorbs : {auto {conArg:1629} : Semiring a} -> (m : a) -> (n : a) -> Either (m = 0) (n = 0) -> m * n = 0

  Zero is an absorbing element of multiplication.

Totality: total
Visibility: export

0 rightDistributive : {auto {conArg:1803} : Semiring a} -> (m + n) * k = (m * k) + (n * k)

  Multiplication is distributive with respect to addition.

Totality: total
Visibility: export