not_isPrimePow_zero

Mathlib.Algebra.IsPrimePow

URI: https://scilib.ai/kg/mathlib#not_isPrimePow_zero

← MathLib Explorer

English

No zero divisor ring has zero as a prime power.

Русский

В кольце без нулевых делителей ноль не является степенью простого числа.

LaTeX

$$$[NoZeroDivisors R] \;:\; \lnot \text{IsPrimePow } (0 : R)$$$

Lean4

theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R) :=
  by
  simp only [isPrimePow_def, not_exists, not_and', and_imp]
  intro x n _hn hx
  rw [pow_eq_zero hx]
  simp

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

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

Разделы

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

Аффилиация

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