Commit 2024-05-27 10:29 c6984f24

View on Github →

feat(NumberTheory/SmoothNumbers): multiplicativity (#13115) Prove that the product of two n-smooth numbers is an n-smooth number. Uses two helper lemmas.

Estimated changes

Modified Mathlib/NumberTheory/SmoothNumbers.lean

added theorem Nat.mem_factoredNumbers_iff_primeFactors_subset

added theorem Nat.mem_factoredNumbers_of_primeFactors_subset

added theorem Nat.mem_smoothNumbers_iff_primeFactors_subset

added theorem Nat.mem_smoothNumbers_of_primeFactors_subset

added theorem Nat.mul_mem_factoredNumbers

added theorem Nat.mul_mem_smoothNumbers

added theorem Nat.primeFactors_subset_of_mem_factoredNumbers

added theorem Nat.primeFactors_subset_of_mem_smoothNumbers

added theorem Nat.smmoothNumbers_eq_factoredNumbers_primesBelow