primeFactorsList_sorted

Mathlib.Data.Nat.Factors

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

English

The list primeFactorsList n is sorted in nondecreasing order.

Русский

Список primeFactorsList n упорядочен по неубыванию.

LaTeX

$$$ \text{List.Sorted} \bigl( (\le) \bigr) (\text{primeFactorsList}(n)) $$$

Lean4

theorem primeFactorsList_sorted (n : ℕ) : List.Sorted (· ≤ ·) (primeFactorsList n) :=
  (isChain_primeFactorsList _).pairwise

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

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

Разделы

Аффилиация

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