Commit 2021-12-17 10:49 081cb8ab
View on Github →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