case a
A : Type ?u.24205
K : Type ?u.24208
R : Type u_1
S : Type ?u.24214
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
s : R
n✝ : ℕ
⊢ coeff (scaleRoots 0 s) n✝ = coeff 0 n✝
A : Type ?u.24205
K : Type ?u.24208
R : Type u_1
S : Type ?u.24214
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
s : R
⊢ scaleRoots 0 s = 0
ext
no goals
case a
A : Type ?u.24205
K : Type ?u.24208
R : Type u_1
S : Type ?u.24214
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
s : R
n✝ : ℕ
⊢ coeff (scaleRoots 0 s) n✝ = coeff 0 n✝
simp