R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).1
no goals
R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
exact CharP.cast_eq_zero_iff R (ringChar R)