Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.eq_proper_divisors_of_subset_of_sum_eq_sum

Modification history