English
Let R be a ring with Fintype, p prime, card R = p^n, and the given condition that p^i = 0 implies i = n for all i ≤ n; then CharP R (p^n).
Русский
Пусть R кольцо с конечной мощностью, card(R) = p^n, p простое, и если p^i = 0 в R тогда i = n; тогда CharP R (p^n).
LaTeX
$$CharP R (p^n)$$
Lean4
theorem charP_of_prime_pow_injective (R) [Ring R] [Fintype R] (p n : ℕ) [hp : Fact p.Prime] (hn : card R = p ^ n)
(hR : ∀ i ≤ n, (p : R) ^ i = 0 → i = n) : CharP R (p ^ n) :=
by
obtain ⟨c, hc⟩ := CharP.exists R
have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
obtain ⟨i, hi, rfl⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn
obtain rfl : i = n := hR i hi <| by rw [← Nat.cast_pow, CharP.cast_eq_zero]
assumption
