mathlib3

6f6739f8 - chore(algebra/star/basic): split out `big_operators` import (#17792)

chore(algebra/star/basic): split out `big_operators` import (#17792) cf https://github.com/leanprover-community/mathlib/pull/17772#issuecomment-1334662059, cc @eric-wieser