    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Exponentiation defined over a commutative semiring as repeated multiplication
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Algebra.Bundles using (CommutativeSemiring)

    module Algebra.Properties.CommutativeSemiring.Exp
      {a ℓ} (S : CommutativeSemiring a ℓ) where

    open CommutativeSemiring S
    import Algebra.Properties.CommutativeMonoid.Mult *-commutativeMonoid as Mult

    ------------------------------------------------------------------------
    -- Definition

    open import Algebra.Properties.Semiring.Exp semiring public

    ------------------------------------------------------------------------
    -- Properties

    ^-distrib-* : ∀ x y n → (x * y) ^ n ≈ x ^ n * y ^ n
    ^-distrib-* = Mult.×-distrib-+