Theorems · Definition · number theory

NumberField.FinitePlace.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) → K →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

The embedding of a field inside its adicCompletion with respect to v.

Defined in

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Cited by

24 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebraIsDedekindDomainIsFractionRing