squarefree_of_dvd_prodPrimes

Mathlib.NumberTheory.SelbergSieve

URI: https://scilib.ai/kg/mathlib#BoundingSieve.squarefree_of_dvd_prodPrimes

English

If a natural number d divides the product of primes s.prodPrimes, then d is squarefree.

Русский

Если d делит произведение простых s.prodPrimes, то d квадратно свободен.

LaTeX

$$$d \\mid s.prodPrimes \\Rightarrow \\operatorname{Squarefree}(d)$$$

Lean4

theorem squarefree_of_dvd_prodPrimes {d : ℕ} (hd : d ∣ s.prodPrimes) : Squarefree d :=
  Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree

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

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

Разделы

Аффилиация

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