GlobalClassFieldTheory.Reciprocity.rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
The rational absolute idele-class representation satisfies the abstract class-field axiom.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace GlobalClassFieldTheory
open scoped NumberField TensorProduct
open NumberField
open CyclicCohomology ClassFormation
open LocalClassFieldTheory
noncomputable section
open CategoryTheory
namespace ReciprocityLean source · statement
theorem rationalIdeleClassRepresentation_satisfiesClassFieldAxiom :
SatisfiesClassFieldAxiom rationalIdeleClassRepresentation