gcd_eq_zero_iff — Mathlib

English

In a CancelCommMonoidWithZero α with GCDMonoid structure, gcd(a,b) = 0 iff a = 0 and b = 0.

Русский

В GCD-моноде α: gcd(a,b) = 0 тогда и только тогда, когда a = 0 и b = 0.

LaTeX

$$$$ \gcd(a,b) = 0 \ \Longleftrightarrow\ \ (a = 0) \land (b = 0) $$$$

Lean4

@[simp]
theorem gcd_eq_zero_iff [GCDMonoid α] (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b = 0 :=
  Iff.intro
    (fun h => by
      let ⟨ca, ha⟩ := gcd_dvd_left a b
      let ⟨cb, hb⟩ := gcd_dvd_right a b
      rw [h, zero_mul] at ha hb
      exact ⟨ha, hb⟩)
    fun ⟨ha, hb⟩ => by
    rw [ha, hb, ← zero_dvd_iff]
    apply dvd_gcd <;> rfl

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