Def NumberField.InfinitePlace.Completion.extensionEmbedding

Modification history

2024-12-07 04:52

Mathlib/NumberTheory/NumberField/Completion.lean

chore(Mathlib/NumberTheory/NumberField/*): rename completion -> Completion (#19646) …

Modified NumberField.InfinitePlace.Completion.extensionEmbedding View on Github →

2024-11-08 12:39

Mathlib/NumberTheory/NumberField/Completion.lean

feat: the completion of a number field at an infinite place (#16483) …

Added NumberField.InfinitePlace.Completion.extensionEmbedding View on Github →