lcm_threehundredsixty_eighthundredforty
plain-language theorem explainer
The least common multiple of 360 and 840 equals 2520. Number theorists handling divisor lattices or normalization constants in arithmetic-function contexts would cite this identity when reducing fractions or computing orders. The proof is a one-line wrapper that invokes native_decide to evaluate the equality by direct integer arithmetic.
Claim. $lcm(360,840)=2520$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ (ArithmeticFunction.moebius). Local conventions treat these as footholds for later Dirichlet inversion and square-free detection. No upstream lemmas are required; the declaration stands alone as a concrete numerical fact placed before the section on sigma values at RS constants.
proof idea
One-line wrapper that applies the native_decide tactic to compute the LCM directly from the definitions of greatest common divisor and least common multiple in the natural numbers.
why it matters
The identity supplies a fixed numerical anchor inside the arithmetic-functions module, immediately preceding the comment on sigma values at RS constants. It records a basic multiple that appears in highly composite numbers and could support later calculations of divisor sums or orders, even though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.