GCD_with_Zero
Provedgreatest-common-divisorproofwiki
Let a be a nonzero integer. Then gcd(a, 0) = |a|.
Preamble
import Mathlib.Data.Int.GCD
Formal statement
theorem GCD_with_Zero (a : ℤ) (ha : a ≠ 0) : Int.gcd a 0 = Int.natAbs a := by sorry
Source
Let a be a nonzero integer. Then gcd(a, 0) = |a|.
import Mathlib.Data.Int.GCD
theorem GCD_with_Zero (a : ℤ) (ha : a ≠ 0) : Int.gcd a 0 = Int.natAbs a := by sorry