case a
R : Type u
S : Type ?u.101158
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
⊢ coeff (map (Subring.subtype T) (toSubring p T hp)) n = coeff p n
R : Type u
S : Type ?u.101158
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
⊢ map (Subring.subtype T) (toSubring p T hp) = p
ext n
no goals
case a
R : Type u
S : Type ?u.101158
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
⊢ coeff (map (Subring.subtype T) (toSubring p T hp)) n = coeff p n
simp [coeff_map]