R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.42950
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
b : { x // x ∈ M }
hb : ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
i : ℕ
⊢ ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.42950
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
b : { x // x ∈ M }
hb : ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
i : ℕ
⊢ coeff (Polynomial.map (algebraMap R S) (integerNormalization M p)) i = coeff (↑b • p) i
rw [coeff_map, coeff_smul]
no goals
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.42950
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
b : { x // x ∈ M }
hb : ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
i : ℕ
⊢ ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
exact hb i