ClassFieldTheory.herbrandFunctionAtLowerIndex_difference
The difference of successive rational Herbrand values is the normalized size of the next lower ramification group.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · statement
theorem herbrandFunctionAtLowerIndex_difference
(K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
(A : ValuationSubring L) (n : ℕ) :
herbrandFunctionAtLowerIndex K A (n + 1) -
herbrandFunctionAtLowerIndex K A n =
(Nat.card (lowerRamificationGroup K A (n + 1)) : ℚ) /
Nat.card (lowerRamificationGroup K A 0)