# Powers of elements in commutative semirings ```agda module commutative-algebra.powers-of-elements-commutative-semirings where ``` <details><summary>Imports</summary> ```agda open import commutative-algebra.commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.identity-types open import foundation.universe-levels open import ring-theory.powers-of-elements-semirings ``` </details> ## Idea The **power operation** on a commutative semiring is the map `n x ↦ xⁿ`, which is defined by iteratively multiplying `x` with itself `n` times. ## Definition ```agda power-Commutative-Semiring : {l : Level} (A : Commutative-Semiring l) → ℕ → type-Commutative-Semiring A → type-Commutative-Semiring A power-Commutative-Semiring A = power-Semiring (semiring-Commutative-Semiring A) ``` ## Properties ### `xⁿ⁺¹ = xⁿx` ```agda module _ {l : Level} (A : Commutative-Semiring l) where power-succ-Commutative-Semiring : (n : ℕ) (x : type-Commutative-Semiring A) → power-Commutative-Semiring A (succ-ℕ n) x = mul-Commutative-Semiring A (power-Commutative-Semiring A n x) x power-succ-Commutative-Semiring = power-succ-Semiring (semiring-Commutative-Semiring A) ``` ### Powers by sums of natural numbers are products of powers ```agda module _ {l : Level} (A : Commutative-Semiring l) where distributive-power-add-Commutative-Semiring : (m n : ℕ) {x : type-Commutative-Semiring A} → power-Commutative-Semiring A (m +ℕ n) x = mul-Commutative-Semiring A ( power-Commutative-Semiring A m x) ( power-Commutative-Semiring A n x) distributive-power-add-Commutative-Semiring = distributive-power-add-Semiring (semiring-Commutative-Semiring A) ``` ### If `x` commutes with `y`, then powers distribute over the product of `x` and `y` ```agda module _ {l : Level} (A : Commutative-Semiring l) where distributive-power-mul-Commutative-Semiring : (n : ℕ) (x y : type-Commutative-Semiring A) → power-Commutative-Semiring A n (mul-Commutative-Semiring A x y) = mul-Commutative-Semiring A ( power-Commutative-Semiring A n x) ( power-Commutative-Semiring A n y) distributive-power-mul-Commutative-Semiring n x y = distributive-power-mul-Semiring ( semiring-Commutative-Semiring A) ( n) ( commutative-mul-Commutative-Semiring A x y) ```