[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
⊢ 2 = 0
[PROOFSTEP]
rw [← Nat.cast_two, CharP.cast_eq_zero]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ x + x = 0
[PROOFSTEP]
rw [← two_smul R x, two_eq_zero, zero_smul]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
⊢ bit0 = 0
[PROOFSTEP]
funext
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
x✝ : R
⊢ bit0 x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
exact add_self_eq_zero _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ bit0 x = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
⊢ bit1 = 1
[PROOFSTEP]
funext
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
x✝ : R
⊢ bit1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
simp [bit1]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ bit1 x = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ -x = x
[PROOFSTEP]
rw [neg_eq_iff_add_eq_zero, ← two_smul R x, two_eq_zero, zero_smul]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x - y = x + y
[PROOFSTEP]
rw [sub_eq_add_neg, neg_eq]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) * (x + y) = x * x + y * y
[PROOFSTEP]
rw [← pow_two, ← pow_two, ← pow_two, add_sq]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : List R
⊢ List.sum l * List.sum l = List.sum (List.map (fun x => x * x) l)
[PROOFSTEP]
simp_rw [← pow_two, list_sum_sq]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : Multiset R
⊢ Multiset.sum l * Multiset.sum l = Multiset.sum (Multiset.map (fun x => x * x) l)
[PROOFSTEP]
simp_rw [← pow_two, multiset_sum_sq]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
s : Finset ι
f : ι → R
⊢ (∑ i in s, f i) * ∑ i in s, f i = ∑ i in s, f i * f i
[PROOFSTEP]
simp_rw [← pow_two, sum_sq]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ -1 = 1 ↔ ringChar R = 2
[PROOFSTEP]
refine' ⟨fun h => _, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : -1 = 1
⊢ ringChar R = 2
[PROOFSTEP]
rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h 
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
h✝ : 1 = -1
h : ↑(1 + 1) = 0
⊢ ringChar R = 2
[PROOFSTEP]
exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one
[GOAL]
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ orderOf (-1) = if ringChar R = 2 then 1 else 2
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1
[PROOFSTEP]
rw [neg_one_eq_one_iff.2 h, orderOf_one]
[GOAL]
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2
[PROOFSTEP]
apply orderOf_eq_prime
[GOAL]
case neg.hg
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1
[PROOFSTEP]
simp
[GOAL]
case neg.hg1
R : Type u_1
ι : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1
[PROOFSTEP]
simpa [neg_one_eq_one_iff] using h
