# Powers of elements in commutative rings

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

Created on 2023-02-20.

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

Imports
open import commutative-algebra.commutative-rings

open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.parity-natural-numbers

open import foundation.identity-types
open import foundation.universe-levels

open import ring-theory.powers-of-elements-rings


## Idea

The power operation on a commutative ring is the map n x ↦ xⁿ, which is defined by iteratively multiplying x with itself n times.

## Definition

power-Commutative-Ring :
{l : Level} (A : Commutative-Ring l) →
ℕ → type-Commutative-Ring A → type-Commutative-Ring A
power-Commutative-Ring A = power-Ring (ring-Commutative-Ring A)


## Properties

### xⁿ⁺¹ = xⁿx and xⁿ⁺¹ ＝ xxⁿ

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

power-succ-Commutative-Ring :
(n : ℕ) (x : type-Commutative-Ring A) →
power-Commutative-Ring A (succ-ℕ n) x ＝
mul-Commutative-Ring A (power-Commutative-Ring A n x) x
power-succ-Commutative-Ring =
power-succ-Ring (ring-Commutative-Ring A)

power-succ-Commutative-Ring' :
(n : ℕ) (x : type-Commutative-Ring A) →
power-Commutative-Ring A (succ-ℕ n) x ＝
mul-Commutative-Ring A x (power-Commutative-Ring A n x)
power-succ-Commutative-Ring' =
power-succ-Ring' (ring-Commutative-Ring A)


### Powers by sums of natural numbers are products of powers

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

(m n : ℕ) {x : type-Commutative-Ring A} →
power-Commutative-Ring A (m +ℕ n) x ＝
mul-Commutative-Ring A
( power-Commutative-Ring A m x)
( power-Commutative-Ring A n x)


### Powers by products of natural numbers are iterated powers

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

power-mul-Commutative-Ring :
(m n : ℕ) {x : type-Commutative-Ring A} →
power-Commutative-Ring A (m *ℕ n) x ＝
power-Commutative-Ring A n (power-Commutative-Ring A m x)
power-mul-Commutative-Ring =
power-mul-Ring (ring-Commutative-Ring A)


### Powers distribute over multiplication

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

distributive-power-mul-Commutative-Ring :
(n : ℕ) (x y : type-Commutative-Ring A) →
power-Commutative-Ring A n (mul-Commutative-Ring A x y) ＝
mul-Commutative-Ring A
( power-Commutative-Ring A n x)
( power-Commutative-Ring A n y)
distributive-power-mul-Commutative-Ring n x y =
distributive-power-mul-Ring
( ring-Commutative-Ring A)
( n)
( commutative-mul-Commutative-Ring A x y)


### (-x)ⁿ = (-1)ⁿxⁿ

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

power-neg-Commutative-Ring :
(n : ℕ) (x : type-Commutative-Ring A) →
power-Commutative-Ring A n (neg-Commutative-Ring A x) ＝
mul-Commutative-Ring A
( power-Commutative-Ring A n (neg-one-Commutative-Ring A))
( power-Commutative-Ring A n x)
power-neg-Commutative-Ring =
power-neg-Ring (ring-Commutative-Ring A)

even-power-neg-Commutative-Ring :
(n : ℕ) (x : type-Commutative-Ring A) →
is-even-ℕ n →
power-Commutative-Ring A n (neg-Commutative-Ring A x) ＝
power-Commutative-Ring A n x
even-power-neg-Commutative-Ring =
even-power-neg-Ring (ring-Commutative-Ring A)

odd-power-neg-Commutative-Ring :
(n : ℕ) (x : type-Commutative-Ring A) →
is-odd-ℕ n →
power-Commutative-Ring A n (neg-Commutative-Ring A x) ＝
neg-Commutative-Ring A (power-Commutative-Ring A n x)
odd-power-neg-Commutative-Ring =
odd-power-neg-Ring (ring-Commutative-Ring A)