Theorems · Theorem · field theory

AbsoluteValue.denseRange_algebraMap_pi

∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [Finite ι] {v : ι → AbsoluteValue F ℝ},
  (∀ (i : ι), (v i).IsNontrivial) →
    (Pairwise fun i j => ¬(v i).IsEquiv (v j)) → DenseRange ⇑(algebraMap F ((i : ι) → WithAbs (v i)))

If v : ι → AbsoluteValue F ℝ is a finite family of nontrivial, pairwise inequivalent real absolute values on a field F, then the diagonal embedding algebraMap F ((i : ι) → WithAbs (v i)) has dense range. This is the abstract weak approximation theorem; see NumberField.InfinitePlace.denseRange_algebraMap_pi for the number-field special case.

Defined in

Mathlib.Analysis.AbsoluteValue.Equivalence

Cited by

1 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFinite