Mathlib Map

Theorems · Definition · field theory

AbsoluteValue.Completion

{K : Type u_1} → [inst : Field K] → AbsoluteValue K ℝ → Type u_1

The completion of a field with respect to a real absolute value.

Defined in
Mathlib.Analysis.Normed.Field.WithAbs
Cited by
24 results in Mathlib
Foundations
Depth 129 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.ext · cited by 8Completion.extNumberField.InfinitePlace.Completion.continuous_ofCompletion · cited by 4Completion.continuous_ofC…NumberField.InfinitePlace.Completion.equivCompletion · cited by 4Completion.equivCompletionNumberField.InfinitePlace.Completion.isometry_toCompletion · cited by 3Completion.isometry_toCom…NumberField.InfinitePlace.Completion.equiv · cited by 2Completion.equivNumberField.InfinitePlace.Completion.algebraMap_toCompletion · cited by 1Completion.algebraMap_toC…NumberField.InfinitePlace.Completion.casesOn · cited by 1Completion.casesOnNumberField.InfinitePlace.Completion.continuous_toCompletion · cited by 1Completion.continuous_toC…NumberField.InfinitePlace.Completion.isometryEquivCompletion · cited by 1Completion.isometryEquivC…NumberField.InfinitePlace.Completion.ofCompletion_surjective · cited by 1Completion.ofCompletion_s…NumberField.InfinitePlace.Completion.ofCompletion.inj · cited by 1ofCompletion.injNumberField.InfinitePlace.Completion.ofCompletion.noConfusion · cited by 1ofCompletion.noConfusionNumberField.InfinitePlace.Completion.algebraMap_eq_coe · cited by 1Completion.algebraMap_eq_…NumberField.InfinitePlace.Completion.coe_toCompletion · cited by 0Completion.coe_toCompleti…Real · cited by 25697RealField · cited by 7404FieldAbsoluteValue · cited by 363AbsoluteValueUniformSpace.Completion · cited by 192UniformSpace.CompletionWithAbs · cited by 102WithAbsAbsoluteValue.CompletionCITED BYCITES

Cites5

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

Cited by33

Results whose statement or proof uses this declaration.