The finite set of allowed places is the actual six-prime support, with cardinality six. It provides the coordinate set used by H² localization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawindef sixAllowedPrimes : Finset Nat.PrimesThe six allowed finite places as a finite coordinate set.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawindef sawinFinitePrimeSupport : Finset (HeightOneSpectrum (𝓞 ℚ))Finite-set and set-valued versions of the ramification support agree.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawintheorem mem_sawinFinitePrimeSupport_iff (v : HeightOneSpectrum (𝓞 ℚ)) :
v ∈ sawinFinitePrimeSupport ↔ v ∈ sawinRationalPrimeSupportThere are precisely six finite coordinates in the allowed support.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawintheorem sawinFinitePrimeSupport_card : sawinFinitePrimeSupport.card = 6