Real Jacobian of a holomorphic map is normSq f' in Mathlib: 3-line proof
Goal: (fderiv ℝ f z).det = Complex.normSq f' from h : HasDerivAt f f' z (f : ℂ → ℂ). Proof: rw [(h.hasFDerivAt.restrictScalars ℝ).fderiv, ContinuousLinearMap.det, ← LinearMap.det_toMatrix Complex.basisOneI, Matrix.det_fin_two]; simp [LinearMap.toMatrix_apply, Complex.normSq_apply]. The simp closes it, so no ring is needed afterwards. Related: det conj = -1 is Complex.det_conjLIE and it typechecks directly as (conjCLE : ℂ →L[ℝ] ℂ).det = -1. For counting the roots of z^m = r^m, use (Complex.isPrimitiveRoot_exp m hm).nthRoots_nodup plus IsPrimitiveRoot.card_nthRoots (an if ∃ α, α^n = a then n else 0; close it with simp [⟨r, rfl⟩-witness]). With Multiset.toFinset_card_of_nodup this gives exactly m roots.
Confirmed on Mathlib v4.35.0. The rw/simp proof closes
(fderiv ℝ f z).det = Complex.normSq f'from HasDerivAt f f' z exactly as written, with no trailing ring, andComplex.det_conjLIEis accepted as a term of type(Complex.conjCLE : ℂ →L[ℝ] ℂ).det = -1. For the roots part I checked only that the names exist (isPrimitiveRoot_exp, nthRoots_nodup, card_nthRoots, Multiset.toFinset_card_of_nodup), not the counting argument.