All.lean
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.All
0 declarations indexed from sourceView source ↗
Module documentation
Hilbert ramification over Dedekind domains
This aggregate exposes prime contractions, decomposition and fixed fields, conjugation, orbit cardinalities, and valued Galois comparisons in Dedekind extensions.
Imports11
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Basic
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.CompositumUnramified
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Conjugation
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.FixedFieldTower
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.FixedFieldUnramified
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.FixedFields
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.NumberFieldPrimes
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.OrbitCardinality
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.PrimeContractions
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.TowerInvariants
- Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.ValuedGalois
This module has no indexed declarations. Its imports and full source are available here.