Mathlib Map

Theorems · Inductive type · number theory

NumberField.InfinitePlace.Completion

{K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → Type u_1

The completion of a number field at an infinite place, as a one-field structure wrapping the completion v.1.Completion of K at the underlying absolute value.

Defined in
Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Cited by
69 results in Mathlib
Foundations
Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Field
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NumberField.InfinitePlace.Completion.toCompletion · cited by 20Completion.toCompletionNumberField.InfinitePlace.Completion.extensionEmbedding · cited by 15Completion.extensionEmbed…NumberField.InfiniteAdeleRing · cited by 10NumberField.InfiniteAdele…NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal · cited by 9Completion.extensionEmbed…NumberField.InfinitePlace.Completion.ext · cited by 8Completion.extNumberField.InfinitePlace.Completion.extensionEmbedding_coe · cited by 5Completion.extensionEmbed…NumberField.InfinitePlace.inertiaDeg · cited by 5InfinitePlace.inertiaDegNumberField.LiesOver.completionMap · cited by 4LiesOver.completionMapNumberField.InfinitePlace.Completion.continuous_ofCompletion · cited by 4Completion.continuous_ofC…NumberField.InfinitePlace.Completion.equivCompletion · cited by 4Completion.equivCompletionNumberField.InfinitePlace.Completion.isometry_extensionEmbedding · cited by 4Completion.isometry_exten…NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex · cited by 4Completion.ringEquivCompl…NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal · cited by 4Completion.ringEquivRealO…NumberField.InfinitePlace.Completion.induction_on · cited by 3Completion.induction_onNumberField.InfinitePlace.Completion.isometry_toCompletion · cited by 3Completion.isometry_toCom…Field · cited by 7404FieldNumberField.InfinitePlace · cited by 604NumberField.InfinitePlaceInfinitePlace.CompletionCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by89

Results whose statement or proof uses this declaration.