isCoprime_span_singleton_iff — Mathlib

English

IsCoprime span{x} span{y} ⇔ IsCoprime x y.

Русский

IsCoprime span{x} span{y} ⇔ IsCoprime x y.

LaTeX

$$$$ IsCoprime(\operatorname{span}\{x\}, \operatorname{span}\{y\}) \iff IsCoprime(x,y) $$$$

Lean4

theorem isCoprime_span_singleton_iff (x y : R) :
    IsCoprime (span <| singleton x) (span <| singleton y) ↔ IsCoprime x y :=
  by
  simp_rw [isCoprime_iff_codisjoint, codisjoint_iff, eq_top_iff_one, mem_span_singleton_sup, mem_span_singleton]
  constructor
  · rintro ⟨a, _, ⟨b, rfl⟩, e⟩; exact ⟨a, b, mul_comm b y ▸ e⟩
  · rintro ⟨a, b, e⟩; exact ⟨a, _, ⟨b, rfl⟩, mul_comm y b ▸ e⟩

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