Module

IsLowerRamificationJump.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.IsLowerRamificationJump

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by4

def

ClassFieldTheory.IsLowerRamificationJump

Documentation

A nonnegative integer n is a lower ramification jump when the lower ramification filtration strictly changes after index n.

Source context 2 commands

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

namespace ClassFieldTheory
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

def IsLowerRamificationJump (A : ValuationSubring L) (n : ℕ) : Prop