gcd_eq_zero_iff — Mathlib

English

The gcd of f over s equals 0 if and only if f(x) = 0 for every x in s.

Русский

НОД f над s равен нулю тогда и только тогда, когда для каждого x в s выполняется f(x) = 0.

LaTeX

$$$s.gcd\\, f = 0 \\iff \\forall x \\in s,\\ f(x) = 0$$$

Lean4

theorem gcd_eq_zero_iff : s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0 :=
  by
  rw [gcd_def, Multiset.gcd_eq_zero_iff]
  constructor <;> intro h
  · intro b bs
    apply h (f b)
    simp only [Multiset.mem_map]
    use b
    simp only [mem_def.1 bs, and_self]
  · intro a as
    rw [Multiset.mem_map] at as
    rcases as with ⟨b, ⟨bs, rfl⟩⟩
    apply h b (mem_def.1 bs)

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