primeFactorsList_subset_of_dvd

Mathlib.Data.Nat.Factors

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

← MathLib Explorer

English

If n ∣ k and k ≠ 0, then n.primeFactorsList ⊆ k.primeFactorsList.

Русский

Если n делится на k и k ≠ 0, то n.primeFactorsList ⊆ k.primeFactorsList.

LaTeX

$${n k : ℕ} (n ∣ k) (k ≠ 0) → n.primeFactorsList ⊆ k.primeFactorsList$$

Lean4

theorem primeFactorsList_subset_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : n.primeFactorsList ⊆ k.primeFactorsList :=
  (primeFactorsList_sublist_of_dvd h h').subset

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

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

Разделы

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

Аффилиация

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