mem_primeFactorsList' — Mathlib

English

For all n and p, p is in n.primeFactorsList iff p is prime, p divides n, and n is nonzero.

Русский

Для всех n и p: p принадлежит n.primeFactorsList тогда и только тогда, когда p простое, p делит n и n ≠ 0.

LaTeX

$$$p \in n.primeFactorsList \iff (Prime(p) \land p \mid n \land n \neq 0)$$$

Lean4

@[simp]
theorem mem_primeFactorsList' {n p} : p ∈ n.primeFactorsList ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
  cases n <;> simp [mem_primeFactorsList, *]

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