English
A function f belongs to finMulAntidiag d n if and only if the product over i of f(i) equals n and n ≠ 0 (for the nonzero case); otherwise, membership is false when n=0.
Русский
Функция f принадлежит finMulAntidiag d n тогда и только тогда, когда произведение по i от f(i) равно n и n ≠ 0; иначе принадлежность ложна, когда n=0.
LaTeX
$$$f\in\text{finMulAntidiag}(d,n) \iff \left(\prod_{i} f(i)=n \land n\neq 0\right)$$$
Lean4
@[simp]
theorem mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} : f ∈ finMulAntidiag d n ↔ ∏ i, f i = n ∧ n ≠ 0 :=
by
unfold finMulAntidiag
split_ifs with h
· simp_rw [mem_map, mem_finAntidiagonal, Function.Embedding.arrowCongrRight_apply, Function.comp_def,
Function.Embedding.trans_apply, Equiv.coe_toEmbedding, Function.Embedding.coeFn_mk, ←
Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq, toMul_sum,
(Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists, Equiv.piCongrRight_apply, Pi.map_apply,
toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe, PNat.coe_prod]
constructor
· rintro ⟨a, ha_mem, rfl⟩
exact ⟨ha_mem, h.ne.symm⟩
· rintro ⟨rfl, _⟩
refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩
apply Nat.pos_of_ne_zero
exact Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)
· simp only [not_lt, nonpos_iff_eq_zero] at h
simp only [h, notMem_empty, ne_eq, not_true_eq_false, and_false]
