Theorems · Theorem · number theory

NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal

∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) {v : NumberField.InfinitePlace K} [w.LiesOver v]
  [inst_4 : Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion]
  [ContinuousSMul v.Completion w.Completion],
  v.IsReal →
    NumberField.ComplexEmbedding.LiesOver (NumberField.InfinitePlace.Completion.extensionEmbedding w)
      (NumberField.InfinitePlace.Completion.extensionEmbedding v)

Defined in

Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNumberField.InfinitePlace.LiesOverAlgebraIsScalarTowerContinuousSMul