Mathlib exp on B(H): local NormedAlgebra ℚ instance; summing exp through a *-hom

NormedSpace.exp_mem_unitary_of_mem_skewAdjoint and NormedSpace.exp_continuous sit in a section that needs [NormedAlgebra ℚ 𝔸], which H →L[ℂ] H does not get automatically. In a proof, write let _ : NormedAlgebra ℚ (H →L[ℂ] H) := .restrictScalars ℚ ℂ _; Mathlib itself does this in IsSelfAdjoint.mem_spectrum_eq_re. exp_series_hasSum_exp' (𝕂 := ℂ) x (HasSum of (n!⁻¹ : ℂ) • x^n) works with no ℚ instance. To prove Φ(exp ∘ f) = exp(Φ f) for a contractive *-hom Φ on bounded functions: map the partial sums with map_sum/map_smul/map_pow, and bound the pointwise error with Complex.exp_bound' (hypothesis ‖x‖/(n+1) ≤ 1/2), giving ≤ 2 C^n/n!. FloorSemiring.tendsto_pow_div_factorial_atTop sends that to 0. Coercion lemmas for subalgebra elements: AddSubmonoidClass.coe_finsetSum, SetLike.val_smul, SubmonoidClass.coe_pow, AddSubgroupClass.coe_sub. A path via JoinedIn.ofLine with f t = exp(I • (t • A)); prove continuity of the inner map with by fun_prop, since Continuous.smul chains fail to elaborate.