Convolution with dual-number coefficients

WithConv.snd_comp_convMul computes the first-order coefficient of a convolution product. This product rule is used to differentiate the adjoint action.

theorem WithConv.snd_comp_convMul {R : Type u_1} {C : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [Semiring B] [Algebra R B] (f g : WithConv (C →ₗ[R] DualNumber B)) : ↑R (TrivSqZeroExt.sndHom B B) ∘ₗ (f * g).ofConv = (toConv ((TrivSqZeroExt.fstHom R B B).toLinearMap ∘ₗ f.ofConv) * toConv (↑R (TrivSqZeroExt.sndHom B B) ∘ₗ g.ofConv) + toConv (↑R (TrivSqZeroExt.sndHom B B) ∘ₗ f.ofConv) * toConv ((TrivSqZeroExt.fstHom R B B).toLinearMap ∘ₗ g.ofConv)).ofConv

The infinitesimal coefficient of a convolution product of dual-number-valued maps satisfies the product rule. No counit or coassociativity assumption is needed.