NYLL
Module

IntCastValuation.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.IntCastValuation
1 declaration indexed from sourceView source ↗

Module documentation

Values of integers in a valued field

The value of a nonzero integer is determined by its p-adic order at the residue characteristic. Taking its natural absolute value reduces the formula to the natural-number case, without a characteristic-zero hypothesis.

Imports1
Imported by2

Declarations

theorem

intCast_eq_pow_padicValInt

L26 ↗
Valuation.intCast_eq_pow_padicValInt
Documentation

The value of a nonzero integer is the residue prime's value raised to the integer's p-adic order.

Source context 4 commands

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

namespace Valuation
universe u w
variable {K : Type u} [Field K]
variable {Γ₀ : Type w} [LinearOrderedCommGroupWithZero Γ₀]
Lean source · statement
theorem intCast_eq_pow_padicValInt (v : Valuation K Γ₀)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (z : ℤ) (hz : z ≠ 0) :
    v (z : K) = v (p : K) ^ padicValInt p z

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.