Commit 2024-07-13 00:30 c6a93595

View on Github →

chore(BigOperators/Ring): generalize Fintype.sum_mul_sum (#14683) Moving the lemma generalizes the typeclass assumptions from [CommSemiring α] to [NonUnitalNonAssocSemiring α].

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

modified theorem Fintype.sum_mul_sum