Algebra.Solver.Ring.Prod

Reexports

Definitions

eprod : Ring a => Prod a as -> a

  Evaluate products of variables each raised to
  given exponent.
  
  Every arithmetic expression in a commutative ring
  can be represented as a sum of products of the variables
  each raised by an exponent and multiplied by a constant
  factor. For instance, expression `x + x * (y + z + z)`
  gets normalized to `x + x * y + 2 * x * z`.

Totality: total
Visibility: public export

0 pone : {auto {conArg:856} : Ring a} -> (as : List a) -> eprod one = 1

  Proof that `one` evaluates to 1.

Totality: total
Visibility: export

0 pvar : {auto {conArg:983} : Ring a} -> (as : List a) -> (e : Elem x as) -> eprod (fromVar e) = x

  Proof that `fromVar x` evaluates to `x`.

Totality: total
Visibility: export

0 pmult : {auto {conArg:1241} : Ring a} -> (p : Prod a as) -> (q : Prod a as) -> eprod (mult p q) = eprod p * eprod q

  Proof that evaluation of a multiplication of products
  is the same as multiplying the results of evaluating each
  of them.

Totality: total
Visibility: export