simp only [mul_zero, zero_mul, add_zero, ← pow_mul, sub_zero]
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ (e.a1 ^ 2 + 0 * 0 * e.a2) ^ 2 - 0 * 12 * b4 e = 0 ↔ e.a1 = 0
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a1 ^ (2 * 2) = 0 ↔ e.a1 = 0