gcd_ne_one_iff_gcd_mul_right_ne_one

English

For integers a, m, n, gcd(a, mn) ≠ 1 if and only if gcd(a,m) ≠ 1 or gcd(a,n) ≠ 1.

Русский

Для целых a, m, n, gcd(a, mn) ≠ 1 тогда и только тогда gcd(a, m) ≠ 1 или gcd(a, n) ≠ 1.

LaTeX

$$$\\gcd(a, mn) \\neq 1 \\iff \\gcd(a,m) \\neq 1 \\lor \\gcd(a,n) \\neq 1$.$$

Lean4

/-- If `gcd a (m * n) ≠ 1`, then `gcd a m ≠ 1` or `gcd a n ≠ 1`. -/
theorem gcd_ne_one_iff_gcd_mul_right_ne_one {a : ℤ} {m n : ℕ} : a.gcd (m * n) ≠ 1 ↔ a.gcd m ≠ 1 ∨ a.gcd n ≠ 1 := by
  simp only [← isCoprime_iff_gcd_eq_one, ← not_and_or, not_iff_not, IsCoprime.mul_right_iff]

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