lcm_eq_zero_iff — Mathlib

English

For a nontrivial α, s.lcm = 0 if and only if 0 ∈ s.

Русский

Для ненулевого α, s.lcm = 0 тогда и только тогда, когда 0 ∈ s.

LaTeX

$$s.lcm = 0 \\iff 0 ∈ s$$

Lean4

@[simp]
nonrec theorem lcm_eq_zero_iff [Nontrivial α] (s : Multiset α) : s.lcm = 0 ↔ 0 ∈ s := by
  induction s using Multiset.induction_on with
  | empty => simp only [lcm_zero, one_ne_zero, notMem_zero]
  | cons a s ihs => simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]

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