dvd_of_dvd_mul_left_of_no_prime_factors

English

If a divides b c and a and c share no common prime factors, then a divides b.

Русский

Если a делит произведение b c и a и c не имеют общих простых делителей, то a делит b.

LaTeX

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

Lean4

/-- Euclid's lemma: if `a ∣ b * c` and `a` and `c` have no common prime factors, `a ∣ b`.
Compare `IsCoprime.dvd_of_dvd_mul_left`. -/
theorem dvd_of_dvd_mul_left_of_no_prime_factors {a b c : R} (ha : a ≠ 0) (h : ∀ ⦃d⦄, d ∣ a → d ∣ c → ¬Prime d) :
    a ∣ b * c → a ∣ b :=
  ((isRelPrime_iff_no_prime_factors ha).mpr h).dvd_of_dvd_mul_right

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