mem_primeFactors_of_ne_zero

Mathlib.Data.Nat.PrimeFin

URI: https://scilib.ai/kg/mathlib#Nat.mem_primeFactors_of_ne_zero

English

If n ≠ 0, then p ∈ primeFactors(n) iff p is prime and p divides n.

Русский

Если n ≠ 0, то p ∈ primeFactors(n) эквивалентно p простое и p делит n.

LaTeX

$$$n \neq 0 \Rightarrow (p \in n.\text{primeFactors} \iff (p.\text{Prime} \land p \mid n))$$$

Lean4

theorem mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by simp [hn]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru