intCast — Mathlib

English

If integers a,b are coprime, then their images in any commutative ring R are coprime.

Русский

Если целые a и b взаимно просты, то их образы в любом коммутативном кольце R взаимно просты.

LaTeX

$$$IsCoprime(a,b) \Rightarrow IsCoprime(a \!:\mathbb{Z} \to R, b \!:\mathbb{Z} \to R)$$$

Lean4

theorem intCast {R : Type*} [CommRing R] {a b : ℤ} (h : IsCoprime a b) : IsCoprime (a : R) (b : R) :=
  by
  rcases h with ⟨u, v, H⟩
  use u, v
  rw_mod_cast [H]
  exact Int.cast_one

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