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

Idea

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

Definition

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

Recent changes

• 2023-09-24. Alec Barreto. The Legendre symbol (#796).
• 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
• 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).