Module

Small.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Small

1 declaration indexed from sourceView source ↗

Module documentation

The carrier of a nonarchimedean local field is universe-small

The integer ring injects into the sequence of its finite quotients by powers of the maximal ideal. Its fraction field is therefore also small enough to be represented in Type 0. No countability of the field itself is asserted.

Imports3

Imported by2

theorem

nonarchimedeanLocalField_small

L30 ↗

LocalFieldTheory.nonarchimedeanLocalField_small

Documentation

A local field in any universe has a carrier equivalent to a type in Type 0.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuativeRel
universe u

Lean source · statement

theorem nonarchimedeanLocalField_small
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Small.{0} K

Module documentation

The carrier of a nonarchimedean local field is universe-small

Declarations

nonarchimedeanLocalField_small