English
The characteristic equals the exponential characteristic iff the former is prime.
Русский
Характеристика равна экспоненциальной характеристике тогда и только тогда, когда сама характеристика простая.
LaTeX
$$$\\\\CharP R p \\\\Rightarrow ExpChar R q \\\\Rightarrow p = q \\\\Leftrightarrow p \\\\text{Prime}$$$
Lean4
/-- The characteristic equals the exponential characteristic iff the former is prime. -/
theorem char_eq_expChar_iff (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ p.Prime :=
by
rcases hq with q | hq_prime
· rw [(CharP.eq R hp (.ofCharZero R) : p = 0)]
decide
· exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩
