Theorems · Theorem · number theory

NumberField.FinitePlace.norm_embedding

∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : K),
  ‖(NumberField.FinitePlace.embedding v) x‖ = (NumberField.HeightOneSpectrum.adicAbv K v) x

The norm of the image after the embedding associated to v is equal to the v-adic absolute value.

Defined in

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Cited by

6 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebraIsDedekindDomainIsFractionRingModule.FiniteModule.Free