rwa [pow_eq_zero_iff] at hdisc
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 ^ (2 * 2) = 0
⊢ e.a3 = 0
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 ^ (2 * 2) = 0
⊢ 0 < 2 * 2