isCoprime — Mathlib

English

In the given setting, IsRelPrime x y implies IsCoprime x y.

Русский

В заданной обстановке IsRelPrime x y подразумевает IsCoprime x y.

LaTeX

$$$\\\\mathrm{IsRelPrime}(x,y) \\\\Rightarrow \\\\mathrm{IsCoprime}(x,y)$$$

Lean4

theorem _root_.IsRelPrime.isCoprime (h : IsRelPrime x y) : IsCoprime x y :=
  by
  rw [← Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_sup_eq, ← Ideal.span_union, Set.singleton_union, ←
    span_gcd, Ideal.span_singleton_eq_top]
  exact h (gcd_dvd_left x y) (gcd_dvd_right x y)

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