bigOmega_twohundredten
plain-language theorem explainer
Ω(210) equals 4, where Ω counts all prime factors with multiplicity. Number theorists using arithmetic functions for small composites or Möbius-related calculations would cite this concrete evaluation. The proof is a direct native decision that computes the cardFactors definition on the input 210.
Claim. $Ω(210) = 4$, where $Ω(n)$ is the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to Ω. The upstream definition states that bigOmega is the abbreviation for ArithmeticFunction.cardFactors, which returns the number of prime factors counted with multiplicity, denoted Ω(n). This places the result inside a setting that prepares basic interfaces before layering Dirichlet algebra or inversion formulas.
proof idea
One-line wrapper that applies native_decide to evaluate the cardFactors definition directly on 210.
why it matters
The declaration supplies a concrete numerical instance inside the arithmetic-functions module, which the module doc describes as providing Möbius footholds. It supports downstream checks on squarefree properties and inversion steps without requiring general lemmas. No parent theorems are listed in the used-by edges, so the result functions as a verified constant for 210 = 2·3·5·7 in the local library.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.