The part of a number with its prime factors in a set

Candidates for Mathlib.Data.Nat.Factors: the product of the prime factors of n that pass a test p, (n.primeFactorsList.filter p).prod, the part of n with its prime factors in a set (as Nat.prod_mem_factoredNumbers of Mathlib.NumberTheory.SmoothNumbers has it), is multiplicative, a divisor of n, 1 when no prime factor passes and n when all do; for the test (·.Coprime m) it is Nat.coprimePart n m, the largest divisor of n ≠ 0 prime to m.

Main definitions

• Nat.coprimePart: the product of the prime factors of n, with multiplicity, that are prime to m.

Main statements

• Nat.prod_filter_primeFactorsList_mul: the part of a b is the product of the parts of a and b; Nat.prod_filter_primeFactorsList_mul_of_forall: a factor a without a prime factor that passes leaves the part of b as it is.
• Nat.prod_filter_primeFactorsList_eq_one, Nat.prod_filter_primeFactorsList_eq_self: the part is 1 when no prime factor passes, and n when all do.
• Nat.prod_filter_primeFactorsList_dvd: the part divides n.
• Nat.coprimePart_dvd, Nat.coprime_coprimePart, Nat.dvd_coprimePart_of_dvd: the part of n prime to m divides n, is prime to m, and every divisor of n ≠ 0 prime to m divides it, so that it is the largest divisor of n prime to m.

Implementation notes

Nat.coprime_coprimePart and Nat.dvd_coprimePart_of_dvd use Nat.coprime_list_prod_left_iff and Nat.coprime_list_prod_right_iff of Mathlib.Data.Nat.GCD.BigOperators, which Mathlib.Data.Nat.Factors does not import.

theorem Nat.prod_filter_primeFactorsList_mul (p : ℕ → Bool) {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (List.filter p (a * b).primeFactorsList).prod = (List.filter p a.primeFactorsList).prod * (List.filter p b.primeFactorsList).prod

theorem Nat.prod_filter_primeFactorsList_eq_one {p : ℕ → Bool} {n : ℕ} (h : ∀ q ∈ n.primeFactorsList, p q = false) : (List.filter p n.primeFactorsList).prod = 1

theorem Nat.prod_filter_primeFactorsList_eq_self {p : ℕ → Bool} {n : ℕ} (hn : n ≠ 0) (h : ∀ q ∈ n.primeFactorsList, p q = true) : (List.filter p n.primeFactorsList).prod = n

theorem Nat.prod_filter_primeFactorsList_mul_of_forall {p : ℕ → Bool} {a b : ℕ} (ha : a ≠ 0) (h : ∀ q ∈ a.primeFactorsList, p q = false) : (List.filter p (a * b).primeFactorsList).prod = (List.filter p b.primeFactorsList).prod

Multiplying by a number without a prime factor that passes the test keeps the part of a number with its prime factors passing it.

theorem Nat.prod_filter_primeFactorsList_dvd (p : ℕ → Bool) (n : ℕ) : (List.filter p n.primeFactorsList).prod ∣ n

def Nat.coprimePart (n m : ℕ) : ℕ

The product of the prime factors of n, with multiplicity, that are prime to m: for n ≠ 0 the largest divisor of n prime to m (Nat.dvd_coprimePart_of_dvd).

Equations

• n.coprimePart m = (List.filter (fun (x : ℕ) => decide (x.Coprime m)) n.primeFactorsList).prod

theorem Nat.coprimePart_eq (n m : ℕ) : n.coprimePart m = (List.filter (fun (x : ℕ) => decide (x.Coprime m)) n.primeFactorsList).prod

theorem Nat.coprimePart_dvd (n m : ℕ) : n.coprimePart m ∣ n

theorem Nat.coprime_coprimePart (n m : ℕ) : (n.coprimePart m).Coprime m

theorem Nat.dvd_coprimePart_of_dvd {n m d : ℕ} (hn : n ≠ 0) (hd : d ∣ n) (hdm : d.Coprime m) : d ∣ n.coprimePart m

The largest divisor prime to m. Every divisor of n ≠ 0 prime to m divides Nat.coprimePart n m, since it is prime to the other prime factors of n, which divide m.