Measure Theory ring Haar Char complex

lemma MeasureTheory.ringHaarChar_complex (z : ℂˣ) : ringHaarChar z = ‖(z : ℂ)‖₊ ^ 2 := by  -- We compute that `volume (x • ([0, 1] × [0, 1])) = ‖x‖₊ ^ 2 * volume ([0, 1] × [0, 1])`.  refine ringHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1 ×ℂ Icc 0 1) (μ := volume)    (measure_pos_of_nonempty_interior _ <| by simp [interior_reProdIm]).ne'    (isCompact_Icc.reProdIm isCompact_Icc).measure_ne_top ?_  -- The determinant of left multiplication by `z⁻¹` as a `ℝ`-linear map is `‖z‖₊ ^ (-2)`.  have key : ((LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ).det = ‖z.val‖₊ ^ (-2 : ℤ) := by    refine Complex.ofReal_injective ?_    rw [LinearMap.det_restrictScalars]    simp [Algebra.norm_complex_apply, normSq_eq_norm_sq, zpow_ofNat]  -- Massaging, we find the result.  convert addHaar_preimage_linearMap (E := ℂ) volume    (f := (LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ) _ _ using 2  · simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def, eq_comm]      using preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1)  · simp [key, ENNReal.ofReal_pow, zpow_ofNat]; rfl  · simp [key, zpow_ofNat]