Module

NatCastValuation.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.NatCastValuation

2 declarations indexed from sourceView source ↗

Module documentation

Values of natural numbers in a valued field

The part of a natural number prime to the residue characteristic has nonzero residue and is therefore a unit of the valuation ring. Thus its value is one, and the value of the natural number is determined by its prime-power factor. No discreteness, completeness, residue-field finiteness, or characteristic-zero hypothesis is needed. The existing discrete-valuation-field API is retained.

Imports4

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic
Mathlib.Algebra.CharP.Defs
Mathlib.NumberTheory.Padics.PadicVal.Basic
Mathlib.RingTheory.Valuation.Integers

Imported by3

theorem

natCast_eq_pow_padicValNat

L31 ↗

Valuation.natCast_eq_pow_padicValNat

Documentation

The value of a nonzero natural number is the value of its residue-characteristic prime-power factor.

Source context 4 commands

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

namespace Valuation
universe u v
variable {K : Type u} [Field K]
variable {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀]

Lean source · statement

theorem natCast_eq_pow_padicValNat (v : Valuation K Γ₀)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (n : ℕ) (hn : n ≠ 0) :
    v (n : K) = v (p : K) ^ padicValNat p n

theorem

valuation_natCast_eq_pow_padicValNat

L69 ↗

ValuationTheory.DiscreteValuationField.DVF.valuation_natCast_eq_pow_padicValNat