English
For a prime p ≠ 2 and elements a, r in a ring R, if r | a^p and r | p a, then C r divides (C a X − 1)^p + 1.
Русский
Для простого p ≠ 2 и элементов a, r в кольце R: если r делит a^p и r делит p a, тогда C r делит (C a X − 1)^p + 1.
LaTeX
$$$$\text{If } p \text{ is prime and } p \neq 2, \; r \mid a^p, \; r \mid p a \quad\Rightarrow\quad C r \mid \bigl(C a \cdot X - 1\bigr)^p + 1.$$$$
Lean4
theorem dvd_C_mul_X_sub_one_pow_add_one {p : ℕ} (hpri : p.Prime) (hp : p ≠ 2) (a r : R) (h₁ : r ∣ a ^ p)
(h₂ : r ∣ p * a) : C r ∣ (C a * X - 1) ^ p + 1 :=
by
have := hpri.dvd_add_pow_sub_pow_of_dvd (C a * X) (-1) (r := C r) ?_ ?_
· rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this
· simp only [mul_pow, ← map_pow, dvd_mul_right, (_root_.map_dvd C h₁).trans]
simp only [map_mul, map_natCast, ← mul_assoc, dvd_mul_right, (_root_.map_dvd C h₂).trans]
