ClassFieldTower.Sawin.exists_squarefree_int_generator_of_isQuadraticExtension
Every quadratic extension of ℚ has a generator whose square is a nonzero signed squarefree integer, nonsquare in ℚ.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFieldTower.SawinLean source · statement
theorem exists_squarefree_int_generator_of_isQuadraticExtension
(L : Type u) [Field L] [Algebra ℚ L]
[Algebra.IsQuadraticExtension ℚ L] :
∃ d : ℤ, ∃ β : L,
Squarefree d.natAbs ∧ d ≠ 0 ∧
β ^ 2 = algebraMap ℚ L (d : ℚ) ∧
IntermediateField.adjoin ℚ ({β} : Set L) = ⊤ ∧
¬ IsSquare (d : ℚ)