Theorems · Theorem · number theory

NumberField.InfinitePlace.embedding_mk_eq

∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ),
  (NumberField.InfinitePlace.mk φ).embedding = φ ∨
    (NumberField.InfinitePlace.mk φ).embedding = NumberField.ComplexEmbedding.conjugate φ

Defined in: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Cited by: 7 results in Mathlib
Foundations: Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHomstatement and proof · cited by 10,189
Fieldstatement and proof · cited by 7,404
Complexstatement and proof · cited by 5,565
NumberField.InfinitePlaceproof · cited by 604
NumberField.InfinitePlace.embeddingstatement and proof · cited by 78
NumberField.InfinitePlace.mkstatement and proof · cited by 56
NumberField.ComplexEmbedding.conjugatestatement and proof · cited by 40
NumberField.InfinitePlace.mk_embeddingproof · cited by 25
NumberField.InfinitePlace.mk_eq_iffproof · cited by 5

Cited by7

Results whose statement or proof uses this declaration.

NumberField.InfinitePlace.embedding_mk_eq_of_isRealproof · cited by 5
NumberField.InfinitePlace.LiesOver.isComplex_of_isComplex_underproof · cited by 2
NumberField.InfinitePlace.isUnramified_mk_iff_isUnmixedproof · cited by 1
NumberField.InfinitePlace.isRamified_mk_iff_isMixedproof · cited by 1
NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eqproof · cited by 1
NumberField.InfinitePlace.bijOn_sumElim_conjugateproof · cited by 1
NumberField.mixedEmbedding.disjoint_span_commMap_kerproof · cited by 0