Theorem NumberField.InfinitePlace.Completion.ofCompletion_toCompletion

Modification history

2026-07-13 08:45
Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
refactor(NumberTheory): make `InfinitePlace.Completion` a one-field structure (#41543) …
Added NumberField.InfinitePlace.Completion.ofCompletion_toCompletionView on Github →