Theorem Nat.mem_factoredNumbers_iff_primeFactors_subset

Modification history

2024-05-27 10:29
Mathlib/NumberTheory/SmoothNumbers.lean
feat(NumberTheory/SmoothNumbers): multiplicativity (#13115) …
Added Nat.mem_factoredNumbers_iff_primeFactors_subsetView on Github →