n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
dig : List ℤ := List.map Coe.coe (digits 10 n)
⊢ 11 ∣ n
n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
⊢ 11 ∣ n
let dig := (digits 10 n).map (Coe.coe : ℕ → ℤ)
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
⊢ 11 ∣ n
n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
dig : List ℤ := List.map Coe.coe (digits 10 n)
⊢ 11 ∣ n
replace h : Even dig.length := by rwa [List.length_map]
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
⊢ List.alternatingSum dig = 0
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
⊢ 11 ∣ n
refine' eleven_dvd_iff.2 ⟨0, (_ : dig.alternatingSum = 0)⟩
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
this : List.alternatingSum (List.reverse dig) = (-1) ^ (List.length dig + 1) • List.alternatingSum dig
⊢ List.alternatingSum dig = 0
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
⊢ List.alternatingSum dig = 0
have := dig.alternatingSum_reverse
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
this : List.alternatingSum (List.map Coe.coe (digits 10 n)) = -List.alternatingSum dig
⊢ List.alternatingSum dig = 0
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
this : List.alternatingSum (List.reverse dig) = (-1) ^ (List.length dig + 1) • List.alternatingSum dig
⊢ List.alternatingSum dig = 0
rw [(p.map _).reverse_eq, _root_.pow_succ, h.neg_one_pow, mul_one, neg_one_zsmul] at this
no goals
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
this : List.alternatingSum (List.map Coe.coe (digits 10 n)) = -List.alternatingSum dig
⊢ List.alternatingSum dig = 0
exact eq_zero_of_neg_eq this.symm
no goals
n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
dig : List ℤ := List.map Coe.coe (digits 10 n)
⊢ Even (List.length dig)
rwa [List.length_map]