English
For any NonAssocRing R that is NoZeroDivisors and Nontrivial, either CharZero R holds or there exists p such that p.Prime and CharP R p.
Русский
Для любого NonAssocRing R, удовлетворяющего NoZeroDivisors и не тривиален, либо CharZero R, либо существует p, простое, такое что CharP R p.
LaTeX
$$CharZero R \lor \exists p:\mathbb{N}, \text{Prime } p \land CharP R p$$
Lean4
theorem exists' (R : Type*) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
CharZero R ∨ ∃ p : ℕ, Fact p.Prime ∧ CharP R p :=
by
obtain ⟨p, hchar⟩ := CharP.exists R
rcases char_is_prime_or_zero R p with h | rfl
exacts [Or.inr ⟨p, Fact.mk h, hchar⟩, Or.inl (charP_to_charZero R)]
