charP — Mathlib

English

Let R be a non-associative semiring. Then R has a CharP structure with modulus equal to its ring character, i.e. CharP R (ringChar R).

Русский

Пусть R — полукольцо без ассоциаций. Тогда у R есть структура CharP с модулем, равным его характеристике ringChar R, то есть CharP R (ringChar R).

LaTeX

$$$CharP\,R\,(ringChar\,R)$$$

Lean4

instance (priority := low) charP : CharP R (ringChar R) :=
  ⟨spec R⟩

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