English
Let R be a commutative semiring, p prime, and u, v in R with v | u and p u v | u^p. Then for any m in N and x in R there exists y in R such that (1 + u x)^(p^m) = 1 + p^m u (x + v y).
Русский
Пусть R — коммутативное полускольное кольцо, p — простое, и u, v ∈ R с v | u и p u v | u^p. Тогда для любого m ∈ N и x ∈ R существует y ∈ R такое, что (1 + u x)^(p^m) = 1 + p^m u (x + v y).
LaTeX
$$$\\\\forall R [CommSemiring R], \\\\forall u, v \\\\in R, \\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\wedge v \\\\\\mid u \\\\wedge p u v \\\\\\mid u^{p} \\\\Rightarrow \\\\forall x \\\\in R, \\\\exists y \\\\in R, (1 + u x)^{p^{m}} = 1 + p^{m} u (x + v y).$$$$
Lean4
theorem exists_one_add_mul_pow_prime_pow_eq {u v : R} (hp : p.Prime) (hvu : v ∣ u) (hpuv : p * u * v ∣ u ^ p) (x : R)
(m : ℕ) : ∃ y, (1 + u * x) ^ (p ^ m) = 1 + p ^ m * u * (x + v * y) :=
match m with
| 0 => ⟨0, by simp⟩
| m + 1 => by
rw [pow_succ', pow_mul]
obtain ⟨y, hy⟩ := exists_one_add_mul_pow_prime_eq hp hvu hpuv x
rw [hy]
obtain ⟨z, hz⟩ :=
exists_one_add_mul_pow_prime_pow_eq (u := p * u) (v := p * v) hp (mul_dvd_mul_left _ hvu)
(by
rw [mul_pow]
simp only [← mul_assoc]
rw [mul_assoc, mul_assoc, ← mul_assoc u, mul_comm u]
apply mul_dvd_mul _ hpuv
rw [← pow_two]
exact pow_dvd_pow _ hp.two_le)
(x + v * y) m
use y + p * z
rw [hz]
ring
