Theorems · Theorem · number theory

NumberField.IsCMField.isConj_eq_isConj

∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] {φ ψ : K →+* ℂ}
  {σ τ : Gal(K/↥(NumberField.maximalRealSubfield K))},
  NumberField.ComplexEmbedding.IsConj φ σ → NumberField.ComplexEmbedding.IsConj ψ τ → σ = τ

All the conjugations of a CM-field over its maximal real subfield are the same.

Defined in

Mathlib.NumberTheory.NumberField.CMField

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCharZeroNumberField.IsCMField