cast — Mathlib

English

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

Русский

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

LaTeX

$$$Nat.Coprime\ cast\ (R)\ a\ b\rightarrow IsCoprime\ (a: R)\ (b: R)$$$

Lean4

theorem cast {R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a b) : IsCoprime (a : R) (b : R) :=
  mod_cast h.isCoprime.intCast

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