The derivative of the pullback of an alternating map along a composite

For f : F [⋀^ι]→L[𝕜] G and g : E →L[𝕜] F, Mathlib's ContinuousAlternatingMap.fderivCompContinuousLinearMap f g is the derivative of h ↦ f.compContinuousLinearMap h at g. In the direction B ∘ g of a composite with an endomorphism B of F, it is the pullback along g of the same derivative at the identity, which is the action of B on f as a derivation:

f.fderivCompContinuousLinearMap g (B ∘ g) = (f.fderivCompContinuousLinearMap id B) ∘ g.

This is the form in which the derivation action of the derivative of a vector field, the second term of the Lie derivative of a differential form, appears when a pullback along a flow is differentiated in time.

theorem ContinuousAlternatingMap.fderivCompContinuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [DecidableEq ι] (f : F [⋀^ι]→L[𝕜] G) (g : E →L[𝕜] F) (B : F →L[𝕜] F) : (f.fderivCompContinuousLinearMap g) (B ∘SL g) = ((f.fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 F)) B).compContinuousLinearMap g

The derivative of the pullback at g in the direction B ∘ g is the pullback along g of the derivative at the identity in the direction B.