Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Totally real and totally complex number fields #

This file defines the type of totally real and totally complex number fields.

Main Definitions and Results #

Tags #

number field, infinite places, totally real, totally complex

A number field K is totally real if all of its infinite places are real. In other words, the image of every ring homomorphism K → ℂ is a subset of .

Instances

    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.

    Equations
    Instances For
      instance NumberField.isTotallyReal_sup {K : Type u_2} [Field K] [NumberField K] {E F : Subfield K} [IsTotallyReal E] [IsTotallyReal F] :
      IsTotallyReal (EF)
      instance NumberField.isTotallyReal_iSup {K : Type u_2} [Field K] [NumberField K] {ι : Type u_3} {k : ιSubfield K} [∀ (i : ι), IsTotallyReal (k i)] :
      IsTotallyReal (⨆ (i : ι), k i)

      A number field K is totally complex if all of its infinite places are complex.

      Instances