English
If R is a finite ring with card R = p^n (p prime) and for all i ≤ n, (p^i) = 0 implies i = n, then CharP R (p^n).
Русский
Пусть R — конечное кольцо с_card(R) = p^n, где p простое, и если для любого i ≤ n из (p^i)=0 следует i=n, тогда CharP R (p^n).
LaTeX
$$CharP R (p^n)$$
Lean4
theorem charP_of_ne_zero (hn : card R = p) (hR : ∀ i < p, (i : R) = 0 → i = 0) : CharP R p where
cast_eq_zero_iff
n := by
have H : (p : R) = 0 := by rw [← hn, Nat.cast_card_eq_zero]
constructor
· intro h
rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
rw [Nat.dvd_iff_mod_eq_zero]
apply hR _ (Nat.mod_lt _ _) h
rw [← hn, Fintype.card_pos_iff]
exact ⟨0⟩
· rintro ⟨n, rfl⟩
rw [Nat.cast_mul, H, zero_mul]
