NYLL
Module

PowerSubImage.lean

Nyll.ValuedFieldTheory.Valuation.PowerSubImage
2 declarations indexed from sourceView source ↗

Module documentation

Valuation obstructions for powers minus the identity

If 1 < v (x ^ n - x) and n > 1, the leading term determines its value, which must be an n-th power. This gives an obstruction using the logarithmic exponent of an integer-valued valuation.

Imports2
  • Mathlib.RingTheory.Valuation.Basic
  • Mathlib.Algebra.Order.GroupWithZero.Canonical
Imported by2

Declarations

theorem

pow_sub_ne_of_one_lt_of_not_pow

L23 ↗
Valuation.pow_sub_ne_of_one_lt_of_not_pow
Documentation

Above valuation one, powers minus the identity can take only power values.

Source context 2 commands

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

namespace Valuation
universe u v
Lean source · statement
theorem pow_sub_ne_of_one_lt_of_not_pow
    {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation K Γ) (n : ℕ) (hn : 1 < n)
    (a : K) (ha : 1 < w a) (hpow : ∀ y : K, w y ^ n ≠ w a) :
    ∀ x : K, x ^ n - x ≠ a
theorem

pow_sub_ne_of_one_lt_of_log_not_dvd

L44 ↗
Valuation.pow_sub_ne_of_one_lt_of_log_not_dvd
Documentation

An integer valuation exponent not divisible by n excludes a value of x ^ n - x whenever the target lies above valuation one.

Source context 2 commands

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

namespace Valuation
universe u v
Lean source · statement
theorem pow_sub_ne_of_one_lt_of_log_not_dvd
    {K : Type u} [Field K]
    (w : Valuation K (WithZero (Multiplicative ℤ))) (n : ℕ) (hn : 1 < n)
    (a : K) (ha : 1 < w a) (hdiv : ¬ (n : ℤ) ∣ WithZero.log (w a)) :
    ∀ 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.