prime_zero_false

Mathlib.Data.Nat.Prime.Defs

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

← MathLib Explorer

English

Prime 0 implies False.

Русский

Prime(0) ⇒ Ложь.

LaTeX

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

Lean4

/-- A copy of `not_prime_zero` 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_zero_false : Prime 0 → False :=
  not_prime_zero

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

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

Разделы

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

Аффилиация

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