All.lean
Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.All
0 declarations indexed from sourceView source ↗
Module documentation
Artin reciprocity for the cyclotomic complexification
This compatibility module reexports the semantic layers constructing the rational fourth-root complexification, its compositum with a number field, the complex-conjugation overextension at a ramified real place, and the resulting infinite-place local-global Artin comparison.
Imports6
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.InfinitePlaceCompatibility
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.InfinitePlaceOverfield
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.NumberFieldComplexification
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.OverextensionArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.RamifiedOverextension
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ComplexificationArtin.RationalComplexification
This module has no indexed declarations. Its imports and full source are available here.