GCD_of_Integer_and_Divisor
Provedgreatest-common-divisorproofwiki
Let a, b be positive integers. If a divides b then gcd(a, b) = a.
Preamble
import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem GCD_of_Integer_and_Divisor (a b : ℕ) (ha : 0 < a) (hb : 0 < b) (h : a ∣ b) : Nat.gcd a b = a := by sorry
Source