mathlib3

a2efed67 - chore(algebra/big_operators/part_enat): drop file (#17934)

chore(algebra/big_operators/part_enat): drop file (#17934) The only lemma in this file is a version of `nat.cast_sum`. Also fix an instance on `part_enat` so that `nat.cast_sum` works for this type.