Completion

📁 Source: Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean

Statistics

Metric	Count
Definitions Completion	1
Theorems	0
Total	1

NumberField.InfinitePlace

Definitions

Name	Category	Theorems
Completion 📖	CompOp	20 math math: Completion.isometry_extensionEmbeddingOfIsReal, Completion.surjective_extensionEmbedding_of_isComplex, Completion.isometry_extensionEmbedding, Completion.locallyCompactSpace, Completion.isClosed_image_extensionEmbedding, Completion.extensionEmbeddingOfIsReal_coe, Completion.isClosed_image_extensionEmbeddingOfIsReal, Completion.instIsTopologicalRing, Completion.extensionEmbedding_coe, Completion.extensionEmbeddingOfIsReal_apply, Completion.bijective_extensionEmbeddingOfIsReal, Completion.bijective_extensionEmbedding_of_isComplex, Completion.algebraMap_coe, LiesOver.extensionEmbedding_liesOver_of_isReal, Completion.surjective_extensionEmbeddingOfIsReal, Completion.liesOver_extensionEmbedding, NumberField.InfiniteAdeleRing.norm_def, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, Completion.Rat.norm_infinitePlace_completion, Completion.liesOver_conjugate_extensionEmbedding

---

← Back to Index