Powers of integers
Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke, Louis Wasserman and Gregor Perčič.
Created on 2023-02-20.
Last modified on 2025-10-14.
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
External links
- Exponentiation at Wikidata
Recent changes
- 2025-10-14. Louis Wasserman. Refactor the natural numbers and integers up to present code standards (#1568).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).