R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ AlgHom.range (mapAlg R S)
⊢ r • p ∈ AlgHom.range (mapAlg R S)
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ lifts (algebraMap R S)
⊢ r • p ∈ lifts (algebraMap R S)
rw [mem_lifts_iff_mem_alg] at hp⊢
no goals
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ AlgHom.range (mapAlg R S)
⊢ r • p ∈ AlgHom.range (mapAlg R S)
exact Subalgebra.smul_mem (mapAlg R S).range hp r