isRelPrime_iff_no_prime_factors — Mathlib

English

For nonzero a, a and b are relatively prime if and only if no prime divides both a and b.

Русский

Для ненулевого a и любого b, взаимно просты тогда и только тогда, когда никакое простое не делит и a, и b.

LaTeX

$$$a \neq 0 \Rightarrow \mathrm{IsRelPrime}(a,b) \iff \forall d, d \mid a \rightarrow d \mid b \rightarrow \lnot \mathrm{Prime}(d).$$$

Lean4

theorem isRelPrime_iff_no_prime_factors {a b : R} (ha : a ≠ 0) : IsRelPrime a b ↔ ∀ ⦃d⦄, d ∣ a → d ∣ b → ¬Prime d :=
  ⟨fun h _ ha hb ↦ (·.not_unit <| h ha hb), fun h ↦
    WfDvdMonoid.isRelPrime_of_no_irreducible_factors (ha ·.1) fun _ irr ha hb ↦
      h ha hb (UniqueFactorizationMonoid.irreducible_iff_prime.mp irr)⟩

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