Coordinate product rule for divergence of a matrix acting on a vector.

theorem AVenhance.Infra.Section5.vecDiv_matrixMulVec {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LA : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} {LV : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => A y i j) (LA i j) x) (hV : HasFDerivAt V LV x) : vecDiv (fun (y : Homogenization.Vec 2) => (A y).mulVec (V y)) x = ∑ i : Fin 2, ∑ j : Fin 2, ((LA i j) (Homogenization.basisVec i) * V x j + A x i j * LV (Homogenization.basisVec i) j)

Divergence of a matrix-vector product, with the two derivative contributions displayed coordinatewise.