English
If the decimal digits of n form a palindrome with even length, then 11 divides n.
Русский
Если десятичные цифры числа n образуют палиндром с четной длиной, тогда 11 делит n.
LaTeX
$$$\\forall n:\\; (\\mathrm{digits}\\ 10\\ n).(\\text{Palindrome}) \\land \\mathrm{Even} (\\mathrm{digits}\\ 10\\ n).length \\Rightarrow 11 \\mid n$$$
Lean4
theorem eleven_dvd_of_palindrome (p : (digits 10 n).Palindrome) (h : Even (digits 10 n).length) : 11 ∣ n :=
by
let dig := (digits 10 n).map fun n : ℕ => (n : ℤ)
replace h : Even dig.length := by rwa [List.length_map]
refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩
have := dig.alternatingSum_reverse
rw [(p.map _).reverse_eq, _root_.pow_succ', h.neg_one_pow, mul_one, neg_one_zsmul] at this
exact eq_zero_of_neg_eq this.symm
