[Merged by Bors] - feat(linear_algebra/{multilinear,alternating): add of_subsingleton #9196
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This was refactored from the
koszul_cx
branch, something I mentioned doing in this Zulip thread.The original version was:
but I decided to remove the
f : M →ₗ[R] N
argument as it can be added later with(of_subsingleton R M i).comp_linear_map f
.Co-authored-by: Amelia Livingston al3717@ic.ac.uk
Link to the original:
mathlib/src/m4r/Koszul_eq_free_Koszul.lean
Lines 80 to 86 in df4221e