RelativeError: pointwise size of the Piola vector

theorem AVenhance.Infra.Section5.RelativeError.spatialGradientMatrix_mulVec_eq_fderiv {F : Homogenization.Vec 2 → Homogenization.Vec 2} (x v : Homogenization.Vec 2) : Matrix.mulVec (FaaDiBruno.spatialGradientMatrix F x) v = (fderiv ℝ F x) v

The gradient matrix acts on a vector as the Fréchet derivative does.