Exponentiation of natural numbers

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elif Uskuplu.

Created on 2022-02-15.
Last modified on 2023-09-10.

module elementary-number-theory.exponentiation-natural-numbers where
Imports 
open import commutative-algebra.powers-of-elements-commutative-semirings

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.commutative-semiring-of-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.identity-types

Idea

The exponent m^n is the number obtained by multiplying m with itself n times.

Definition

exp-ℕ : ℕ → ℕ → ℕ
exp-ℕ m 0 = 1
exp-ℕ m (succ-ℕ n) = (exp-ℕ m n) *ℕ m

infixr 45 _^ℕ_
_^ℕ_ = exp-ℕ

power-ℕ : ℕ → ℕ → ℕ
power-ℕ = power-Commutative-Semiring ℕ-Commutative-Semiring

Properties

Tarski's high school arithmetic laws for exponentiation

annihilation-law-exp-ℕ : (n : ℕ) → 1 ^ℕ n ＝ 1
annihilation-law-exp-ℕ zero-ℕ = refl
annihilation-law-exp-ℕ (succ-ℕ n) =
  right-unit-law-mul-ℕ (1 ^ℕ n) ∙ annihilation-law-exp-ℕ n

left-distributive-exp-add-ℕ :
  (x y z : ℕ) → x ^ℕ (y +ℕ z) ＝ (x ^ℕ y) *ℕ (x ^ℕ z)
left-distributive-exp-add-ℕ x y zero-ℕ = inv (right-unit-law-mul-ℕ (x ^ℕ y))
left-distributive-exp-add-ℕ x y (succ-ℕ z) =
  ( ap (_*ℕ x) (left-distributive-exp-add-ℕ x y z)) ∙
  ( associative-mul-ℕ (x ^ℕ y) (x ^ℕ z) x)

right-distributive-exp-mul-ℕ :
  (x y z : ℕ) → (x *ℕ y) ^ℕ z ＝ (x ^ℕ z) *ℕ (y ^ℕ z)
right-distributive-exp-mul-ℕ x y zero-ℕ = refl
right-distributive-exp-mul-ℕ x y (succ-ℕ z) =
  ( ap (_*ℕ (x *ℕ y)) (right-distributive-exp-mul-ℕ x y z)) ∙
  ( interchange-law-mul-mul-ℕ (x ^ℕ z) (y ^ℕ z) x y)

exp-mul-ℕ : (x y z : ℕ) → x ^ℕ (y *ℕ z) ＝ (x ^ℕ y) ^ℕ z
exp-mul-ℕ x zero-ℕ z = inv (annihilation-law-exp-ℕ z)
exp-mul-ℕ x (succ-ℕ y) z =
  ( left-distributive-exp-add-ℕ x (y *ℕ z) z) ∙
  ( ( ap (_*ℕ (x ^ℕ z)) (exp-mul-ℕ x y z)) ∙
    ( inv (right-distributive-exp-mul-ℕ (x ^ℕ y) x z)))

The exponent m^n is always nonzero

is-nonzero-exp-ℕ :
  (m n : ℕ) → is-nonzero-ℕ m → is-nonzero-ℕ (m ^ℕ n)
is-nonzero-exp-ℕ m zero-ℕ p = is-nonzero-one-ℕ
is-nonzero-exp-ℕ m (succ-ℕ n) p =
  is-nonzero-mul-ℕ (m ^ℕ n) m (is-nonzero-exp-ℕ m n p) p

Recent changes