English
If p is prime and p ∉ s, then f(p^e · m) = f(p^e) · f(m) for multiplicative f and m ∈ factoredNumbers(s).
Русский
Если p простое и не принадлежит s, то для плоской функции f, удовлетворяющей умножению на coprime аргументы, выполняется f(p^e m) = f(p^e) f(m) при m ∈ factoredNumbers(s).
LaTeX
$$f(p^e m) = f(p^e) f(m) for all e ∈ ℕ and m ∈ factoredNumbers(s), provided hp : p.Prime and hs : p ∉ s$$
Lean4
/-- The sets of `s`-factored and of `s ∪ {N}`-factored numbers are the same when `N` is not prime.
See `Nat.equivProdNatFactoredNumbers` for when `N` is prime. -/
theorem factoredNumbers_insert (s : Finset ℕ) {N : ℕ} (hN : ¬N.Prime) :
factoredNumbers (insert N s) = factoredNumbers s := by
ext m
refine ⟨fun hm ↦ ⟨hm.1, fun p hp ↦ ?_⟩, fun hm ↦ ⟨hm.1, fun p hp ↦ Finset.mem_insert_of_mem <| hm.2 p hp⟩⟩
exact Finset.mem_of_mem_insert_of_ne (hm.2 p hp) fun h ↦ hN <| h ▸ prime_of_mem_primeFactorsList hp
