intCast_mul_natCast_gcdA_eq_gcd — Mathlib

English

For any natural n, in a ring R of characteristic p, one has (n * gcdA(p) ) cast to R equals gcd(n,p) cast to R.

Русский

Для натурального n в кольце R характеристики p выполняется (n · gcdA(p)) ⟼ R = gcd(n,p) ⟼ R.

LaTeX

$$$(n * n.gcdA p : R) = (n.gcd p : R)$$$

Lean4

theorem intCast_mul_natCast_gcdA_eq_gcd (n : ℕ) : (n * n.gcdA p : R) = n.gcd p :=
  by
  suffices ↑(n * n.gcdA p + p * n.gcdB p : ℤ) = ((n.gcd p : ℤ) : R) by simpa using this
  rw [← Nat.gcd_eq_gcd_ab]

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