Commit 2022-12-14 08:46 a2efed67
View on Github →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.
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.