mk_isRelPrime_iff — Mathlib

English

IsRelPrime (Associates.mk a) (Associates.mk b) is equivalent to IsRelPrime a b.

Русский

IsRelPrime (Associates.mk a) (Associates.mk b) эквивалентно IsRelPrime a b.

LaTeX

$$$ \text{IsRelPrime}([a])\;\text{and}\;\text{IsRelPrime}([b]) \iff \text{IsRelPrime}(a,b) $$$

Lean4

@[simp]
theorem mk_isRelPrime_iff {a b : M} : IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b := by
  simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]

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