R : Type u_1
ι : Type ?u.22943
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : -1 = 1
⊢ ringChar R = 2
R : Type u_1
ι : Type ?u.22943
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ -1 = 1 ↔ ringChar R = 2
refine' ⟨fun h => _, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
R : Type u_1
ι : Type ?u.22943
inst✝¹ : Ring R
inst✝ : Nontrivial R
h✝ : 1 = -1
h : ↑(1 + 1) = 0
⊢ ringChar R = 2
R : Type u_1
ι : Type ?u.22943
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : -1 = 1
⊢ ringChar R = 2
rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
no goals
R : Type u_1
ι : Type ?u.22943
inst✝¹ : Ring R
inst✝ : Nontrivial R
h✝ : 1 = -1
h : ↑(1 + 1) = 0
⊢ ringChar R = 2
exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one