Powers of integers

Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke and Gregor Perčič.

Created on 2023-02-20.
Last modified on 2023-09-21.

module elementary-number-theory.powers-integers where
Imports 
open import commutative-algebra.powers-of-elements-commutative-rings

open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.ring-of-integers

open import foundation.identity-types

Idea

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

Definition

power-ℤ : ℕ → ℤ → ℤ
power-ℤ = power-Commutative-Ring ℤ-Commutative-Ring

Properties

xⁿ⁺¹ = xⁿx

power-succ-ℤ : (n : ℕ) (x : ℤ) → power-ℤ (succ-ℕ n) x ＝ (power-ℤ n x) *ℤ x
power-succ-ℤ = power-succ-Commutative-Ring ℤ-Commutative-Ring

Recent changes