case hx
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (fst (inr m)) • snd (inr m) = fst (inr m) • snd (inr m)
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ exp 𝕜 (inr m) = 1 + inr m
rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]
no goals
case hx
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (fst (inr m)) • snd (inr m) = fst (inr m) • snd (inr m)
rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]