Grace/Cumulus/NumberTheory/LCM.g17

Open in Workbench Download source

Imports

GCDMore

Declarations

Source

1-- The least common multiple: defined from the greatest common divisor by2-- gcd(a, b) · lcm(a, b) = a · b, characterised as the least common multiple,3-- with its units, commutativity, associativity, and behaviour on coprime4-- numbers5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.NumberTheory.LCM11import GCDMore1213predicate IsLCM (a b m : Nat) :=14  a ∣ m ∧ b ∣ m ∧ (∀ c, Nat(c) → a ∣ c → b ∣ c → m ∣ c)1516theorem IsLCM.intro (a b m : Nat)17  requires left : a ∣ m18  requires right : b ∣ m19  requires least : ∀ c, Nat(c) → a ∣ c → b ∣ c → m ∣ c20  shows IsLCM(a, b, m)21proof22  exact ⟨left, right, least⟩2324theorem IsLCM.divides_left (a b m : Nat)25  requires lcm : IsLCM(a, b, m)26  shows a ∣ m27proof28  exact lcm.left2930theorem IsLCM.divides_right (a b m : Nat)31  requires lcm : IsLCM(a, b, m)32  shows b ∣ m33proof34  exact lcm.right.left3536theorem IsLCM.least (a b m c : Nat)37  requires lcm : IsLCM(a, b, m)38  requires left : a ∣ c39  requires right : b ∣ c40  shows m ∣ c41proof42  exact lcm.right.right with c, left, right4344theorem IsLCM.unique (a b m n : Nat)45  requires first : IsLCM(a, b, m)46  requires second : IsLCM(a, b, n)47  shows m = n48proof49  have forward := IsLCM.least at a, b, m, n50    with first, second.left, second.right.left51  have backward := IsLCM.least at a, b, n, m52    with second, first.left, first.right.left53  exact divides.antisymmetric with forward, backward5455theorem IsLCM.symmetric (a b m : Nat)56  requires lcm : IsLCM(a, b, m)57  shows IsLCM(b, a, m)58proof59  rcases lcm with ⟨left, right, least⟩60  refine ⟨right, left, _⟩61  intros c cNat first second62  exact least with c, second, first6364def lcm (a b : Nat) : Nat := quotientNat(a * b, gcd(a, b))6566theorem lcm.natural (a b : Nat)67  shows Nat(lcm(a, b))68proof69  unfold lcm70  exact quotientNat.natural at gcd(a, b), a * b7172theorem lcm.zero_left (b : Nat)73  shows lcm(0, b) = 074proof75  unfold lcm76  have zero : 0 * b = 0 by ring77  rw zero78  simp [quotientNat]7980theorem lcm.zero_right (a : Nat)81  shows lcm(a, 0) = 082proof83  unfold lcm84  have zero : a * 0 = 0 by ring85  rw zero86  simp [quotientNat]8788theorem lcm.commutative (a b : Nat)89  shows lcm(a, b) = lcm(b, a)90proof91  unfold lcm92  have commute := gcd.commutative at a, b93  have product : a * b = b * a by ring94  rw [commute, product]95  rfl9697theorem gcd.mul_lcm (a b : Nat)98  shows gcd(a, b) * lcm(a, b) = a * b99proof100  have split : gcd(a, b) = 0 ∨ gcd(a, b) ≠ 0 by tauto101  cases split with zero | nonzero102  . have both := gcd.zero_iff at a, b103    have zeros := both.forward with zero104    rcases zeros with ⟨aZero, bZero⟩105    rw [zero, aZero, bZero]106    ring107  . have multiple := gcd.divides_mul at a, b, b108    have equation := divides.quotient_equation at gcd(a, b), a * b109      with nonzero, multiple110    unfold lcm111    cc112113theorem lcm.mul_gcd (a b : Nat)114  shows lcm(a, b) * gcd(a, b) = a * b115proof116  have product := gcd.mul_lcm at a, b117  have commute : lcm(a, b) * gcd(a, b) = gcd(a, b) * lcm(a, b) by ring118  rw commute119  exact product120121-- The cofactors of a and b against their greatest common divisor are coprime.122theorem gcd.cofactor_coprime (a b p q : Nat)123  requires nonzero : gcd(a, b) ≠ 0124  requires left : gcd(a, b) * p = a125  requires right : gcd(a, b) * q = b126  shows gcd(p, q) = 1127proof128  have distribute := gcd.mul_left_distribute at p, q, gcd(a, b)129  rw [left, right] at distribute130  have products : gcd(a, b) * gcd(p, q) = gcd(a, b) * 1131    have one : gcd(a, b) * 1 = gcd(a, b) by ring132    rw one133    symm134    exact distribute135  exact mul.left_cancel_positive at gcd(p, q), 1, gcd(a, b)136    with nonzero, products137138theorem lcm.cofactor_form (a b p q : Nat)139  requires nonzero : gcd(a, b) ≠ 0140  requires left : gcd(a, b) * p = a141  requires right : gcd(a, b) * q = b142  shows lcm(a, b) = gcd(a, b) * p * q143proof144  have product := gcd.mul_lcm at a, b145  have form : gcd(a, b) * lcm(a, b) = gcd(a, b) * (gcd(a, b) * p * q)146    linear_combination product - a * right - (gcd(a, b) * q) * left147  exact mul.left_cancel_positive at lcm(a, b), gcd(a, b) * p * q, gcd(a, b)148    with nonzero, form149150theorem lcm.divides_left (a b : Nat)151  shows a ∣ lcm(a, b)152proof153  have split : gcd(a, b) = 0 ∨ gcd(a, b) ≠ 0 by tauto154  cases split with zero | nonzero155  . have both := gcd.zero_iff at a, b156    have zeros := both.forward with zero157    rcases zeros with ⟨aZero, bZero⟩158    rw [aZero, bZero]159    have value := lcm.zero_left at 0160    rw value161    exact divides.reflexive at 0162  . have product := gcd.mul_lcm at a, b163    obtain ⟨k, kNat, equation⟩ := gcd.divides_right at a, b164    have rearranged : gcd(a, b) * lcm(a, b) = gcd(a, b) * (a * k)165      linear_combination product - a * equation166    have cancelled := mul.left_cancel_positive at lcm(a, b), a * k, gcd(a, b)167      with nonzero, rearranged168    witness k169    symm170    exact cancelled171172theorem lcm.divides_right (a b : Nat)173  shows b ∣ lcm(a, b)174proof175  have commute := lcm.commutative at a, b176  rw commute177  exact lcm.divides_left at b, a178179theorem lcm.least (a b c : Nat)180  requires left : a ∣ c181  requires right : b ∣ c182  shows lcm(a, b) ∣ c183proof184  have split : gcd(a, b) = 0 ∨ gcd(a, b) ≠ 0 by tauto185  cases split with zero | nonzero186  . have both := gcd.zero_iff at a, b187    have zeros := both.forward with zero188    rcases zeros with ⟨aZero, bZero⟩189    rw aZero at left190    rw [aZero, bZero]191    have value := lcm.zero_left at 0192    rw value193    exact left194  . obtain ⟨p, pNat, pEquation⟩ := gcd.divides_left at a, b195    obtain ⟨q, qNat, qEquation⟩ := gcd.divides_right at a, b196    have cofactor := gcd.cofactor_coprime at a, b, p, q197      with nonzero, pEquation, qEquation198    have form := lcm.cofactor_form at a, b, p, q199      with nonzero, pEquation, qEquation200    obtain ⟨k, kNat, kEquation⟩ := left201    have scaled : gcd(a, b) * q ∣ gcd(a, b) * (p * k)202      rw qEquation203      have shape : gcd(a, b) * (p * k) = c204        linear_combination k * pEquation + kEquation205      rw shape206      exact right207    have cancelled := divides.mul_cancel_left at gcd(a, b), q, p * k208      with nonzero209    have reduced := cancelled.forward with scaled210    have dividesK := coprime.cancel at p, q, k with cofactor, reduced211    obtain ⟨m, mNat, mEquation⟩ := dividesK212    witness m213    rw form214    linear_combination (q * m) * pEquation + a * mEquation + kEquation215216theorem lcm.correct (a b : Nat)217  shows IsLCM(a, b, lcm(a, b))218proof219  have left := lcm.divides_left at a, b220  have right := lcm.divides_right at a, b221  refine ⟨left, right, _⟩222  intros c cNat first second223  exact lcm.least at a, b, c with first, second224225theorem lcm.unique (a b m : Nat)226  requires certificate : IsLCM(a, b, m)227  shows lcm(a, b) = m228proof229  have correct := lcm.correct at a, b230  exact IsLCM.unique with correct, certificate231232theorem lcm.divides_iff (a b c : Nat)233  shows lcm(a, b) ∣ c ↔ a ∣ c ∧ b ∣ c234proof235  constructor236  . intro h237    have left := lcm.divides_left at a, b238    have right := lcm.divides_right at a, b239    constructor240    . exact divides.transitive at a, lcm(a, b), c with left, h241    . exact divides.transitive at b, lcm(a, b), c with right, h242  . intro both243    rcases both with ⟨left, right⟩244    exact lcm.least at a, b, c with left, right245246theorem lcm.of_divides (a b : Nat)247  requires hab : a ∣ b248  shows lcm(a, b) = b249proof250  have reflexive := divides.reflexive at b251  have certificate : IsLCM(a, b, b)252    refine ⟨hab, reflexive, _⟩253    intros c cNat first second254    exact second255  exact lcm.unique with certificate256257theorem lcm.of_divides_right (a b : Nat)258  requires hba : b ∣ a259  shows lcm(a, b) = a260proof261  have commute := lcm.commutative at a, b262  rw commute263  exact lcm.of_divides at b, a with hba264265theorem lcm.one_left (a : Nat)266  shows lcm(1, a) = a267proof268  have one := one.divides at a269  exact lcm.of_divides with one270271theorem lcm.one_right (a : Nat)272  shows lcm(a, 1) = a273proof274  have one := one.divides at a275  exact lcm.of_divides_right with one276277theorem lcm.self (a : Nat)278  shows lcm(a, a) = a279proof280  have reflexive := divides.reflexive at a281  exact lcm.of_divides with reflexive282283theorem lcm.divides_mul (a b : Nat)284  shows lcm(a, b) ∣ a * b285proof286  have left := divides.mul_left_self at a, b287  have right := divides.mul_right_self at b, a288  exact lcm.least at a, b, a * b with left, right289290theorem lcm.zero_iff (a b : Nat)291  shows lcm(a, b) = 0 ↔ a = 0 ∨ b = 0292proof293  constructor294  . intro zero295    have product := gcd.mul_lcm at a, b296    rw zero at product297    have vanish : a * b = 0298      rw ← product299      ring300    have split := mul.eq_zero_iff at a, b301    exact split.forward with vanish302  . intro split303    cases split with aZero | bZero304    . rw aZero305      exact lcm.zero_left at b306    . rw bZero307      exact lcm.zero_right at a308309theorem lcm.nonzero (a b : Nat)310  requires left : a ≠ 0311  requires right : b ≠ 0312  shows lcm(a, b) ≠ 0313proof314  intro zero315  have split := lcm.zero_iff at a, b316  have alternatives := split.forward with zero317  cases alternatives with aZero | bZero318  . exact left with aZero319  . exact right with bZero320321theorem lcm.positive (a b : Nat)322  requires left : a ≠ 0323  requires right : b ≠ 0324  shows 0 < lcm(a, b)325proof326  have distinct := lcm.nonzero with left, right327  exact Less.positive_of_ne_zero with distinct328329theorem lcm.ge_left (a b : Nat)330  requires left : a ≠ 0331  requires right : b ≠ 0332  shows a ≤ lcm(a, b)333proof334  have multiple := lcm.divides_left at a, b335  have distinct := lcm.nonzero with left, right336  exact divides.le at a, lcm(a, b) with multiple, distinct337338theorem lcm.ge_right (a b : Nat)339  requires left : a ≠ 0340  requires right : b ≠ 0341  shows b ≤ lcm(a, b)342proof343  have multiple := lcm.divides_right at a, b344  have distinct := lcm.nonzero with left, right345  exact divides.le at b, lcm(a, b) with multiple, distinct346347theorem lcm.le_mul (a b : Nat)348  requires left : a ≠ 0349  requires right : b ≠ 0350  shows lcm(a, b) ≤ a * b351proof352  have multiple := lcm.divides_mul at a, b353  have distinct := mul.nonzero with left, right354  exact divides.le at lcm(a, b), a * b with multiple, distinct355356theorem lcm.coprime (a b : Nat)357  requires coprimeAB : gcd(a, b) = 1358  shows lcm(a, b) = a * b359proof360  have product := gcd.mul_lcm at a, b361  rw coprimeAB at product362  have one : 1 * lcm(a, b) = lcm(a, b) by ring363  rw one at product364  exact product365366theorem lcm.eq_mul_iff (a b : Nat)367  requires left : a ≠ 0368  requires right : b ≠ 0369  shows lcm(a, b) = a * b ↔ gcd(a, b) = 1370proof371  constructor372  . intro same373    have product := gcd.mul_lcm at a, b374    rw same at product375    have distinct := mul.nonzero with left, right376    have unit : gcd(a, b) * (a * b) = 1 * (a * b)377      rw product378      ring379    have swapLeft : gcd(a, b) * (a * b) = (a * b) * gcd(a, b) by ring380    have swapRight : 1 * (a * b) = (a * b) * 1 by ring381    rw [swapLeft, swapRight] at unit382    exact mul.left_cancel_positive at gcd(a, b), 1, a * b with distinct, unit383  . intro coprimeAB384    exact lcm.coprime with coprimeAB385386theorem gcd.divides_lcm (a b : Nat)387  shows gcd(a, b) ∣ lcm(a, b)388proof389  have left := gcd.divides_left at a, b390  have multiple := lcm.divides_left at a, b391  exact divides.transitive at gcd(a, b), a, lcm(a, b) with left, multiple392393theorem lcm.associative (a b c : Nat)394  shows lcm(lcm(a, b), c) = lcm(a, lcm(b, c))395proof396  have innerLeft := lcm.divides_left at a, b397  have innerRight := lcm.divides_right at a, b398  have outerLeft := lcm.divides_left at lcm(a, b), c399  have outerRight := lcm.divides_right at lcm(a, b), c400  have dividesA := divides.transitive at a, lcm(a, b), lcm(lcm(a, b), c)401    with innerLeft, outerLeft402  have dividesB := divides.transitive at b, lcm(a, b), lcm(lcm(a, b), c)403    with innerRight, outerLeft404  have dividesBC := lcm.least at b, c, lcm(lcm(a, b), c)405    with dividesB, outerRight406  have certificate : IsLCM(a, lcm(b, c), lcm(lcm(a, b), c))407    refine ⟨dividesA, dividesBC, _⟩408    intros d dNat dA dBC409    have left := lcm.divides_left at b, c410    have right := lcm.divides_right at b, c411    have dB := divides.transitive at b, lcm(b, c), d with left, dBC412    have dC := divides.transitive at c, lcm(b, c), d with right, dBC413    have dAB := lcm.least at a, b, d with dA, dB414    exact lcm.least at lcm(a, b), c, d with dAB, dC415  symm416  exact lcm.unique with certificate417418theorem lcm.mul_right_distribute (a b c : Nat)419  shows lcm(a * c, b * c) = lcm(a, b) * c420proof421  have split : c = 0 ∨ c ≠ 0 by tauto422  cases split with zero | nonzero423  . rw zero424    have left : a * 0 = 0 by ring425    have right : b * 0 = 0 by ring426    rw [left, right]427    have value := lcm.zero_left at 0428    rw value429    ring430  . have innerLeft := lcm.divides_left at a, b431    have innerRight := lcm.divides_right at a, b432    have reflexive := divides.reflexive at c433    have scaledLeft := divides.mul_mono at a, lcm(a, b), c, c434      with innerLeft, reflexive435    have scaledRight := divides.mul_mono at b, lcm(a, b), c, c436      with innerRight, reflexive437    have certificate : IsLCM(a * c, b * c, lcm(a, b) * c)438      refine ⟨scaledLeft, scaledRight, _⟩439      intros d dNat dA dB440      have cDivides := divides.of_mul_right at a, c, d with dA441      obtain ⟨e, eNat, eEquation⟩ := cDivides442      have shapeA : a * c ∣ e * c443        have commute : e * c = c * e by ring444        rw [commute, eEquation]445        exact dA446      have shapeB : b * c ∣ e * c447        have commute : e * c = c * e by ring448        rw [commute, eEquation]449        exact dB450      have cancelA := divides.mul_cancel_right at c, a, e with nonzero451      have cancelB := divides.mul_cancel_right at c, b, e with nonzero452      have eA := cancelA.forward with shapeA453      have eB := cancelB.forward with shapeB454      have least := lcm.least at a, b, e with eA, eB455      have scaled := divides.mul_mono at lcm(a, b), e, c, c456        with least, reflexive457      have commute : e * c = c * e by ring458      rw [commute, eEquation] at scaled459      exact scaled460    exact lcm.unique with certificate461462theorem lcm.mul_left_distribute (a b c : Nat)463  shows lcm(c * a, c * b) = c * lcm(a, b)464proof465  have left : c * a = a * c by ring466  have right : c * b = b * c by ring467  have product : lcm(a, b) * c = c * lcm(a, b) by ring468  rw [left, right, ← product]469  exact lcm.mul_right_distribute at a, b, c470