English
For d, m, n with m | n and n ≠ 0, finMulAntidiag d m equals the piFinset of m being the product condition restricted to divisors of n.
Русский
Для d, m, n с m | n и n ≠ 0, finMulAntidiag d m равен piFinset, ограниченному делителями n и условием произведения равного m.
LaTeX
$$$\text{finMulAntidiag}(d,m) = \{f\in Fintype.piFinset(\,n.divisors\, )\mid ∏ i f i = m\}$ при дополнительных условиях$$
Lean4
theorem finMulAntidiag_eq_piFinset_divisors_filter {d m n : ℕ} (hmn : m ∣ n) (hn : n ≠ 0) :
finMulAntidiag d m = {f ∈ Fintype.piFinset fun _ : Fin d => n.divisors | ∏ i, f i = m} :=
by
ext f
simp only [ne_eq, Fintype.mem_piFinset, mem_divisors, mem_filter]
constructor
· intro hf
refine ⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩
exact fun i => ⟨(dvd_of_mem_finMulAntidiag hf i).trans hmn, hn⟩
· rw [mem_finMulAntidiag]
exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩
