mathlib

081cb8ab - chore(algebra/associated): split off dependencies of `big_operators` (#10848)

chore(algebra/associated): split off dependencies of `big_operators` (#10848) This prepares for the replacement of `nat.prime` with `_root_.prime` by reducing the amount of dependencies needed to define `_root_.prime`. Note that there wouldn't be an import loop without this change, just that `data/nat/prime.lean` would have a bigger amount of imports. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nat.2Eprime Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>