Commit 2024-07-11 16:02 82487ba2
View on Github →chore(RingTheory/AdicCompletion): manual instances (#14534)
Instead of inferring AddCommGroup, Module, etc. instances for AdicCompletion I M from being a submodule, we explicitly spell out the definitions to improve performance.
Also marks some definitions as noncomputable to save time spent on compilation.
See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Adic.20completion.20is.20slow.