This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Cubes of natural numbers
module elementary-number-theory.cubes-natural-numbers where
Imports
open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.squares-natural-numbers open import foundation.dependent-pair-types open import foundation.fibers-of-maps open import foundation.universe-levels
Idea
The cube¶ n³ of a
natural number n is the triple
product
n³ := n * n * n
of n with itself.
Definitions
Cubes of natural numbers
cube-ℕ : ℕ → ℕ cube-ℕ n = square-ℕ n *ℕ n
The predicate of being a cube of natural numbers
is-cube-ℕ : ℕ → UU lzero is-cube-ℕ = fiber cube-ℕ
The cubic root of cubic natural numbers
cubic-root-ℕ : (n : ℕ) → is-cube-ℕ n → ℕ cubic-root-ℕ n = pr1