of_eq

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#ringChar.of_eq

English

If the ring characteristic of R equals p, then CharP R p holds.

Русский

Если характеристика кольца R равна p, то R имеет структуру CharP R p.

LaTeX

$$$ringChar R = p \rightarrow CharP R p$$$

Lean4

theorem of_eq {p : ℕ} (h : ringChar R = p) : CharP R p :=
  CharP.congr (ringChar R) h

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

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

Разделы

Аффилиация

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