Zulip Chat Archive

Stream: general

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