The radicands 5, 13, 17, 21, 33 have no nonempty square subproduct. There are exactly thirty-one nonempty subsets. The natural-number check uses the square-root decision procedure inside the Lean kernel; the rational statement follows from the square criterion for natural casts.
The five radicands used in the initial real multiquadratic layer.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.Sawindef sawinQuadraticRadicand : Fin 5 → ℕSurrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.Sawintheorem sawinQuadraticRadicand_nat_products_nonsquare :
∀ s : Finset (Fin 5), s.Nonempty →
¬ IsSquare (∏ i ∈ s, sawinQuadraticRadicand i)Every nonempty subproduct of the five radicands is nonsquare over ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.Sawintheorem sawinQuadraticRadicand_product_nonsquare
(s : Finset (Fin 5)) (hs : s.Nonempty) :
¬ IsSquare (∏ i ∈ s, (sawinQuadraticRadicand i : ℚ))Each of the five radicands defines a genuine quadratic extension of ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.Sawintheorem sawinQuadraticRadicand_nonsquare (i : Fin 5) :
¬ IsSquare (sawinQuadraticRadicand i : ℚ)