ne_zero

Mathlib.Algebra.IsPrimePow

URI: https://scilib.ai/kg/mathlib#IsPrimePow.ne_zero

English

If n is a prime power in a domain without zero divisors, then n ≠ 0.

Русский

Если n — степень простого в кольце без нулевых делителей, то n ≠ 0.

LaTeX

$$$[NoZeroDivisors R] \; {n} \; (IsPrimePow n) \rightarrow n \neq 0$$$

Lean4

theorem ne_zero [NoZeroDivisors R] {n : R} (h : IsPrimePow n) : n ≠ 0 := fun t => not_isPrimePow_zero (t ▸ h)

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

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

Разделы

Аффилиация

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