162theorem costSpectrumValue_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : 163 costSpectrumValue (m * n) = costSpectrumValue m + costSpectrumValue n := by
proof body
Term-mode proof.
164 unfold costSpectrumValue 165 rw [Nat.factorization_mul hm hn] 166 rw [Finsupp.sum_add_index'] 167 · intro p 168 simp 169 · intro p i j 170 push_cast 171 ring 172 173/-- The cost is nonnegative for any positive `n`. 174 Each summand `k · J(p) ≥ 0` by primality of `p`, so the sum is ≥ 0. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.