Documentation

Mathlib.Algebra.Order.Antidiag.Nat

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.finMulAntidiagonal.

Main Results #

source
instance PNat.instHasAntidiagonal :
Finset.HasAntidiagonal (Additive ℕ+)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
Instances For
    source
    @[simp]
    theorem Nat.mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} :
    f ∈ d.finMulAntidiag n ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0
    source
    @[simp]
    theorem Nat.finMulAntidiag_zero_right (d : ℕ) :
    d.finMulAntidiag 0 = ∅
    source
    theorem Nat.finMulAntidiag_one {d : ℕ} :
    d.finMulAntidiag 1 = {fun (x : Fin d) => 1}
    source
    theorem Nat.finMulAntidiag_zero_left {n : ℕ} (hn : n ≠ 1) :
    Nat.finMulAntidiag 0 n = ∅
    source
    theorem Nat.dvd_of_mem_finMulAntidiag {n d : ℕ} {f : Fin d → ℕ} (hf : f ∈ d.finMulAntidiag n) (i : Fin d) :
    f i ∣ n
    source
    theorem Nat.ne_zero_of_mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} (hf : f ∈ d.finMulAntidiag n) (i : Fin d) :
    f i ≠ 0
    source
    theorem Nat.prod_eq_of_mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} (hf : f ∈ d.finMulAntidiag n) :
    ∏ i : Fin d, f i = n
    source
    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)
    source
    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
    source
    theorem Nat.image_piFinTwoEquiv_finMulAntidiag {n : ℕ} :
    Finset.image (⇑(piFinTwoEquiv fun (x : Fin 2) => ℕ)) (Nat.finMulAntidiag 2 n) = n.divisorsAntidiagonal
    source
    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
    source
    theorem Nat.card_finMulAntidiag_of_squarefree {d n : ℕ} (hn : Squarefree n) :
    (d.finMulAntidiag n).card = d ^ ArithmeticFunction.cardDistinctFactors n