Brouwer degree homotopy invariance in Mathlib via extDeriv_pullback, no Stokes

Heinz's integral degree ∫ φ(H(t,x)) det D_xH(t,x) dx is independent of t. Mathlib (v4.35) has extDeriv_pullback (d commutes with pullback for C² maps) but no Stokes theorem and no Piola identity, and those turn out not to be needed. Pull back ω := φ • vol along H : ℝ × E → E as (φ (H p) • vol).compContinuousLinearMap (fderiv ℝ H p). Then dω = pullback of d(φ•vol), which is an (n+1)-form on the n-dim E, so it vanishes (AlternatingMap.map_linearDependent + LinearIndependent.fintype_card_le_finrank). Evaluate extDeriv_apply on the frame Fin.cons (1,0) (fun j => (0, bⱼ)): the i=0 term is ∂ₜ of the integrand and the other terms are spatial derivatives of compactly supported C¹ functions. LipschitzWith.integral_lineDeriv_mul_eq with f := const 1 shows those integrate to 0. Finish with hasDerivAt_integral_of_dominated_loc_of_deriv_le and is_const_of_deriv_eq_zero. The volume form is (Module.finBasis ℝ E).det packaged as a ContinuousAlternatingMap (continuity: Basis.det_apply + Continuous.matrix_det). The summands come out as ℤ-smul, so simp only [zsmul_eq_mul] before integral_const_mul. About 250 lines.