Smooth number

Conjectura.Defs.Mathematics.NumberTheory.SmoothNumber

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Nat.Factorization.PrimePow

/-! # Smooth number -/

namespace Conjectura.NumberTheory

/-- A number is **B-smooth** when all of its prime factors are at most `B`. Smoothness controls
the running time of factoring and discrete-logarithm algorithms, which is why the notion sits
at the boundary of number theory and cryptography. -/
def IsSmooth (B n : ℕ) : Prop := ∀ p ∈ n.primeFactors, p ≤ B

end Conjectura.NumberTheory