abs

Mathlib.RingTheory.Prime

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

English

If p is prime in a ring with a linear order, then |p| is also prime.

Русский

Если p — простое в кольце с линейным порядком, то |p| тоже простое.

LaTeX

$$$\text{Prime}(p) \Rightarrow \text{Prime}(|p|)$$$

Lean4

theorem abs [LinearOrder α] {p : α} (hp : Prime p) : Prime (abs p) :=
  by
  obtain h | h := abs_choice p <;> rw [h]
  · exact hp
  · exact hp.neg

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

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

Разделы

Аффилиация

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