Theorem NumberField.LiesOver.continuous_completionMap

Modification history

2026-09-28 09:24
Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean
chore: make `adicCompletion` and `Completion` print nicer (#41702) …
Modified NumberField.LiesOver.continuous_completionMapView on Github →
2026-07-13 08:45
Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean
refactor(NumberTheory): make `InfinitePlace.Completion` a one-field structure (#41543) …
Added NumberField.LiesOver.continuous_completionMapView on Github →