ClassFieldTheory.herbrandFunctionAtLowerIndex
The Herbrand value at a nonnegative integral lower index: φ(n) = (1 / |G₀|) · ∑_{i=1}^{n} |Gᵢ|.
Its ramification-theoretic interpretation requires the lower groups to be finite. The definition alone does not impose that hypothesis.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace ClassFieldTheory
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]Lean source · statement
def herbrandFunctionAtLowerIndex (A : ValuationSubring L) (n : ℕ) : ℚ