How to prove ω (m * n) = ω m + ω n if m, n are coprime

Stream: new members

[Qingfeng Li]

import MathLib

open ArithmeticFunction
open Nat
open Finset
open IsMultiplicative

theorem cardDistinctFactors_coprime_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) (copri : m.Coprime n) : ω (m * n) = ω m + ω n := by
  sorry

When I prove some conbination problems, I met this problem : Is ω (m * n) = ω m + ω n for Coprime m n ? Where ω n denotes the number of distinct prime factors of n. I think it's trivial in math but it's not easy to prove in lean.

[Ruben Van de Velde]

import Mathlib

open ArithmeticFunction
open Nat
open Finset
open IsMultiplicative

theorem cardDistinctFactors_coprime_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) (copri : m.Coprime n) : ω (m * n) = ω m + ω n := by
  simp [ArithmeticFunction.cardDistinctFactors]
  have := Nat.perm_primeFactorsList_mul_of_coprime copri |>.dedup
  rw [this.length_eq]
  rw [List.Disjoint.dedup_append]
  · rw [List.length_append]
  exact coprime_primeFactorsList_disjoint copri

[Ruben Van de Velde]

You're welcome to submit this to mathlib