GCD_from_Congruence_Modulo_m
Provedgreatest-common-divisormodulo-arithmeticproofwiki
If a ≡ b (mod m), then gcd(a, m) = gcd(b, m).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem GCD_from_Congruence_Modulo_m (a b : ℤ) (m : ℕ) (h : (a - b) % m = 0) : Int.gcd a m = Int.gcd b m := by sorry
Source