Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-16 01:14 b13c1a07

View on Github →

feat(number_theory/divisors): add nat.cons_self_proper_divisors (#18176)

Rename nat.divisors_eq_proper_divisors_insert_self_of_pos to nat.insert_self_proper_divisors, assume n ≠ 0 instead of 0 < n and swap LHS with RHS.
Add nat.cons_self_proper_divisors. This is easier to use with finset.prod_cons/finset.sum_cons.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.erase_cons_of_ne

Modified src/group_theory/order_of_element.lean

modified theorem sum_card_order_of_eq_card_pow_eq_one

Modified src/group_theory/specific_groups/cyclic.lean

Modified src/number_theory/divisors.lean

added theorem nat.cons_self_proper_divisors

deleted theorem nat.divisors_eq_proper_divisors_insert_self_of_pos

added theorem nat.insert_self_proper_divisors

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

modified theorem polynomial.cyclotomic_coeff_zero

Modified src/ring_theory/polynomial/cyclotomic/eval.lean