gcd_eq_zero_iff — Mathlib

English

The gcd equals zero exactly when every element of the multiset is zero.

Русский

НОД равен нулю тогда и только тогда, когда каждый элемент мультисета равен нулю.

LaTeX

$$$s.\mathrm{gcd} = 0 \iff \forall x \in s,\ x = 0$$$

Lean4

theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x ∈ s, x = 0 :=
  by
  constructor
  · intro h x hx
    apply eq_zero_of_zero_dvd
    rw [← h]
    apply gcd_dvd hx
  · refine s.induction_on ?_ ?_
    · simp
    intro a s sgcd h
    simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]

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