Square-free natural numbers

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Alec Barreto and Nathan van Doorn.

Created on 2022-03-15.
Last modified on 2023-09-24.

module elementary-number-theory.square-free-natural-numbers where
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.squares-natural-numbers

open import foundation.universe-levels


A natural number n is said to be square-free if x² | n ⇒ x = 1 for any natural number x.


is-square-free-ℕ :   UU lzero
is-square-free-ℕ n = (x : )  div-ℕ (square-ℕ x) n  is-one-ℕ x

Recent changes