IndisputableMonolith.NumberTheory.Primes.GCDLCM

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3
   4/-!
   5# GCD/LCM utilities (prime-friendly)
   6
   7This file centralizes small gcd/lcm algebra lemmas we’ll reuse across the primes framework.
   8Most statements are already in Mathlib, but we expose stable wrappers in our namespace.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace NumberTheory
  13namespace Primes
  14
  15open Nat
  16
  17/-- If `a` and `b` are coprime, then `lcm a b = a * b`. -/
  18theorem coprime_lcm_eq_mul (a b : ℕ) (h : Nat.Coprime a b) : Nat.lcm a b = a * b := by
  19  have hgcd : Nat.gcd a b = 1 := h
  20  simpa [hgcd] using (Nat.gcd_mul_lcm a b)
  21
  22/-- `gcd a b * lcm a b = a * b` (a standard arithmetic identity). -/
  23theorem gcd_mul_lcm (a b : ℕ) : Nat.gcd a b * Nat.lcm a b = a * b := by
  24  exact Nat.gcd_mul_lcm a b
  25
  26/-! ### Casted lcm formulas (for analytic work) -/
  27
  28/-- A casted form of `gcd_mul_lcm`:
  29\[
  30(\gcd(a,b) : \mathbb{Q}) \cdot (\operatorname{lcm}(a,b) : \mathbb{Q}) = (a b : \mathbb{Q}).
  31\]
  32-/
  33theorem gcd_mul_lcm_cast (a b : ℕ) :
  34    (Nat.gcd a b : ℚ) * (Nat.lcm a b : ℚ) = (a * b : ℚ) := by
  35  norm_cast
  36  exact gcd_mul_lcm a b
  37
  38/-- For `gcd(a,b) ≠ 0`, we can solve for `lcm` in `ℚ`:
  39\[
  40(\operatorname{lcm}(a,b) : \mathbb{Q}) = \frac{ab}{\gcd(a,b)}.
  41\]
  42-/
  43theorem lcm_cast_eq_mul_div_gcd (a b : ℕ) (h : Nat.gcd a b ≠ 0) :
  44    (Nat.lcm a b : ℚ) = (a * b : ℚ) / (Nat.gcd a b : ℚ) := by
  45  have hgcd_q : (Nat.gcd a b : ℚ) ≠ 0 := by
  46    exact_mod_cast h
  47  -- Multiply both sides by `gcd` and use `gcd_mul_lcm_cast`.
  48  apply (mul_left_cancel₀ hgcd_q)
  49  -- LHS: gcd * lcm ; RHS: gcd * (ab/gcd) = ab
  50  -- Use `gcd_mul_lcm_cast` and `mul_div_cancel₀`.
  51  calc
  52    (Nat.gcd a b : ℚ) * (Nat.lcm a b : ℚ)
  53        = (a * b : ℚ) := gcd_mul_lcm_cast a b
  54    _ = (Nat.gcd a b : ℚ) * ((a * b : ℚ) / (Nat.gcd a b : ℚ)) := by
  55        -- `gcd * (ab / gcd) = ab`
  56        symm
  57        simpa [div_eq_mul_inv, mul_assoc] using (mul_div_cancel₀ (a := (a * b : ℚ)) hgcd_q)
  58
  59end Primes
  60end NumberTheory
  61end IndisputableMonolith
  62