Grace/Cumulus/NumberTheory/CoprimeSquares.g17

Open in Workbench Download source

Imports

LCM · PerfectSquares

Declarations

Source

1-- Coprime factors of a square are squares: a divisor whose square divides2-- a square divides its root, and when a * b is a square with gcd(a, b) = 13-- both a and b are squares4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.CoprimeSquares10import LCM11import PerfectSquares1213-- A divisor of a is coprime to b whenever a is.14theorem coprime.of_divides_left (a b g : Nat)15  requires coprimeAB : gcd(a, b) = 116  requires divides : g ∣ a17  shows gcd(g, b) = 118proof19  have every := gcd.eq_one_iff at g, b20  apply every.backward21  intros d dNat dg db22  have da := divides.transitive at d, g, a with dg, divides23  exact coprime.divisor_one at a, b, d with coprimeAB, da, db2425-- If d² divides c², then d divides c.26theorem divides.of_mul_self (d c : Nat)27  requires squares : d * d ∣ c * c28  shows d ∣ c29proof30  have split : c = 0 ∨ c ≠ 0 by tauto31  cases split with zero | nonzero32  . rw zero33    exact divides.zero at d34  . have gcdNonzero := gcd.nonzero_right at d, c with nonzero35    obtain ⟨p, pNat, dShape⟩ := gcd.divides_left at d, c36    obtain ⟨q, qNat, cShape⟩ := gcd.divides_right at d, c37    have cofactors := gcd.cofactor_coprime at d, c, p, q38      with gcdNonzero, dShape, cShape39    have squareNonzero := mul.nonzero at gcd(d, c), gcd(d, c)40      with gcdNonzero, gcdNonzero41    have cancel := divides.mul_cancel_left42      at gcd(d, c) * gcd(d, c), p * p, q * q with squareNonzero43    have regroup : gcd(d, c) * gcd(d, c) * (p * p) ∣44        gcd(d, c) * gcd(d, c) * (q * q)45      have leftSide : gcd(d, c) * gcd(d, c) * (p * p) = d * d by ring [dShape]46      have rightSide : gcd(d, c) * gcd(d, c) * (q * q) = c * c by ring [cShape]47      rw [leftSide, rightSide]48      exact squares49    have cofactorSquares := cancel.forward with regroup50    have pDivides := divides.of_mul_left at p, p, q * q with cofactorSquares51    have coprimeSquare := coprime.pow_right at p, q, 2 with cofactors52    have two := pow.two at q53    rw two at coprimeSquare54    have pSelf := divides.reflexive at p55    have pOne := coprime.divisor_one at p, q * q, p56      with coprimeSquare, pSelf, pDivides57    rw pOne at dShape58    have unit : gcd(d, c) * 1 = gcd(d, c) by ring59    rw unit at dShape60    rw ← dShape61    exact gcd.divides_right at d, c6263-- A coprime factor of a square is a square: with g = gcd(a, c), a = g p and64-- c = g q, the equation a b = c² reduces to p b = g q², and the coprimality65-- of p with q² and of g with b force p ∣ g and g ∣ p, so a = g².66theorem IsSquare.left_of_coprime_mul (a b c : Nat)67  requires coprimeAB : gcd(a, b) = 168  requires product : a * b = c * c69  shows IsSquare(a)70proof71  have split : a = 0 ∨ a ≠ 0 by tauto72  cases split with zero | nonzero73  . rw zero74    exact IsSquare.zero75  . have gcdNonzero := gcd.nonzero at a, c with nonzero76    obtain ⟨p, pNat, aShape⟩ := gcd.divides_left at a, c77    obtain ⟨q, qNat, cShape⟩ := gcd.divides_right at a, c78    have cofactors := gcd.cofactor_coprime at a, c, p, q79      with gcdNonzero, aShape, cShape80    have reduced : p * b = gcd(a, c) * (q * q)81      have expanded : gcd(a, c) * (p * b) = gcd(a, c) * (gcd(a, c) * (q * q))82        have leftSide : gcd(a, c) * (p * b) = a * b by ring [aShape]83        have rightSide : gcd(a, c) * (gcd(a, c) * (q * q)) = c * c84          ring [cShape]85        rw [leftSide, rightSide]86        exact product87      exact mul.left_cancel_positive at p * b, gcd(a, c) * (q * q), gcd(a, c)88        with gcdNonzero, expanded89    have coprimeSquare := coprime.pow_right at p, q, 2 with cofactors90    have two := pow.two at q91    rw two at coprimeSquare92    have pDividesProduct : p ∣ gcd(a, c) * (q * q)93      rw ← reduced94      exact divides.mul_left_self at p, b95    have coprimeSquareP := coprime.symmetric at p, q * q with coprimeSquare96    have pDivides := coprime.cancel_right at q * q, p, gcd(a, c)97      with coprimeSquareP, pDividesProduct98    have gDividesA := gcd.divides_left at a, c99    have coprimeGB := coprime.of_divides_left at a, b, gcd(a, c)100      with coprimeAB, gDividesA101    have gDividesProduct : gcd(a, c) ∣ p * b102      rw reduced103      exact divides.mul_left_self at gcd(a, c), q * q104    have coprimeBG := coprime.symmetric at gcd(a, c), b with coprimeGB105    have gDivides := coprime.cancel_right at b, gcd(a, c), p106      with coprimeBG, gDividesProduct107    have equal := divides.antisymmetric at p, gcd(a, c) with pDivides, gDivides108    rw equal at aShape109    witness gcd(a, c)110    symm111    exact aShape112113theorem IsSquare.of_coprime_mul (a b c : Nat)114  requires coprimeAB : gcd(a, b) = 1115  requires product : a * b = c * c116  shows IsSquare(a) ∧ IsSquare(b)117proof118  constructor119  . exact IsSquare.left_of_coprime_mul at a, b, c with coprimeAB, product120  . have coprimeBA := coprime.symmetric at a, b with coprimeAB121    have commuted : b * a = c * c122      rw ← product123      ring124    exact IsSquare.left_of_coprime_mul at b, a, c with coprimeBA, commuted125