NYLL
Module

ArtinSchreierNonSurjective.lean

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

Module documentation

Failure of surjectivity for powers minus the identity in a DVF

The inverse of a prime uniformizer cannot equal x ^ n - x for n > 1: its reciprocal polynomial is Eisenstein and would otherwise have a root in the base field. The argument does not require Henselianity or a characteristic assumption.

Imports5
Imported by3

Declarations

theorem

exists_not_pow_sub

L27 ↗
ValuationTheory.DiscreteValuationField.DVF.exists_not_pow_sub
Documentation

Powers minus the identity omit an element in every discretely valued field.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField
open Polynomial
universe u v
Lean source · statement
theorem DVF.exists_not_pow_sub
    {K : Type u} [Field K] (base : DVF.{u, v} K)
    (n : ℕ) (hn : 1 < n) :
    ∃ a : K, ∀ x : K, x ^ n - x ≠ a

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