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)

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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 = Finset.filter (fun (f : Fin d → ℕ) => ∏ i : Fin d, f i = m) (Fintype.piFinset fun (x : Fin d) => n.divisors)

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

@[deprecated Nat.finMulAntidiag_existsUnique_prime_dvd (since := "2024-12-17")]

theorem Nat.finMulAntidiag_exists_unique_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

Alias of Nat.finMulAntidiag_existsUnique_prime_dvd.

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) : (Finset.filter (fun (p : ℕ × ℕ) => p.1.lcm p.2 = n) (n.divisors ×ˢ n.divisors)).card = 3 ^ ArithmeticFunction.cardDistinctFactors n