Theorem Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow

Modification history

2026-03-18 05:54
Mathlib/Data/Nat/Factorization/Divisors.lean
feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization (#34554)
Added Nat.properDivisors_eq_map_attach_Iio_factorization_prod_powView on Github →