		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Pow-by-alpha

Raise a field element to the \alpha power.

Signature
(pow-by-alpha elem alpha prime) → new-elem
Arguments: elem — Guard (fep elem prime).; alpha — Guard (integerp alpha).; prime — Guard (primep prime).
Returns: new-elem — Type (fep new-elem prime), given (primep prime).

If the exponent is negative, we map 0 to 0 and we map non-zero elements to the inverses of their positive powers. Note that raising a non-zero field element to a power yields a non-zero element.

Definitions and Theorems

Function: pow-by-alpha

(defun pow-by-alpha (elem alpha prime)
  (declare (xargs :guard (and (integerp alpha)
                              (primep prime)
                              (fep elem prime))))
  (let ((__function__ 'pow-by-alpha))
    (declare (ignorable __function__))
    (if (< alpha 0)
        (if (= elem 0)
            0
          (inv (pow elem (- alpha) prime) prime))
      (pow elem alpha prime))))

Theorem: fep-of-pow-by-alpha

(defthm fep-of-pow-by-alpha
  (implies (primep prime)
           (b* ((new-elem (pow-by-alpha elem alpha prime)))
             (fep new-elem prime)))
  :rule-classes :rewrite)