Theorems · Theorem · number theory

NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one

∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → σ ≠ 1 → orderOf σ = 2

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra