Distinct prime factors

Stream: new members

[Nathan]

I'm trying to prove something about distinct prime factors, and I'm stumped. How can I prove some basic things like the following?

import Mathlib.NumberTheory.ArithmeticFunction
open ArithmeticFunction.omega

example {a : ℕ} (ho : ω a = 1) : ∃ p n, Nat.Prime p ∧ a = p^n := sorry
example {a b : ℕ} (h : a.Coprime b) : ω (a * b) = (ω a) + (ω b) := sorry

[Yan Yablonovskiy 🇺🇦]

Unfortunately the best I could do for now

import Mathlib.NumberTheory.ArithmeticFunction
open ArithmeticFunction.omega

open ArithmeticFunction in
example {a b : ℕ} {ha: a ≠ 0} {hb : b ≠ 0} {hsa : Squarefree a} {hsb : Squarefree b} (h : a.Coprime b) :
    ω (a * b) = (ω a) + (ω b) := by
  simp [cardFactors_mul ha hb,(cardDistinctFactors_eq_cardFactors_iff_squarefree ha).mpr hsa,(cardDistinctFactors_eq_cardFactors_iff_squarefree hb).mpr hsb,(cardDistinctFactors_eq_cardFactors_iff_squarefree (show (a*b)≠0 by simp [ha,hb])).mpr (by simp [(Nat.squarefree_mul h).mpr ⟨hsa,hsb⟩]) ]

First I tried #loogle ArithmeticFunction.cardDistinctFactors, _ * _ which didnt get anywhere, then I tried ArithmeticFunction.cardFactors, _ * _ which found me something similar. Then i looked at ArithmeticFunction.cardFactors, ArithmeticFunction.cardDistinctFactors to see their relationship, and finally Squarefree ?a,Squarefree ?b, Squarefree (?a*?b) . Someone else might be able to assist you better but thats the sequence if thats helpful.

[Nathan]

i'm afraid i might have to look at deduped lists to actually solve these...

[Nathan]

what you wrote requires Squarefree

[Nathan]

like as premises

[Yan Yablonovskiy 🇺🇦]

Nathan said:

what you wrote requires Squarefree

Sadly yes, thats why i prefaced it with "Unfortunately the best I could do for now"

[Nathan]

:man_shrugging:

[Ruben Van de Velde]

Looking at ArithmeticFunction.cardDistinctFactors on loogle <https://loogle.lean-lang.org/?q=ArithmeticFunction.cardDistinctFactors> shows only 12 declarations, so it seems like we need to add some api

[Ruben Van de Velde]

import Mathlib
open ArithmeticFunction.omega

example {a : ℕ} (ho : ω a = 1) : ∃ p n, Nat.Prime p ∧ a = p^n := sorry
example {a b : ℕ} (h : a.Coprime b) : ω (a * b) = (ω a) + (ω b) := by
  simp [ArithmeticFunction.cardDistinctFactors]
  rw [Nat.perm_primeFactorsList_mul_of_coprime h |>.dedup |>.length_eq]
  rw [(Nat.coprime_primeFactorsList_disjoint h).dedup_append, List.length_append]

[Nathan]

thanks :) what's |>.?

[Ruben Van de Velde]

import Mathlib
open ArithmeticFunction.omega

example {a : ℕ} (ho : ω a = 1) : ∃ p n, Nat.Prime p ∧ a = p^n := by
  simp [ArithmeticFunction.cardDistinctFactors] at ho
  rw [List.length_eq_one_iff] at ho
  obtain ⟨p, hp⟩ := ho
  refine ⟨p, a.primeFactorsList.length, Nat.prime_of_mem_primeFactorsList (n := a) ?_, ?_⟩
  · rw [← List.mem_dedup, hp]
    simp
  · have : a ≠ 0 := by
      rintro rfl
      simp at hp
    apply Nat.eq_prime_pow_of_unique_prime_dvd this
    intro d hdp hddvd
    suffices d ∈ [p] by simp_all
    rwa [← hp, List.mem_dedup, Nat.mem_primeFactorsList_iff_dvd this hdp]

[Ruben Van de Velde]

Nat.perm_primeFactorsList_mul_of_coprime h |>.dedup means (Nat.perm_primeFactorsList_mul_of_coprime h).dedup but with fewer parentheses

[Ruben Van de Velde]

Better:

example {a : ℕ} : ω a = 1 ↔ IsPrimePow a := by
  rw [ArithmeticFunction.cardDistinctFactors_apply,
    isPrimePow_iff_card_primeFactors_eq_one,
    ← Nat.toFinset_factors, List.card_toFinset]

[Ruben Van de Velde]

#31585

[Nathan]

nice!!