map — Mathlib

English

If x and y are coprime in R and f: R →+* S is a ring hom, then f(x) and f(y) are coprime in S.

Русский

Если элементы x и y в R взаимно просты и имеется кольцевое отображение f: R →+* S, то их изображения f(x) и f(y) в S взаимно просты.

LaTeX

$$$\exists a,b\in R\,(a x + b y = 1) \Rightarrow \exists a',b'\in S\,(a' f(x) + b' f(y) = 1)$$$

Lean4

theorem map (H : IsCoprime x y) {S : Type v} [CommSemiring S] (f : R →+* S) : IsCoprime (f x) (f y) :=
  let ⟨a, b, h⟩ := H
  ⟨f a, f b, by rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]⟩

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