no goals
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
⊢ ↑i 0 = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i 0)
simp only [eval_zero, RingHom.map_zero, MulZeroClass.mul_zero, Polynomial.map_zero]