mem_factoredNumbers — Mathlib

English

An m belongs to factoredNumbers(s) iff m ≠ 0 and every prime divisor p of m lies in s.

Русский

Число m принадлежит factoredNumbers(s) тогда и только тогда, когда m ≠ 0 и каждый простый делитель m принадлежит s.

LaTeX

$$m ∈ \mathrm{factoredNumbers}(s) \iff m \neq 0 \wedge \forall p \in \mathrm{primeFactorsList}(m), p \in s$$

Lean4

theorem mem_factoredNumbers {s : Finset ℕ} {m : ℕ} : m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ∈ primeFactorsList m, p ∈ s :=
  Iff.rfl

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