All.lean
Nyll.ClassFieldTheory.Theorems.NormTheorems.All
0 declarations indexed from sourceView source ↗
Module documentation
Local-to-global norm theorems
This module gathers the public local-global principles for field norms.
Imports9
- Nyll.ClassFieldTheory.Theorems.NormTheorems.CyclicHasseNormTheorem
- Nyll.ClassFieldTheory.Theorems.NormTheorems.CompletionTensorNormDecomposition
- Nyll.ClassFieldTheory.Theorems.NormTheorems.CompletionTensorNormDecompositionCanonical
- Nyll.ClassFieldTheory.Theorems.NormTheorems.GlobalNormIsEverywhereLocalNorm
- Nyll.ClassFieldTheory.Theorems.NormTheorems.ComplexInfinitePlaceAllNorm
- Nyll.ClassFieldTheory.Theorems.NormTheorems.InfiniteNormIffPositive
- Nyll.ClassFieldTheory.Theorems.NormTheorems.NegativeOneNotInfiniteNorm
- Nyll.ClassFieldTheory.Theorems.NormTheorems.UnramifiedInfinitePlaceAllNorm
- Nyll.ClassFieldTheory.Theorems.NormTheorems.TensorNormBaseChange
Imported by1
This module has no indexed declarations. Its imports and full source are available here.