gcd_greatest — Mathlib

English

Русский

LaTeX

$$$\forall a,b,d \in \mathbb{N},\; d \mid a \land d \mid b \land (\forall e \in \mathbb{N}, (e \mid a \land e \mid b) \rightarrow e \mid d) \Longrightarrow d = \gcd(a,b).$$$

Lean4

theorem gcd_greatest {a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ e : ℕ, e ∣ a → e ∣ b → e ∣ d) : d = a.gcd b :=
  (dvd_antisymm (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)) (dvd_gcd hda hdb)).symm

Похожие утверждения