Theorems · Theorem · number theory

NumberField.FinitePlace.mk_apply

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K),
  (NumberField.FinitePlace.mk v) x = ‖(NumberField.FinitePlace.embedding v) x‖

Defined in

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField