Theorem NumberField.InfinitePlace.Completion.equivCompletion_symm_apply_toCompletion

Modification history

2026-11-10 13:06
Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
refactor: make `InfinitePlace.Completion` an `abbrev` (#45508) …
Added NumberField.InfinitePlace.Completion.equivCompletion_symm_apply_toCompletionView on Github →