ext f
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiagonal m = filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)