Theorem: MvPowerSeries.eval₂_C (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

State before:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
r : R
⊢ eval₂ φ a ((C σ R) r) = φ r
Tactic:
rw [← coe_C, eval₂_coe hφ ha, MvPolynomial.eval₂_C]
State after:
no goals