NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal

{K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.IsReal → v.Completion ≃ᵢ ℝ

If the infinite place v is real, then v.Completion is isometric to ℝ.

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

Around this declaration

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

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

Realstatement and proof · cited by 25,697
Equivproof · cited by 8,337
Fieldstatement and proof · cited by 7,404
NumberField.InfinitePlacestatement and proof · cited by 604
NumberField.InfinitePlace.IsRealstatement and proof · cited by 301
IsometryEquivstatement · cited by 177
EquivLike.toEquivproof · cited by 125
NumberField.InfinitePlace.Completionstatement and proof · cited by 69
NumberField.InfinitePlace.Completion.ringEquivRealOfIsRealproof · cited by 4
NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsRealproof · cited by 2

Results whose statement or proof uses this declaration.

Nothing cites this yet.