Theorems · Definition · number theory

NumberField.LiesOver.completionMap

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {v : NumberField.InfinitePlace K} →
            {w : NumberField.InfinitePlace L} → [w.LiesOver v] → v.Completion →+* w.Completion

The ring homomorphism v.Completion →+* w.Completion induced by algebraMap K L, when w lies over v.

Defined in

Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNumberField.InfinitePlace.LiesOver