Theorems · Theorem · number theory

NumberField.IsCMField.complexEmbedding_complexConj

∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (φ : K →+* ℂ) (x : K),
  φ ((NumberField.IsCMField.complexConj K) x) = (starRingEnd ℂ) (φ x)

Defined in

Mathlib.NumberTheory.NumberField.CMField

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldCharZeroNumberField.IsCMFieldAlgebra.IsIntegral