English
Define finMulAntidiag(d,n) to be the finite set of d-tuples of natural numbers whose product equals n; it is empty if n = 0; otherwise it comes from the d-fold antidiagonal via a multiplicative embedding from positive naturals.
Русский
Определим finMulAntidiag(d,n) как конечную множество d-кортежей натуральных чисел, чья произведение равно n; пусто если n = 0; иначе получаем из d-частного антидиагоналя через умножающее вложение.
LaTeX
$$$\text{finMulAntidiag}(d,n) = \begin{cases} \text{Finset.finAntidiagonal}_d(\text{Additive.ofMul}(n)), & n>0 \\ \emptyset, & n=0 \end{cases}$$$
Lean4
/-- The `Finset` of all `d`-tuples of natural numbers whose product is `n`. Defined to be `∅` when
`n = 0`. -/
def finMulAntidiag (d : ℕ) (n : ℕ) : Finset (Fin d → ℕ) :=
if hn : 0 < n then
(Finset.finAntidiagonal d (Additive.ofMul (α := ℕ+) ⟨n, hn⟩)).map <|
.arrowCongrRight <| Additive.toMul.toEmbedding.trans <| ⟨PNat.val, PNat.coe_injective⟩
else ∅
