Commit 2026-09-07 15:38 5a548ade

View on Github →

feat(Data/Nat/Factorization/Basic): add mul_factorization_le (#43477) Give a mildly tighter upper bound compared to factorization_lt

Estimated changes

Modified Mathlib/Data/Nat/Factorization/Basic.lean

added theorem Nat.mul_factorization_le

Modified Mathlib/Data/Nat/Factorization/Defs.lean

added theorem Nat.factorization_le_padicValNat

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

added theorem mul_padicValNat_le