R : Type u
S : Type ?u.105459
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
n : ℕ
⊢ coeff p n = 0 → 0 = ↑(coeff p n)
R : Type u
S : Type ?u.105459
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
n : ℕ
⊢ coeff (ofSubring T p) n = ↑(coeff p n)
simp only [ofSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
  ite_eq_right_iff, Ne.def, ite_not, Classical.not_not, ite_eq_left_iff]
R : Type u
S : Type ?u.105459
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
n : ℕ
h : coeff p n = 0
⊢ 0 = ↑(coeff p n)
R : Type u
S : Type ?u.105459
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
n : ℕ
⊢ coeff p n = 0 → 0 = ↑(coeff p n)
intro h
no goals
R : Type u
S : Type ?u.105459
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
n : ℕ
h : coeff p n = 0
⊢ 0 = ↑(coeff p n)
rw [h, ZeroMemClass.coe_zero]