Slow unification of ContinuousLinearMap.comp (ContinuousLinearMap.adjoint) and star *
#11299
Comments
mattrobball
changed the title
ContinuousLinearMap.comp (ContinuousLinearMap.adjoint) and star *
mathlib-bors bot
pushed a commit
that referenced
this issue
Mar 11, 2024
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.
kbuzzard
pushed a commit
that referenced
this issue
Mar 12, 2024
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.
dagurtomas
pushed a commit
that referenced
this issue
Mar 22, 2024
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.
utensil
pushed a commit
that referenced
this issue
Mar 26, 2024
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.
Louddy
pushed a commit
that referenced
this issue
Apr 15, 2024
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.
uniwuni
pushed a commit
that referenced
this issue
Apr 19, 2024
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.
callesonne
pushed a commit
that referenced
this issue
Apr 22, 2024
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In
Mathlib.Analysis.InnerProductSpace.Unitary,unitary.star_mul_self_of_mem hufor(hu : u ∈ unitary (H →L[𝕜] H))elaborates slowly thanks to slow unification checks[1.068378s] ✅ ContinuousLinearMap.comp (ContinuousLinearMap.adjoint u) u =?= star ?a * ?b.The text was updated successfully, but these errors were encountered: