[Merged by Bors] - refactor(NumberTheory): make InfinitePlace.Completion a one-field structure#41543

smmercuri wants to merge 5 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

smmercuri:Completion-one-fieldsmmercuri/mathlib4:Completion-one-fieldCopy head branch name to clipboard