Review

leanprover-community · Feb 21, 2025 · f023af2 · f023af2
1 parent 4139f61
commit f023af2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Analysis/Complex/Isometry.lean b/Mathlib/Analysis/Complex/Isometry.lean
@@ -41,7 +41,7 @@ rotation. -/
 def rotation : Circle →* ℂ ≃ₗᵢ[ℝ] ℂ where
   toFun a :=
     { DistribMulAction.toLinearEquiv ℝ ℂ a with
-      norm_map' := fun x => show ‖a * x‖ = ‖x‖ by
+      norm_map' x := show ‖a * x‖ = ‖x‖ by
         rw [norm_mul, Circle.norm_coe, one_mul] }
   map_one' := LinearIsometryEquiv.ext <| by simp
   map_mul' a b := LinearIsometryEquiv.ext <| mul_smul a b