# Powers of elements in commutative semirings

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Maša Žaucer.

Created on 2023-02-20.

module commutative-algebra.powers-of-elements-commutative-semirings where

Imports
open import commutative-algebra.commutative-semirings

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


## 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

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

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

module _
{l : Level} (A : Commutative-Semiring l)
where

(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)


### If x commutes with y, then powers distribute over the product of x and y

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)