Module

QuadraticReality.lean

Nyll.SawinTotallyRealTowers.QuadraticReality

2 declarations indexed from sourceView source ↗

Module documentation

Reality of an extension generated by a rational square root

A square root of a nonnegative rational number has real image under every complex embedding. If it generates the extension, conjugation fixes the whole image. Conversely, a rational number that is a square in a totally real number field must be nonnegative.

Imports6

Mathlib.Algebra.Algebra.Rat
Mathlib.Algebra.Ring.Commute
Mathlib.Analysis.Real.Sqrt
Mathlib.Data.Rat.Cast.Order
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Imported by3

theorem

isTotallyReal_of_sq_nonneg_adjoin

L32 ↗

ClassFieldTower.Sawin.isTotallyReal_of_sq_nonneg_adjoin

Documentation

An extension of ℚ generated by a square root of a nonnegative rational number is totally real. No degree or nonsquare hypothesis is needed.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped ComplexConjugate
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isTotallyReal_of_sq_nonneg_adjoin
    (L : Type u) [Field L] [Algebra ℚ L] {d : ℚ} {α : L}
    (hα : α ^ 2 = algebraMap ℚ L d)
    (hgen : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (hd : 0 ≤ d) : IsTotallyReal L

theorem

rat_nonneg_of_sq_of_isTotallyReal

L77 ↗

ClassFieldTower.Sawin.rat_nonneg_of_sq_of_isTotallyReal