case a
A : Type ?u.488366
K : Type ?u.488369
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
n✝ : ℕ
⊢ coeff (map f (scaleRoots p x)) n✝ = coeff (scaleRoots (map f p) (↑f x)) n✝
A : Type ?u.488366
K : Type ?u.488369
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
⊢ map f (scaleRoots p x) = scaleRoots (map f p) (↑f x)
ext
no goals
case a
A : Type ?u.488366
K : Type ?u.488369
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
n✝ : ℕ
⊢ coeff (map f (scaleRoots p x)) n✝ = coeff (scaleRoots (map f p) (↑f x)) n✝
simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]