n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x in divisorsAntidiagonal n,
      f (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).fst (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).snd =
    ∏ i in divisors n, f (n / i) i
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in divisorsAntidiagonal n, f i.fst i.snd = ∏ i in divisors n, f (n / i) i
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
no goals
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x in divisorsAntidiagonal n,
      f (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).fst (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).snd =
    ∏ i in divisors n, f (n / i) i
exact prod_divisorsAntidiagonal fun i j => f j i