1.1. The maximal real subfield🔗

Definition1.1.1

uses 0

Used by 5

Reverse dependency previews

Preview

Theorem 1.3.1

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

The maximal real subfield of \mathbb{Q}(\zeta_p) is \mathbb{Q}(\zeta_p)^+ \;=\; \mathbb{Q}(\zeta_p + \zeta_p^{-1}), the fixed field of complex conjugation. It is a totally real subfield of \mathbb{Q}(\zeta_p) of degree (p-1)/2 over \mathbb{Q}, and \mathbb{Q}(\zeta_p) is a CM field over \mathbb{Q}(\zeta_p)^+.

Lean code for Definition1.1.1●1 definition

defdefined in Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

complete

def NumberField.maximalRealSubfield.{u_2} (K : Type u_2) [Field K] :
  Subfield K

def NumberField.maximalRealSubfield.{u_2}
  (K : Type u_2) [Field K] : Subfield K

The maximal real subfield of `K`. It is totally real,
see `NumberField.isTotallyReal_maximalRealSubfield`, and contains all the other totally real
subfields of `K`, see `NumberField.IsTotallyReal.le_maximalRealSubfield`.

The class-number splitting begins by separating the class number of the full cyclotomic field from that of its maximal real subfield.