ringChar_zero_iff_CharZero

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#CharP.ringChar_zero_iff_CharZero

English

For any CharP R p in a nontrivial ring, p ≠ 1.

Русский

Для любого CharP R p в не нулевом кольце p ≠ 1.

LaTeX

$$$p \neq 1$$$

Lean4

theorem ringChar_zero_iff_CharZero : ringChar R = 0 ↔ CharZero R := by rw [ringChar.eq_iff, charP_zero_iff_charZero]

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

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

Разделы

Аффилиация

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