nodup_primeFactorsList

Mathlib.Data.Nat.Squarefree

URI: https://scilib.ai/kg/mathlib#Squarefree.nodup_primeFactorsList

← MathLib Explorer

English

If n is squarefree, then its prime factors list is nodup.

Русский

Если n квадратно-простое, то у его списка простых множителей нет повторов.

LaTeX

$$$\\text{Squarefree}(n) \\Rightarrow n.primeFactorsList.Nodup$$$

Lean4

theorem nodup_primeFactorsList {n : ℕ} (hn : Squarefree n) : n.primeFactorsList.Nodup :=
  (Nat.squarefree_iff_nodup_primeFactorsList hn.ne_zero).mp hn

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

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

Разделы

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

Аффилиация

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