Theorems · Definition · number theory

NumberField.InfinitePlace.LiesOver

{K : Type u_1} →
  [inst : Field K] →
    {L : Type u_2} →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace L → NumberField.InfinitePlace K → Prop

An infinite place w of L / K lies over the infinite place v of K if v is the restriction of w to K.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Cited by

25 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra