cons_self_properDivisors

Mathlib.NumberTheory.Divisors

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

← MathLib Explorer

English

For n ≠ 0, cons n (properDivisors n) equals divisors n when viewed as a Finset.

Русский

Для n ≠ 0 конc n (properDivisors n) совпадает с divisors(n) как Finset.

LaTeX

$$$\mathrm{cons}\, n\, (\mathrm{properDivisors}(n)) = \mathrm{divisors}(n)\quad (n \neq 0)$$$

Lean4

theorem cons_self_properDivisors (h : n ≠ 0) : cons n (properDivisors n) self_notMem_properDivisors = divisors n := by
  rw [cons_eq_insert, insert_self_properDivisors h]

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

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

Разделы

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

Аффилиация

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