Sets of tuples with a fixed product

This file defines the finite set of d-tuples of natural numbers with a fixed product n as Nat.finMulAntidiag.

Main Results

• There are d^(ω n) ways to write n as a product of d natural numbers, when n is squarefree (card_finMulAntidiag_of_squarefree)
• There are 3^(ω n) pairs of natural numbers whose lcm is n, when n is squarefree (card_pair_lcm_eq)

@[implicit_reducible]

instance PNat.instHasAntidiagonal : Finset.HasAntidiagonal (Additive ℕ+)

def Nat.finMulAntidiag (d n : ℕ) : Finset (Fin d → ℕ)

The Finset of all d-tuples of natural numbers whose product is n. Defined to be ∅ when n = 0.

@[simp]

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

@[simp]

theorem Nat.finMulAntidiag_zero_right (d : ℕ) : d.finMulAntidiag 0 = ∅

theorem Nat.finMulAntidiag_one {d : ℕ} : d.finMulAntidiag 1 = {fun (x : Fin d) => 1}

theorem Nat.finMulAntidiag_zero_left {n : ℕ} (hn : n ≠ 1) : finMulAntidiag 0 n = ∅

theorem Nat.dvd_of_mem_finMulAntidiag {n d : ℕ} {f : Fin d → ℕ} (hf : f ∈ d.finMulAntidiag n) (i : Fin d) : f i ∣ n

theorem Nat.ne_zero_of_mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} (hf : f ∈ d.finMulAntidiag n) (i : Fin d) : f i ≠ 0

theorem Nat.prod_eq_of_mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} (hf : f ∈ d.finMulAntidiag n) : ∏ i : Fin d, f i = n

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

theorem Nat.image_apply_finMulAntidiag {d n : ℕ} {i : Fin d} (hd : d ≠ 1) : Finset.image (fun (f : Fin d → ℕ) => f i) (d.finMulAntidiag n) = n.divisors

theorem Nat.image_piFinTwoEquiv_finMulAntidiag {n : ℕ} : Finset.image (⇑(piFinTwoEquiv fun (x : Fin 2) => ℕ)) (finMulAntidiag 2 n) = n.divisorsAntidiagonal

theorem Nat.finMulAntidiag_existsUnique_prime_dvd {d n p : ℕ} (hn : Squarefree n) (hp : p ∈ n.primeFactorsList) (f : Fin d → ℕ) (hf : f ∈ d.finMulAntidiag n) : ∃! i : Fin d, p ∣ f i

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

theorem Nat.finMulAntidiag_three {n : ℕ} (a : Fin 3 → ℕ) (ha : a ∈ finMulAntidiag 3 n) : a 0 * a 1 * a 2 = n

The following private declarations are ingredients for the proof of card_pair_lcm_eq.

theorem Nat.card_pair_lcm_eq {n : ℕ} (hn : Squarefree n) : {p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}.card = 3 ^ ArithmeticFunction.cardDistinctFactors n