Def NumberField.InfinitePlace.Completion.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.toCompletion View on Github →