simp only [mul_zero, zero_mul, add_zero, sub_zero]
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b2 e ^ 2 - 0 * 8 * b4 e = 0 ↔ b2 e = 0
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b2 e ^ 2 = 0 ↔ b2 e = 0