def Nat.Full (k n : ℕ) : Prop

A 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$.

Equations

• k.Full n = ∀ p ∈ n.primeFactors, p ^ k ∣ n

instance Nat.Full.decide (k n : ℕ) : Decidable (k.Full n)

Equations

• Nat.Full.decide k n = id inferInstance

@[reducible, inline]

abbrev Nat.Powerful : ℕ → Prop

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".

Equations

• Nat.Powerful = Nat.Full 2

instance Nat.Powerful.decide (n : ℕ) : Decidable n.Powerful

Equations

• Nat.Powerful.decide n = id Finset.decidableDforallFinset

theorem Nat.full_of_le_full (k n : ℕ) {m : ℕ} (hk : k ≤ m) (h : m.Full n) : k.Full n

theorem Nat.not_full_of_prime_mod_prime_sq (n k : ℕ) {p : ℕ} (hp : Prime p) (h : n % p ^ (k + 1) = p) : ¬(k + 1).Full n

If $n \equiv p \pmod{p ^ (k + 1)}$, for a prime $p$ then $n$ is not $(k + 1)$-full.

def Nat.primeFactorsEq : Lean.Meta.Simp.DSimproc

Simproc to compute the set Nat.primeFactors.

Equations

• One or more equations did not get rendered due to their size.