ringExpChar — Mathlib

English

The unique exponential characteristic of a semiring is given by ringExpChar(R) = max(ringChar(R), 1).

Русский

Уникальная экспоненциальная характеристика полупрямого кольца равна max(ringChar(R), 1).

LaTeX

$$$\\\\mathrm{ringExpChar}(R) = \\max(\\\\mathrm{ringChar}(R), \\,1)$$$

Lean4

/-- Noncomputable function that outputs the unique exponential characteristic of a semiring. -/
noncomputable def ringExpChar : ℕ :=
  max (ringChar R) 1

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