Splitting a gcd at a prime

Write two natural numbers as p ^ a * m' and p ^ b * n' with p dividing neither m' nor n'. Their gcd then splits into the gcd of the p-free parts times p to the smaller of the two exponents:

gcd (p^a·m') (p^b·n') = gcd m' n' · p ^ min a b.

TauCeti.Nat.gcd_pow_mul_pow_mul is that statement for an arbitrary such splitting, and TauCeti.Nat.gcd_eq_gcd_ordCompl_mul_pow_min is its canonical instance, where the splitting is the one Nat.ordProj and Nat.ordCompl perform. TauCeti.Nat.gcd_ordCompl_lt draws the consequence that lets an induction on the gcd terminate: when p divides both arguments, passing to the p-free parts strictly shrinks the gcd.

Main results

• TauCeti.Nat.gcd_pow_mul_pow_mul: the gcd splits at a prime, for an explicit splitting.
• TauCeti.Nat.gcd_eq_gcd_ordCompl_mul_pow_min: the same for the ordProj/ordCompl splitting.
• TauCeti.Nat.gcd_ordCompl_lt: removing the p-part strictly shrinks the gcd.

theorem TauCeti.Nat.gcd_pow_mul_pow_mul {p a b m' n' : ℕ} (hp : Nat.Prime p) (hm' : ¬p ∣ m') (hn' : ¬p ∣ n') : (p ^ a * m').gcd (p ^ b * n') = m'.gcd n' * p ^ min a b

The gcd splits at a prime. If p divides neither m' nor n', then the p-free part of gcd (p^a·m') (p^b·n') is gcd m' n' and its p-part is p ^ min a b.

No positivity is asked of m' or n': ¬p ∣ m' already forces m' ≠ 0, since every prime divides 0.

theorem TauCeti.Nat.gcd_eq_gcd_ordCompl_mul_pow_min {p m n : ℕ} (hp : Nat.Prime p) (hm : m ≠ 0) (hn : n ≠ 0) : m.gcd n = (m / p ^ m.factorization p).gcd (n / p ^ n.factorization p) * p ^ min (m.factorization p) (n.factorization p)

The gcd splits at a prime, canonically:

gcd m n = gcd (ordCompl[p] m) (ordCompl[p] n) · p ^ min (v_p m) (v_p n)

for nonzero m and n — the gcd of the p-free parts, times p to the smaller of the two p-adic valuations.

theorem TauCeti.Nat.gcd_ordCompl_lt {p m n : ℕ} (hp : Nat.Prime p) (hm : m ≠ 0) (hn : n ≠ 0) (hpm : p ∣ m) (hpn : p ∣ n) : (m / p ^ m.factorization p).gcd (n / p ^ n.factorization p) < m.gcd n

Removing the p-part strictly shrinks the gcd, when p divides both arguments:

gcd (ordCompl[p] m) (ordCompl[p] n) < gcd m n.

This is what lets an induction along TauCeti.Nat.gcd_eq_gcd_ordCompl_mul_pow_min terminate.