norm_num
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : -0 * 0 * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * 0 * b4 e * b6 e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 27 = 3 * 9
no goals