not_weird

Mathlib.NumberTheory.FactorisationProperties

URI: https://scilib.ai/kg/mathlib#Nat.Prime.not_weird

English

If p is prime, then p is not weird.

Русский

Если p простое, то p не странное число.

LaTeX

$$$\operatorname{Prime}(n) \rightarrow \lnot \operatorname{Weird}(n)$$$

Lean4

theorem not_weird (h : Prime n) : ¬Weird n :=
  by
  simp only [Nat.Weird, not_and_or]
  left
  exact h.not_abundant

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

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

Разделы

Аффилиация

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