theorem
L19 ↗herbrandFunction_nat
ClassFieldTheory.herbrandFunction_nat
At a natural lower index, the real piecewise Herbrand function equals the rational finite-sum value after casting to reals.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u vLean source · statement
theorem herbrandFunction_nat
(K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
(A : ValuationSubring L) (n : ℕ) :
ClassFieldTheory.herbrandFunction K A (n : ℝ) =
(herbrandFunctionAtLowerIndex K A n : ℝ)