Topic: Use proof in ∑ big operator
Niels Voss (Dec 12 2022 at 07:02):
Is there a way to fill in this sorry?
example : ℕ := ∑ x in (divisors_antidiagonal 10), (have x.1 * x.2 = 10 := sorry, 5)
I'm basically looking for a way to use the proof that
x ∈ (divisors_antidiagonal 10) within the body of the big ∑. This situation occurred in a more complicated situation where I was trying to prove that a recursive function terminates, when I was doing a recursive call with the second element of each pair in
(divisors_antidiagonal n).erase ⟨1, n⟩
Last updated: Aug 03 2023 at 10:10 UTC