Theorems · Theorem · number theory

NumberField.InfinitePlace.denseRange_algebraMap_pi

∀ (K : Type u_1) [inst : Field K] [NumberField K],
  DenseRange ⇑(algebraMap K ((v : NumberField.InfinitePlace K) → WithAbs ↑v))

Weak approximation for infinite places The number field K is dense when embedded diagonally in the product (v : InfinitePlace K) → WithAbs v.1, in which WithAbs v.1 represents K equipped with the topology coming from the infinite place v.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField