no goals
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ leadingCoeff (k • p) = k • leadingCoeff p
rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
  natDegree_smul_of_smul_regular p h]