feat: charZero_iff_forall_prime_ne_zero (#6518)

Author: ChrisHughes24

Mathlib/Algebra/CharP/Basic.lean

@@ -732,3 +732,18 @@ theorem not_char_dvd (p : ℕ) [CharP R p] (k : ℕ) [h : NeZero (k : R)] : ¬p
 #align ne_zero.not_char_dvd NeZero.not_char_dvd
 
 end NeZero
+
+namespace CharZero
+
+theorem charZero_iff_forall_prime_ne_zero
+    [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
+    CharZero R ↔ ∀ p : ℕ, p.Prime → (p : R) ≠ 0 := by
+  refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
+  let p := ringChar R
+  cases CharP.char_is_prime_or_zero R p with
+  | inl hp => simpa using h p hp
+  | inr h =>
+    haveI : CharP R 0 := h ▸ inferInstance
+    exact CharP.charP_to_charZero R
+
+end CharZero