/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Algebra.Order.Ring.Nat
public import Mathlib.Algebra.Order.Star.Basic
public import Mathlib.Data.Nat.PrimeFin
public meta import Mathlib.Data.Nat.PrimeFin@[expose] public sectionnamespace NatA natural number $n$ is said to be $k$-full (or $k$-powerful) if for every prime factor $p$ of $n$, the $k$-th power $p^k$ also divides $n$.
def Full (k : ℕ) (n : ℕ) : Prop := ∀ p ∈ n.primeFactors, p^k ∣ ninstance Full.decide : ∀ k n, Decidable (Full k n) := ⊢ (k n : ℕ) → Decidable (k.Full n)
k:ℕn:ℕ⊢ Decidable (k.Full n)
k:ℕn:ℕ⊢ Decidable (∀ p ∈ n.primeFactors, p ^ k ∣ n)
All goals completed! 🐙Every natural number is $0$-full.
theorem Full.zero_left (n : ℕ) : (0 : ℕ).Full n := n:ℕ⊢ Full 0 n
All goals completed! 🐙Every natural number is $1$-full.
theorem Full.one_left (n : ℕ) : (1 : ℕ).Full n := n:ℕ⊢ Full 1 n
All goals completed! 🐙$0$ is always $k$-full.
theorem Full.zero_right (k : ℕ) : k.Full 0 := k:ℕ⊢ k.Full 0
All goals completed! 🐙$1$ is always $k$-full.
theorem Full.one_right (k : ℕ) : k.Full 1 := k:ℕ⊢ k.Full 1
All goals completed! 🐙A Powerful number is a natural number $n$ where for every prime divisor $p$, $p^2$ divides $n$. Powerful numbers are also known as "squareful", "square-full", or "$2$-full".
abbrev Powerful : ℕ → Prop := (2).Fullinstance Powerful.decide : ∀ n, Decidable (Powerful n) := ⊢ (n : ℕ) → Decidable n.Powerful
n:ℕ⊢ Decidable n.Powerful
n:ℕ⊢ Decidable (∀ p ∈ n.primeFactors, p ^ 2 ∣ n)
All goals completed! 🐙theorem full_of_le_full (k : ℕ) (n : ℕ) {m : ℕ} (hk : k ≤ m) (h : m.Full n) : k.Full n :=
fun p a ↦ pow_dvd_of_le_of_pow_dvd hk (h p a)If $n \equiv p \pmod{p ^ (k + 1)}$, for a prime $p$ then $n$ is not $(k + 1)$-full.
n:ℕk:ℕp:ℕhp:Prime ph:n % p ^ (k + 1) = pthis:p ∣ p ^ (k + 1)⊢ p ∣ p ^ (k + 1) * (n / p ^ (k + 1)) + p ∧ ¬p ^ (k + 1) * (n / p ^ (k + 1)) + p = 0
n:ℕk:ℕp:ℕhp:Prime ph:n % p ^ (k + 1) = pthis:p ∣ p ^ (k + 1)⊢ p ∣ p ^ (k + 1) * (n / p ^ (k + 1)) ∧ (p = 0 ∨ n < p ^ (k + 1) → ¬p = 0)
All goals completed! 🐙
n:ℕk:ℕp:ℕhp:Prime ph:n % p ^ (k + 1) = p⊢ ¬p ^ (k + 1) ∣ n n:ℕk:ℕp:ℕhp:Prime ph✝:n % p ^ (k + 1) = ph:p ^ (k + 1) ∣ n⊢ False
n:ℕk:ℕp:ℕhp:Prime ph✝:0 = ph:p ^ (k + 1) ∣ n⊢ False
All goals completed! 🐙open Lean Meta Qq in
Simproc to compute the set Nat.primeFactors.
dsimproc primeFactorsEq (Nat.primeFactors _) := fun e ↦ do
unless e.isAppOfArity `Nat.primeFactors 1 do return .continue
let some n ← Lean.Nat.fromExpr? e.appArg! | return .continue
let outAsList : List Q(ℕ) := (unsafe n.primeFactors.val.unquot).map mkNatLit
let outAsFinset : Q(Finset ℕ) := outAsList.foldl (fun s n ↦ q(insert $n $s)) q({})
return .done outAsFinset