no goals
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedCommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : NormedAlgebra 𝕜 R
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : Module 𝕜 M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalRing R
inst✝⁴ : TopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
⊢ snd (exp 𝕜 x) = exp 𝕜 (fst x) • snd x
rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]