Review

leanprover-community · Sep 2, 2023 · ff02d50 · ff02d50
1 parent 95b2f22
commit ff02d50
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean
@@ -47,7 +47,6 @@ theorem volume_preserving_equiv_real_prod : MeasurePreserving measurableEquivRea
   (volume_preserving_finTwoArrow ℝ).comp volume_preserving_equiv_pi
 #align complex.volume_preserving_equiv_real_prod Complex.volume_preserving_equiv_real_prod
 
-instance : Measure.IsAddHaarMeasure (@volume ℂ Complex.measureSpace) :=
-  Measure.MapLinearEquiv.isAddHaarMeasure _ _
+instance : Measure.IsAddHaarMeasure (@volume ℂ _) := Measure.MapLinearEquiv.isAddHaarMeasure _ _
 
 end Complex