mathlib

05c491cd - feat(big_operators): single out one term from prod (#7040)