Skip to content

Commit

Permalink
fix (InnerProductSpace.Basic): make toSesqForm noncomputable (#6512)
Browse files Browse the repository at this point in the history
Explicitly marks `ContinuousLinearMap.toSesqForm` as `noncomputable` to prevent runaway build process which does produces nothing.
  • Loading branch information
mattrobball committed Aug 11, 2023
1 parent df08e0d commit cd15d65
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Mathlib/Analysis/InnerProductSpace/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1817,11 +1817,12 @@ namespace ContinuousLinearMap

variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace π•œ E']

-- Note: odd and expensive build behavior is explicitly turned off using `noncomputable`
set_option maxHeartbeats 500000 in
set_option synthInstance.maxHeartbeats 100000 in
/-- Given `f : E β†’L[π•œ] E'`, construct the continuous sesquilinear form `fun x y ↦ βŸͺx, A y⟫`, given
as a continuous linear map. -/
def toSesqForm : (E β†’L[π•œ] E') β†’L[π•œ] E' β†’L⋆[π•œ] E β†’L[π•œ] π•œ :=
noncomputable def toSesqForm : (E β†’L[π•œ] E') β†’L[π•œ] E' β†’L⋆[π•œ] E β†’L[π•œ] π•œ :=
(ContinuousLinearMap.flipβ‚—α΅’' E E' π•œ (starRingEnd π•œ) (RingHom.id π•œ)).toContinuousLinearEquiv ∘L
ContinuousLinearMap.compSL E E' (E' β†’L⋆[π•œ] π•œ) (RingHom.id π•œ) (RingHom.id π•œ) (innerSLFlip π•œ)
#align continuous_linear_map.to_sesq_form ContinuousLinearMap.toSesqForm
Expand Down

0 comments on commit cd15d65

Please sign in to comment.