issue !4#11299: Slow unification of `ContinuousLinearMap....

Stream: triage

[Random Issue Bot]

Today I chose issue 11299 for discussion!

Slow unification of ContinuousLinearMap.comp (ContinuousLinearMap.adjoint) and star *
Created by @Matthew Robert Ballard (@mattrobball) on 2024-03-11
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

I thought I'd have a look at this but

import Mathlib.Analysis.InnerProductSpace.Adjoint

variable {𝕜 : Type*} [RCLike 𝕜] {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
  [CompleteSpace H] {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x : H)

count_heartbeats in -- 736
#check unitary.star_mul_self_of_mem hu

is now quick. Is the problem now resolved?

[Johan Commelin]

Is it still quick if you import all of mathlib? If so please comment on the issue. Probably semi-interesting to figure out what made it quick, before closing.
(On mobile, so I can't test it myself right now.)