Module

BoundedCyclotomicExponent.lean

Nyll.ValuedFieldTheory.Valuation.BoundedCyclotomicExponent

1 declaration indexed from sourceView source ↗

Module documentation

The p-adic order of a bounded cyclotomic exponent

If a natural exponent below p^(s+1) differs from one, its difference from one is nonzero and has p-adic order below s+1. The absolute value of that integer is strictly below the modulus, so divisibility by the modulus is impossible. The exponent zero and the prime two are included.

Imports3

Mathlib.NumberTheory.Padics.PadicVal.Basic
Mathlib.Data.Int.Basic
Mathlib.Algebra.Order.GroupWithZero.Basic

Imported by2

theorem

one_sub_natCast_ne_zero_and_padicValInt_lt

L24 ↗

ValuationTheory.one_sub_natCast_ne_zero_and_padicValInt_lt

Documentation

A bounded exponent different from one has nonzero difference from one and p-adic order strictly below the selected prime-power level.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem one_sub_natCast_ne_zero_and_padicValInt_lt
    (p a s : ℕ) [Fact p.Prime]
    (ha : a < p ^ (s + 1)) (ha1 : a ≠ 1) :
    1 - (a : ℤ) ≠ 0 ∧ padicValInt p (1 - (a : ℤ)) < s + 1

Module documentation

The p-adic order of a bounded cyclotomic exponent

Declarations

one_sub_natCast_ne_zero_and_padicValInt_lt