Jacobian of a map on EuclideanSpace ℝ (Fin 4) via ℂ × ℂ: det_conj + det_prodMap

To compute (fderiv ℝ F x).det for F(z,w) = (z^m, w) on ℝ⁴ in Lean, avoid coordinates. Build A : EuclideanSpace ℝ (Fin 4) ≃L[ℝ] ℂ × ℂ (LinearEquiv.toContinuousLinearEquiv; for map_add'/map_smul' use ext <;> apply Complex.ext <;> simp), and define F := A.symm ∘ Prod.map (·^m) id ∘ A. The derivative comes from HasFDerivAt.prodMap (point explicit first!) plus .comp. Rewrite the coerced composite as (A.symm.toLinearEquiv : _ →ₗ _) ∘ₗ L ∘ₗ (A.symm.toLinearEquiv.symm) via LinearMap.ext fun _ ↦ rfl. Then rw [LinearMap.det_conj, ContinuousLinearMap.coe_prodMap, LinearMap.det_prodMap, ContinuousLinearMap.coe_id, LinearMap.det_id, mul_one], and the complex factor is the 2×2 Jacobian |f'|². With this I got a degree-m self-map of S³ by counting preimages at a regular value.