PR summary fad8d3adce

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

You should add API for doing things like replacing terms of short exact sequences with isomorphic terms/equal submodules, etc. Then this will be more useful in #32058

You should add API for doing things like replacing terms of short exact sequences with isomorphic terms/equal submodules, etc. Then this will be more useful in #32058

I disagree, this is a matter with Funtion.Exact for linear map, nothing to do with ModuleCat.
This PR already contain the ones do related to ModuleCat.

What do you mean? You can add all the general API that can be factored out from the long proof in #32058. You don't have to restrict yourself to ModuleCat. Of course, feel free to split the API additions into two PRs if you feel like there is a natural split.

I mean the inconvenience in #32058 is caused by two different things: 1: the things related with ModuleCat, which is already all in this PR, 2: the inconvenence of proving exactness for LinearMap, hopefully I'll soon open another PR for it.

Let us merge this now. Some additions may be useful in the future

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job