Commit 2026-11-10 13:06 6dab8781

refactor: make InfinitePlace.Completion an abbrev (#45508) #41543 turned InfinitePlace.Completion from an abbrev into a one-field structure around AbsoluteValue.Completion to improve performance. #45407 made AbsoluteValue.Completion a one-field structure around UniformSpace.Completion, so now InfinitePlace.Completion can become an abbrev again and inherit the abstract theory of AbsoluteValue.Completion (for example LiesOverInstances.lean can now be deprecated). This PR also reverts an instance hack introduced in #45407 to resolve a diamond and instead fixes it by using equivAux instead of equiv in the transfer instances of NormedField and Algebra for AbsoluteValue.Completion. Tests are included in MathlibTest to show that the nsmul and zsmul diamonds remain fixed.