R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ False
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ringChar R ≠ 1
intro h
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 0 = 1
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ False
apply zero_ne_one' R
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 1 = 0
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 0 = 1
symm
no goals
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 1 = 0
rw [← Nat.cast_one, ringChar.spec, h]