Cubes of natural numbers

Content created by Egbert Rijke.

Created on 2023-12-06.
Last modified on 2024-01-28.

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

See also

Recent changes