English
Let R be a ring (with unity). If p and q are exponential characteristics of R, then p = q.
Русский
Пусть R — кольцо с единицей. Если p и q являются экспоненциальными характеристиками R, то p = q.
LaTeX
$$$\\\\forall R\\\\, \\\\[ \\\\ ExpChar R p \\\\to ExpChar R q \\\\to p = q \\\\]$$$
Lean4
/-- The exponential characteristic is unique. -/
theorem eq {p q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q :=
by
rcases hp with ⟨hp⟩ | ⟨hp'⟩
· rcases hq with hq | hq'
exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]
· rcases hq with hq | hq'
exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')), CharP.eq R ‹_› ‹_›]
