Power-free integers

DefinitionPower-free natural numbers#✓fully proved

Let \(k\) be a natural number. A natural number \(n\) is \(k\)-free when \(k \ge 2\), \(n > 0\), and \(p^k\) does not divide \(n\) for any prime \(p\).

def IsPowerFree (n k : ℕ) : Prop :=
  2 ≤ k ∧ 0 < n ∧ ∀ p : ℕ, p.Prime → ¬p ^ k ∣ n

Used by 14

Used byOdd-to-even ratio of \(k\)-full, \(l\)-free numbers · Odd-to-even ratio of \(l\)-free numbers · Characterization of power-free numbers · A natural number is 2-free if and only if it is squarefree · Power-freeness is monotone in the exponent · A k-free number has no prime k-th power divisor · Divisors of k-free numbers are k-free · Power-free numbers are positive · The exponent of a power-free number is at least two · Finitely many Brocard–Ramanujan solutions of polynomial shape · Brocard–Ramanujan solutions with \(x - 1\) or \(x + 1\) power-free are finite · Brocard–Ramanujan solutions with \(x - 1\) or \(x + 1\) seven-free · Petrow–Young Weyl bound on the critical line · Petrow–Young Weyl bound for central values

TheoremCharacterization of power-free numbers#✓fully proved

For natural numbers \(n\) and \(k\), \(n\) is \(k\)-free if and only if \(k \ge 2\), \(n > 0\), and \(p^k\) does not divide \(n\) for any prime \(p\).

theorem isPowerFree_iff {n k : ℕ} :
    n.IsPowerFree k ↔ 2 ≤ k ∧ 0 < n ∧ ∀ p : ℕ, p.Prime → ¬p ^ k ∣ n

Uses 1

Statement usesPower-free natural numbers

TheoremThe exponent of a power-free number is at least two#✓fully proved

If a natural number \(n\) is \(k\)-free, then \(k \ge 2\).

theorem IsPowerFree.two_le {n k : ℕ} (h : n.IsPowerFree k) : 2 ≤ k

Uses 1 · Used by 2

Statement usesPower-free natural numbers

Used byPower-freeness is monotone in the exponent · Divisors of k-free numbers are k-free

TheoremPower-free numbers are positive#✓fully proved

If a natural number \(n\) is \(k\)-free, then \(n > 0\).

theorem IsPowerFree.pos {n k : ℕ} (h : n.IsPowerFree k) : 0 < n

Uses 1 · Used by 2

Statement usesPower-free natural numbers

Used byPower-freeness is monotone in the exponent · Divisors of k-free numbers are k-free

TheoremA k-free number has no prime k-th power divisor#✓fully proved

If a natural number \(n\) is \(k\)-free and \(p\) is a prime, then \(p^k\) does not divide \(n\).

theorem IsPowerFree.not_dvd {n k p : ℕ} (h : n.IsPowerFree k)
    (hp : p.Prime) : ¬p ^ k ∣ n

Uses 1 · Used by 3

Statement usesPower-free natural numbers

Used byA natural number is 2-free if and only if it is squarefree · Power-freeness is monotone in the exponent · Divisors of k-free numbers are k-free

TheoremDivisors of k-free numbers are k-free#✓fully proved

If a natural number \(n\) is \(k\)-free and \(m\) divides \(n\), then \(m\) is \(k\)-free.

theorem IsPowerFree.of_dvd {m n k : ℕ} (h : n.IsPowerFree k)
    (hmn : m ∣ n) : m.IsPowerFree k

Uses 4

Statement usesPower-free natural numbers

Proof usesA k-free number has no prime k-th power divisor · Power-free numbers are positive · The exponent of a power-free number is at least two

TheoremPower-freeness is monotone in the exponent#✓fully proved

If a natural number \(n\) is \(k\)-free and \(k \le l\), then \(n\) is \(l\)-free.

theorem IsPowerFree.mono {n k l : ℕ} (h : n.IsPowerFree k)
    (hkl : k ≤ l) : n.IsPowerFree l

Uses 4

Statement usesPower-free natural numbers

Proof usesA k-free number has no prime k-th power divisor · Power-free numbers are positive · The exponent of a power-free number is at least two

TheoremA natural number is 2-free if and only if it is squarefree#✓fully proved

For every natural number \(n\), \(n\) is \(2\)-free if and only if \(n\) is squarefree, that is, \(d^2\) divides \(n\) only for \(d = 1\).

theorem isPowerFree_two {n : ℕ} : n.IsPowerFree 2 ↔ Squarefree n

Uses 2

Statement usesPower-free natural numbers

Proof usesA k-free number has no prime k-th power divisor

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.