lcm_eq_zero_iff — Mathlib

English

If α is nontrivial, then s.lcm f = 0 if and only if there exists x in s with f(x) = 0.

Русский

Если α ненулевой, то s.lcm f = 0 тогда и только тогда, когда существует x ∈ s, такое что f(x) = 0.

LaTeX

$$$s.lcm f = 0 \iff \exists x \in s,\ f(x) = 0$$$

Lean4

@[simp]
theorem lcm_eq_zero_iff [Nontrivial α] : s.lcm f = 0 ↔ ∃ x ∈ s, f x = 0 := by
  simp only [lcm_def, Multiset.lcm_eq_zero_iff, Multiset.mem_map, mem_val]

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