theorem proved term proof

`omega_mul_of_coprime`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 264theorem omega_mul_of_coprime {m n : ℕ} (_hm : m ≠ 0) (_hn : n ≠ 0) (h : Nat.Coprime m n) :
 265    omega (m * n) = omega m + omega n := by

proof body

Term-mode proof.

 266  simp only [omega]
 267  exact ArithmeticFunction.cardDistinctFactors_mul h
 268
 269/-- Ω (number of prime factors with multiplicity) is additive: Ω(mn) = Ω(m) + Ω(n). -/

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use