Theorem Nat.coe_properDivisors_eq_prod_pow_lt_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_properDivisors_eq_prod_pow_lt_factorizationView on Github →