The shift rule for the Fermat quotient

For the Fermat quotient q(l) = (l^(p−1) − 1)/p: (l + p t)^(p−1) ≡ l^(p−1) − p t l^(p−2) (mod p²), hence q(l + p t) ≡ q(l) − t / l (mod p). The binomial step is Mathlib's sq_dvd_add_pow_sub_sub.

Main results

• ConjeturaC.sq_dvd_shift, ConjeturaC.pow_shift_zmod_sq: the congruence modulo p².
• ConjeturaC.fermatQuot_shift: q(l + p t) ≡ q(l) − t l⁻¹ (mod p) for p ∤ l.

def ConjeturaC.fermatQuot (p : ℕ) (l : ℤ) : ℤ

Fermat quotient (integer division; exact when p is prime and p ∤ l).

Equations

• ConjeturaC.fermatQuot p l = (l ^ (p - 1) - 1) / ↑p

theorem ConjeturaC.sq_dvd_shift {p : ℕ} (hp : 1 ≤ p) (l t : ℤ) : ↑p ^ 2 ∣ (l + ↑p * t) ^ (p - 1) - (l ^ (p - 1) - ↑p * t * l ^ (p - 2))

p² ∣ (l + p t)^(p-1) - (l^(p-1) - p t l^(p-2)), for any p ≥ 1.

theorem ConjeturaC.pow_shift_zmod_sq {p : ℕ} (hp : 1 ≤ p) (l t : ℤ) : (↑l + ↑p * ↑t) ^ (p - 1) = ↑l ^ (p - 1) - ↑p * ↑t * ↑l ^ (p - 2)

Same statement as an identity in ZMod (p^2).

theorem ConjeturaC.mul_fermatQuot {p : ℕ} [hp : Fact (Nat.Prime p)] {l : ℤ} (hl : ¬↑p ∣ l) : ↑p * fermatQuot p l = l ^ (p - 1) - 1

theorem ConjeturaC.fermatQuot_shift {p : ℕ} [hp : Fact (Nat.Prime p)] {l : ℤ} (t : ℤ) (hl : ¬↑p ∣ l) : ↑(fermatQuot p (l + ↑p * t)) = ↑(fermatQuot p l) - ↑t * (↑l)⁻¹

Shift rule: q(l + p t) ≡ q(l) - t · l⁻¹ (mod p).