LeanPool.SelbergSieve4.ForMathlib.ProdsAntidiagonal

@[reducible, inline]

abbrev Nat.finMulAntidiagonal (d n : ℕ) : Finset (Fin d → ℕ)

Alias for the multiplicative antidiagonal indexed by Fin d.

Equations

• d.finMulAntidiagonal n = d.finMulAntidiag n

theorem Nat.mem_finMulAntidiagonal {d n : ℕ} {f : Fin d → ℕ} : f ∈ d.finMulAntidiagonal n ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Membership in the multiplicative antidiagonal.

theorem Nat.finMulAntidiagonal_univ_eq {d m n : ℕ} (hmn : m ∣ n) (hn : n ≠ 0) : d.finMulAntidiagonal m = {f ∈ Fintype.piFinset fun (x : Fin d) => n.divisors | ∏ i : Fin d, f i = m}

theorem Nat.card_finMulAntidiagonal {d n : ℕ} (hn : Squarefree n) : (d.finMulAntidiagonal n).card = d ^ ArithmeticFunction.cardDistinctFactors n