Commit 2026-03-18 05:54 034c50cb

View on Github →

feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization (#34554)

Estimated changes

Modified Mathlib.lean

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

added theorem Nat.Iic_factorization_prod_pow_injective

added theorem Nat.Iio_factorization_prod_pow_injective

added theorem Nat.coe_divisors_eq_prod_pow_le_factorization

added theorem Nat.coe_properDivisors_eq_prod_pow_lt_factorization

added theorem Nat.divisors_eq_image_Iic_factorization_prod_pow

added theorem Nat.divisors_eq_map_attach_Iic_factorization_prod_pow

added theorem Nat.properDivisors_eq_image_Iio_factorization_prod_pow

added theorem Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow