dvd_of_dvd_mul_right_of_gcd_one — Mathlib

English

If a | b·c and gcd(a,b) = 1, then a | c.

Русский

Если a делит b·c и gcd(a,b) = 1, тогда a делит c.

LaTeX

$$$$a \\mid bc \\wedge \\gcd(a,b) = 1 \\Rightarrow a \\mid c.$$$$

Lean4

/-- Euclid's lemma: if `a ∣ b * c` and `gcd a b = 1` then `a ∣ c`.
Compare with `IsCoprime.dvd_of_dvd_mul_right` and
`UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors` -/
theorem dvd_of_dvd_mul_right_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a b = 1) : a ∣ c :=
  by
  rw [mul_comm] at habc
  exact dvd_of_dvd_mul_left_of_gcd_one habc hab

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