Lifting the exponent lemma

TheoremLifting the exponent for odd primes#✓fully proved

Let \(p\) be an odd prime, let \(a \ne b\) be integers such that \(p\) divides \(a - b\) but does not divide \(ab\), and let \(n \ge 1\) be a natural number. Then

\[v_p(a^n - b^n) = v_p(n) + v_p(a - b),\]

where \(v_p\) denotes the \(p\)-adic valuation.

theorem padicValInt_pow_sub_pow (p : ℕ) [Fact (Nat.Prime p)] {a b : ℤ} {n : ℕ}
    (hodd : Odd p) (hne : a ≠ b) (hcop : ¬ (p : ℤ) ∣ a * b)
    (hdiv : (p : ℤ) ∣ a - b) (hn : n ≠ 0) :
    padicValInt p (a ^ n - b ^ n) = padicValNat p n + padicValInt p (a - b)

TheoremLifting a congruence to one along powers of the modulus#✓fully proved

Let \(p\), \(n\) and \(a\) be natural numbers. If \(a \equiv 1 \pmod p\), then \(a^{p^n} \equiv 1 \pmod{p^{n+1}}\).

The modulus \(p\) need not be prime.

theorem pow_pow_modEq_one_of_modEq_one (p n a : ℕ) (h : Nat.ModEq p a 1) :
    Nat.ModEq (p ^ (n + 1)) (a ^ (p ^ n)) 1

Used by 1

Used byPrime-power lifting of a congruence to one

TheoremPrime-power lifting of a congruence to one#✓fully proved

Let \(p\) be a prime and let \(n\) and \(a\) be positive integers. If \(a \equiv 1 \pmod p\), then \(a^{p^n} \equiv 1 \pmod{p^{n+1}}\).

theorem prime_power_lifting_modEq_one
    (p n a : ℕ) (hp : Nat.Prime p) (hn : 0 < n) (ha : 0 < a)
    (h : Nat.ModEq p a 1) :
    Nat.ModEq (p ^ (n + 1)) (a ^ (p ^ n)) 1

Sources

• Hacène Belbachir and Celia Salhi, "The Generalized Bi-Periodic Fibonacci Sequence Modulo m," Journal of Integer Sequences 24 (2021), Article 21.9.4, Theorem, lines 340–341, https://cs.uwaterloo.ca/journals/JIS/VOL24/Salhi/salhi4.tex. It follows from pow_pow_modEq_one_of_modEq_one; the hypotheses hp, hn and ha are unused and keep the source's shape.

Uses 1

Proof usesLifting a congruence to one along powers of the modulus

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.