neg

Mathlib.RingTheory.Prime

URI: https://scilib.ai/kg/mathlib#Prime.neg

← MathLib Explorer

English

If p is a prime element in a commutative ring, then −p is also prime.

Русский

Если p — простой элемент в коммутативном кольце, то −p также прост.

LaTeX

$$$\forall p\, (Prime(p) \rightarrow Prime(-p))$$$

Lean4

theorem neg {p : α} (hp : Prime p) : Prime (-p) :=
  by
  obtain ⟨h1, h2, h3⟩ := hp
  exact ⟨neg_ne_zero.mpr h1, by rwa [IsUnit.neg_iff], by simpa [neg_dvd] using h3⟩

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

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

Разделы

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

Аффилиация

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