Lax Lean Archive

Proof of `The determinant of the least-common-multiple matrix` (1st statement)

groundedproofs/Lax426240Proofs/LcmDeterminant.lean · lax-426240

What this proof establishes

no assumptions

thm✓Lax426240.LcmDeterminant (1st statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

lcm(i,j)=i⋅(1/gcd(i,j))⋅jlcm(i,j) = i · (1/gcd(i,j)) · j factors the matrix as DSDD S D; Smith's determinant for SS with 1/m=∑d∣mg(d)1/m = ∑_{d ∣ m} g(d) (Möbius inversion) gives the product.