Theorems · Theorem · number theory

NumberField.AdeleRing.algebraMap_fst_apply

∀ (R : Type u_1) (K : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : K) (v : NumberField.InfinitePlace K),
  ((algebraMap K (NumberField.AdeleRing R K)) x).1 v = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }

Defined in

Mathlib.NumberTheory.NumberField.AdeleRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing