Commit 2026-03-19 03:44 38d2f28a

View on Github →

feat(Data/Nat/Factorization/Defs): more theorems about f.prod (· ^ ·) (#36792)

Estimated changes

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

deleted theorem Nat.eq_factorization_iff

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

added theorem Nat.dvd_iff_exists_le_factorization

added theorem Nat.dvd_prod_pow_of_factorization_le

added theorem Nat.eq_factorization_iff

modified def Nat.factorizationEquiv

added theorem Nat.factorization_prod_pow_eq_self_of_le_factorization

added theorem Nat.prod_pow_dvd_of_le_factorization

modified theorem Nat.prod_pow_factorization_eq_self

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

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

Modified Mathlib/Tactic/NormNum/Irrational.lean