gcd_to_nat — Mathlib

English

The gcd of ZNum numbers, when viewed as Nat, corresponds to the integer gcd after embedding back and forth between ZNum and integers.

Русский

НОД чисел ZNum, приведённый к Nat, соответствует целочисленному НОД после обратно-впередных преобразований между ZNum и целыми числами.

LaTeX

$$$\forall a,b:\; (a.gcd b : \mathbb{N}) = Int.gcd a b$$$

Lean4

@[simp]
theorem gcd_to_nat (a b) : (gcd a b : ℕ) = Int.gcd a b :=
  (Num.gcd_to_nat _ _).trans <| by simp only [abs_to_nat]; rfl

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