## Stream: new members

### Topic: Proof transfer from antidiagonal to divisors_antidiagonal

#### Sigma (Jan 02 2022 at 06:20):

In the library we have docs#finset.nat.sum_antidiagonal_eq_sum_range_succ and I need to use the analogous statement

variables {M : Type*} [ring M]
lemma div_antidiagonal_eq_sum_divisors (X : ℕ) (func : ℕ × ℕ → M) :
X.divisors_antidiagonal.sum func =
finset.sum X.divisors (λ x, func ⟨x, X / x⟩)


I was hoping I could basically copy the proof over, swapping n-k for X / x, but the proof just looks like black magic. I tried printing it and looked to find the important bits, but it refused to typecheck even after I cleaned it up. I tried rewriting it in terms of a product instead of a sum like for the one we have, but it didn't do anything.
I was wondering what I should try next.

#### Eric Rodriguez (Jan 02 2022 at 06:42):

import algebra.big_operators.nat_antidiagonal
import number_theory.divisors

open_locale big_operators

variables {M : Type*} [ring M]
lemma div_antidiagonal_eq_sum_divisors (X : ℕ) (func : ℕ × ℕ → M) :
X.divisors_antidiagonal.sum func =
∑ x in X.divisors, func (x, X / x) :=
begin
convert finset.sum_map _ ⟨λ x, (x, X / x) , λ x y h, (prod.mk.inj h).1⟩ _,
ext,
simp,
end


seems to lead to a pretty sensible proof state, and the proof is basically copy-paste; what are you confused about? glad to try and explain if i get it myself ^^

Last updated: Dec 20 2023 at 11:08 UTC