ClassFieldTheory.fractionalIdealNorm_primeExponent
The exponent at v of an ideal norm is the inertia-degree-weighted sum of the exponents at the primes lying above v.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v
open scoped Classical inLean source · full declaration
theorem fractionalIdealNorm_primeExponent
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[FiniteDimensional K L]
(I : NumberFieldFractionalIdealGroup L)
(v : HeightOneSpectrum (𝓞 K)) :
FractionalIdeal.count K v
((fractionalIdealNorm K L I : NumberFieldFractionalIdealGroup K) :
FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
(NumberFieldFractionalIdealGroup.countVector I).sum fun W n =>
if fractionalIdealNormPrimeBelow K L W = v then
(W.asIdeal.inertiaDeg (𝓞 K) : ℤ) * n
else 0 := by
exact fractionalIdealNorm_count K L I v