Module

PrimePowerIntegralMultiple.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.PrimePowerIntegralMultiple

1 declaration indexed from sourceView source ↗

Module documentation

Integral multiples by powers of the residue characteristic

The residue characteristic has value less than one. Its powers therefore make any field element integral, by the Archimedean property of the multiplicative integers with zero. Completeness is not needed.

Imports2

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.RamificationIndex
Mathlib.GroupTheory.ArchimedeanDensely

Imported by2

theorem

exists_natCast_pow_mul_le_one

L24 ↗

Valuation.exists_natCast_pow_mul_le_one

Documentation

Every field element becomes integral after multiplication by a power of the residue characteristic.

Source context 2 commands

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

namespace Valuation
variable {K : Type*} [Field K]

Lean source · statement

theorem exists_natCast_pow_mul_le_one
    (v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ)
    [CharP (IsLocalRing.ResidueField v.valuationSubring) p] (b : K) :
    ∃ n : ℕ, v ((p : K) ^ n * b) ≤ 1

Module documentation

Integral multiples by powers of the residue characteristic

Declarations

exists_natCast_pow_mul_le_one