prime_one_false

Mathlib.Data.Nat.Prime.Defs

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

← MathLib Explorer

English

Prime 1 implies False.

Русский

Prime(1) ⇒ Ложь.

LaTeX

$$$\\\\mathrm{Prime}(1) \\\\rightarrow \\\\mathrm{False}$$$

Lean4

/-- A copy of `not_prime_one` stated in a way that works for `aesop`.

See https://github.com/leanprover-community/aesop/issues/197 for an explanation. -/
@[aesop safe destruct]
theorem prime_one_false : Prime 1 → False :=
  not_prime_one

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

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

Разделы

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

Аффилиация

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