dvd_of_mem_primeFactorsList

Mathlib.Data.Nat.Factors

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

← MathLib Explorer

English

If h: p ∈ n.primeFactorsList, then p ∣ n.

Русский

Если h: p ∈ n.primeFactorsList, тогда p ∣ n.

LaTeX

$$$ \forall {n p}, (p \in n.primeFactorsList) \Rightarrow p \mid n $$$

Lean4

theorem dvd_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ∣ n :=
  by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · exact dvd_zero p
  · rwa [← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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