ModuleRealCompositum.lean
Nyll.SawinTotallyRealTowers.RealCompositum
2 declarations indexed from sourceView source ↗ Module documentation
Real places in composita over the rationals
The initial Sawin tower has base field ℚ. Over this base, being unramified at infinite places is exactly total reality. Total reality is preserved by composita inside an algebraic extension, so this supplies the real-place condition independently of the finite ramification support and the prime p.
Imports3
- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Imported by3
Declarations
ClassFieldTower.Sawin.isUnramifiedAtInfinitePlaces_rat_iff_isTotallyReal
DocumentationSince every infinite place of ℚ is real, an extension of ℚ is unramified at infinite places exactly when its infinite places are all real.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField
universe u
namespace ClassFieldTower.Sawin
ClassFieldTower.Sawin.isUnramifiedAtInfinitePlaces_rat_sup
DocumentationThe compositum of two subextensions of an algebraic extension of ℚ retains the real-place condition. No odd-degree or Galois hypothesis is needed.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField
universe u
namespace ClassFieldTower.Sawin