All.lean
Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.All
0 declarations indexed from sourceView source ↗
Module documentation
Low-degree Herbrand quotients
Public aggregate for the low-degree Tate quotients, their cardinality and exact-sequence calculations, and the resulting Herbrand quotient theory.
Imports8
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Basic
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.BinaryProduct
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Cardinality
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Core
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.EquivariantEquiv
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Index
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Product
- Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.TateComparison
Imported by1
This module has no indexed declarations. Its imports and full source are available here.