English
A 2-adic LTE identity: for integers with certain parity conditions, the difference x^2^n − y^2^n factors as (x − y) times a product, reflecting v_2 growth with exponent n.
Русский
LTE для 2-адической кратности: при целых числах и подходящих проверочных условиях разность x^{2^n} − y^{2^n} имеет разложение на (x − y) и произведение, отражающее рост v_2 с показательнением n.
LaTeX
$$For integers x,y and n, x^{2^n} − y^{2^n} = (∏_{i=0}^{n-1} (x^{2^i} + y^{2^i}))(x−y).$$
Lean4
/-- **Lifting the exponent lemma** for odd primes. -/
theorem emultiplicity_pow_sub_pow {x y : ℤ} (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) (n : ℕ) :
emultiplicity (↑p) (x ^ n - y ^ n) = emultiplicity (↑p) (x - y) + emultiplicity p n :=
by
rcases n with - | n
· simp only [emultiplicity_zero, add_top, pow_zero, sub_self]
have h : FiniteMultiplicity _ _ := Nat.finiteMultiplicity_iff.mpr ⟨hp.ne_one, n.succ_pos⟩
simp only [Nat.succ_eq_add_one] at h
rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩
conv_lhs => rw [hk, pow_mul, pow_mul]
rw [Nat.prime_iff_prime_int] at hp
rw [emultiplicity_pow_sub_pow_of_prime hp, emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx,
h.emultiplicity_eq_multiplicity]
· rw [← geom_sum₂_mul]
exact dvd_mul_of_dvd_right hxy _
· exact fun h => hx (hp.dvd_of_dvd_pow h)
· rw [Int.natCast_dvd_natCast]
rintro ⟨c, rfl⟩
refine hpn ⟨c, ?_⟩
rwa [pow_succ, mul_assoc]
