expChar_center_iff — Mathlib

English

The exponent-Char property of the center equals that of the whole ring.

Русский

Свойство экспоненциальной характеристической Char-параметр центра равно параметру всего кольца.

LaTeX

$$$\\mathrm{ExpChar}(\\mathrm{Subring.center} R) p \\iff \\mathrm{ExpChar}(R) p$$$

Lean4

theorem expChar_center_iff {R : Type u} [Ring R] {p : ℕ} : ExpChar (Subring.center R) p ↔ ExpChar R p :=
  (algebraMap (Subring.center R) R).expChar_iff Subtype.val_injective p

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