NYLL
Module

NondivisibleValueGroup.lean

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

Module documentation

Nondivisibility of a rank-one discrete value group

For each natural number greater than one, the image of a discrete valuation contains a nonzero value that is not an nth power. A normalized valuation and uniformizer supply the witness.

Imports1
Imported by1

Declarations

theorem

exists_value_not_pow

L23 ↗
ValuationTheory.DiscreteValuationField.DVF.exists_value_not_pow
Documentation

A rank-one discrete value group is not divisible by any natural number larger than one. The witness lies in the actual image of the valuation.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
universe u v
Lean source · statement
theorem exists_value_not_pow {K : Type u} [Field K] (D : DVF.{u, v} K)
    (n : ℕ) (hn : 1 < n) :
    ∃ x : K, x ≠ 0 ∧ ∀ y : K, D.valuation y ^ n ≠ D.valuation x

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