gcd_coe — Mathlib

English

For positive integers n and m, the greatest common divisor of n and m, when viewed as a natural number, equals the standard gcd of n and m in the natural numbers.

Русский

Пусть n и m — положительные целые числа; НОД(n, m), взятый как обычное натуральное число, совпадает с обычным НОД(n, m) в ℕ.

LaTeX

$$$ (\\\\gcd n m : \\\\mathbb{N}) = \\\\operatorname{Nat.gcd}(n, m) $$$

Lean4

@[simp, norm_cast]
theorem gcd_coe (n m : ℕ+) : (gcd n m : ℕ) = Nat.gcd n m :=
  rfl

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