-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Open
Description
Add a reassoc attribute for LinearMap lemmas so that we don't need to reassociate back and forth.
For example, if we have simp lemmas for f ∘ₗ g, then we want it to also apply for f ∘ₗ (g ∘ₗ h).
This was a TODO here:
| -- TODO: Add `reassoc` for `LinearMap`. Then we wouldn't need to reassociate back and forth. |
But #34312 golfed it, so that TODO doesn't apply anymore. But I think it's a good thing to do.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels