Theorems · Theorem · number theory

NumberField.InfinitePlace.bijOn_sumElim_conjugate

∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  Set.BijOn
    (Sum.elim NumberField.InfinitePlace.embedding
      (NumberField.ComplexEmbedding.conjugate ∘ NumberField.InfinitePlace.embedding))
    (Set.sumEquiv.symm
      (NumberField.InfinitePlace.ramifiedPlacesOver L v, NumberField.InfinitePlace.ramifiedPlacesOver L v))
    (NumberField.ComplexEmbedding.mixedEmbeddingsOver L v.embedding)

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra