Commit 2024-05-05 19:07 1abe8819
View on Github →Add constantCoeff_smul to RingTheory.PowerSeries.Basic (#12616)
example : (constantCoeff ℝ) ((2:ℝ)•X) = 0 := by simp
simp doesn't solve the above because there is no lemma constantCoeff_smul tagged simp. This PR adds it to RingTheory.PowerSeries.Basic.