Naturality of the derivative of the exponential

Continuous algebra homomorphisms intertwine the derivatives of the exponential. In particular, this transports the matrix derivative through a change of basis without differentiating a second exponential series.

theorem ContinuousAlgHom.map_expFDeriv {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [ContinuousSMul ℚ 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] (f : A →A[𝕜] B) (x y : A) : f ((TauCeti.expFDeriv 𝕜 x) y) = (TauCeti.expFDeriv 𝕜 (f x)) (f y)

Continuous algebra homomorphisms commute with the derivative of the exponential.