mathlib
fa230957 - fix(algebra/big_operators): add missing `to_additive`s (#18878)

Commit

2 years ago

fix(algebra/big_operators): add missing `to_additive`s (#18878) These lemmas were written before `pi.mul_single` existed.

Author

eric-wieser

Parents