From d287a74723f4efc27ae712574b56df27bad46f08 Mon Sep 17 00:00:00 2001 From: Batixx Date: Mon, 27 Jul 2026 06:58:24 +0200 Subject: [PATCH] chore: remove misleading comment --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index d9ed9660d2ea58..c7bddb218368d8 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -68,8 +68,6 @@ namespace ContinuousLinearMap variable [CompleteSpace E] [CompleteSpace G] --- Note: made noncomputable to stop excess compilation --- https://github.com/leanprover-community/mathlib4/issues/7103 /-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric equivalence. -/