Module

QuadraticGenerator.lean

Nyll.SawinTotallyRealTowers.QuadraticGenerator

1 declaration indexed from sourceView source ↗

Module documentation

A nonsquare rational generator for a quadratic extension

The nontrivial square root of unity in ℚ makes every quadratic extension a Kummer extension. The resulting generator has irreducible polynomial X ^ 2 - C d, which forces its rational square d to be nonzero and nonsquare. No ramification or reality assumption is involved.

Imports3

Mathlib.Algebra.Group.Even
Mathlib.FieldTheory.KummerExtension
Mathlib.FieldTheory.KummerPolynomial

Imported by3

theorem

exists_nonsquare_rat_generator_of_isQuadraticExtension

L26 ↗

ClassFieldTower.Sawin.exists_nonsquare_rat_generator_of_isQuadraticExtension

Documentation

Every quadratic extension of ℚ is generated by a square root of a nonzero nonsquare rational number.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_nonsquare_rat_generator_of_isQuadraticExtension
    (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L] :
    ∃ (d : ℚ) (α : L), α ^ 2 = algebraMap ℚ L d ∧
      IntermediateField.adjoin ℚ ({α} : Set L) = ⊤ ∧
      ¬ IsSquare d ∧ d ≠ 0

Module documentation

A nonsquare rational generator for a quadratic extension

Declarations

exists_nonsquare_rat_generator_of_isQuadraticExtension