English
In a commutative ring α with IsDomain and NormalizedGCDMonoid, if a divides b−c, then gcd(a,b) = gcd(a,c).
Русский
В коммутативном кольце α, IsDomain и нормализованном gcd-монойде, если a ∣ (b−c), то gcd(a,b) = gcd(a,c).
LaTeX
$$$$ a,b,c \\in \\alpha,\\ a \\mid (b-c) \\Rightarrow \\gcd(a,b) = \\gcd(a,c). $$$$
Lean4
theorem gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c :=
by
apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;> rw [dvd_gcd_iff] <;>
refine ⟨gcd_dvd_left _ _, ?_⟩
· rcases h with ⟨d, hd⟩
rcases gcd_dvd_right a b with ⟨e, he⟩
rcases gcd_dvd_left a b with ⟨f, hf⟩
use e - f * d
rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
· rcases h with ⟨d, hd⟩
rcases gcd_dvd_right a c with ⟨e, he⟩
rcases gcd_dvd_left a c with ⟨f, hf⟩
use e + f * d
rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
