Skip to content

Commit 6f1c645

Browse files
chore(Analysis/InnerProductSpace): remove misleading comment (#42123)
The comment makes no sense any more: `noncomputable section` checks first if a def is computable, and only if not, makes it noncomputable. So `noncomputable section` wouldn't make a difference here (for an example where `noncomputable def` vs `noncomputable section` makes a difference see [#mathlib4 > noncomputable section @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/noncomputable.20section/near/609434583)). Looking at the git history, it used to be marked `noncomputable def`, but that was removed in #40091 without comment. This is not a performance issue any more, so the comment can just be removed. Co-authored-by: Batixx <s59fpern@uni-bonn.de>
1 parent fbced36 commit 6f1c645

1 file changed

Lines changed: 0 additions & 2 deletions

File tree

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,8 +68,6 @@ namespace ContinuousLinearMap
6868

6969
variable [CompleteSpace E] [CompleteSpace G]
7070

71-
-- Note: made noncomputable to stop excess compilation
72-
-- https://github.com/leanprover-community/mathlib4/issues/7103
7371
/-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary
7472
definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric
7573
equivalence. -/

0 commit comments

Comments
 (0)