Def IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt

Modification history

2025-10-05 10:04

Mathlib/NumberTheory/LocalField/Basic.lean

feat: the definition of nonarchimedean local fields (#27465)

Added IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt View on Github →