grunweg
grunweg
AIUI, this is blocked on the author fixing the build failures - let me label it as such.
Thanks for the fast review!
Coming here from issue triage: what's the current state of this PR (except for the merge conflict)?
Coming here from issue triage: what's the current state of this PR?
Coming here from issue triage: it seems this PR is basically ready to go, except for merge conflicts. Would you like help with these?
Coming here for PR triage: I recently created a PR with LinearEquiv.prodUnique - so I care about that getting merged. I'm very happy for your PR to merge first, though....
This PR has been merged as #24168 now; hence, let me close this PR. Thanks for your work!
Coming here for PR triage: is this PR still relevant? (We certainly have to functionality now.)
I just labelled this PR with a best guess as to its current state. Feel free to adjust if you know better!
I wonder: would this be a good place to explain mathlib's deprecation policy? (After six months, deprecated declarations may be removed.) Yes, that is scope creep - but that is...