Theorem: MvPowerSeries.constantCoeff_smul (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
inst✝¹¹ : DecidableEq σ
A : Type u_2
inst✝¹⁰ : CommSemiring A
R✝ : Type u_3
inst✝⁹ : CommRing R✝
inst✝⁸ : Algebra A R✝
τ : Type u_4
inst✝⁷ : DecidableEq τ
S✝ : Type u_5
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra A S✝
inst✝⁴ : Algebra R✝ S✝
inst✝³ : IsScalarTower A R✝ S✝
R : Type u_6
inst✝² : Semiring R
S : Type u_7
inst✝¹ : Semiring S
inst✝ : Module R S
φ : MvPowerSeries σ S
a : R
⊢ (constantCoeff σ S) (a • φ) = a • (constantCoeff σ S) φ
Tactic:
rfl
State after:
no goals