ringChar_ne_zero_of_finite

Mathlib.Algebra.CharP.Lemmas

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

English

In a finite ring, the ring's characteristic is nonzero.

Русский

В конечном кольце характеристика кольца ненулевая.

LaTeX

$$ringChar(R) ≠ 0$$

Lean4

theorem ringChar_ne_zero_of_finite [Finite R] : ringChar R ≠ 0 :=
  char_ne_zero_of_finite R (ringChar R)

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

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

Разделы

Аффилиация

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