NYLL
Module

HerbrandFunctionAtLowerIndexStrictMono.lean

Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionAtLowerIndexStrictMono
1 declaration indexed from sourceView source ↗

Module documentation

Strict growth of the integral-index Herbrand function

For a finite extension, each lower ramification group is finite and nonempty. Thus every increment of the rational Herbrand function is strictly positive. This does not assert integrality of its values.

Imports4
Imported by1

Declarations

theorem

herbrandFunctionAtLowerIndex_strictMono

L26 ↗
ClassFieldTheory.herbrandFunctionAtLowerIndex_strictMono
Documentation

The rational Herbrand function at nonnegative integral lower indices is strictly increasing for a finite field extension.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory
universe u v
Lean source · statement
theorem herbrandFunctionAtLowerIndex_strictMono
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] (A : ValuationSubring L) :
    StrictMono (herbrandFunctionAtLowerIndex K A)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.