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