Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
perf(InnerProduct.Adjoint): speed up elaboration in two proofs (#11300)
For as yet un-completely diagnosed reasons, `unitary.star_mul_self_of_mem hu` for `(hu : u ∈ unitary (H →L[𝕜] H))` elaborates slowly thanks to `[1.068378s] ✅ ContinuousLinearMap.comp (ContinuousLinearMap.adjoint u) u =?= star ?a * ?b`. This PR pulls out the statements into `have`'s which speeds up the proofs significantly. #11299 documents the issue for future investigation.
- Loading branch information