Smooth number
IsSmoothdef
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 ≤ BFrom Mathlib
import Conjectura.Defs.Mathematics.NumberTheory.SmoothNumber · maintainer — open · raw source
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