Theorem Nat.coe_divisors_eq_prod_pow_le_factorization

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.coe_divisors_eq_prod_pow_le_factorizationView on Github →