Skip to content

[Merged by Bors] - feat: algebraic properties of LinearMap.compMultilinear#17932

Closed
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/compMultilinear
Closed

[Merged by Bors] - feat: algebraic properties of LinearMap.compMultilinear#17932
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/compMultilinear

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Oct 18, 2024 •
edited
Loading

This also demotes LinearMap.compAlternatingMap to a plain function, for consistency.

To make up for this loss, it introduces LinearMap.compAlternatingMapₗ as the stronger linear version.

Open in Gitpod

@eric-wieser
feat: algebraic properties of LinearMap.compMultilinear
69f1798 
This also demotes `LinearMap.compAlternatingMap` to a plain function, for consistency.
@eric-wieser eric-wieser added the t-algebra Algebra (groups, rings, fields, etc) label Oct 18, 2024
@eric-wieser eric-wieser requested a review from urkud October 18, 2024 23:25
@eric-wieser eric-wieser mentioned this pull request Oct 18, 2024
Closed
4 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 18, 2024 •
edited
Loading

PR summary a644005b86

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.LinearMap.compMultilinearMapₗ
+ add_compAlternatingMap
+ add_compMultilinearMap
+ compAlternatingMap_add
+ compAlternatingMap_smul
+ compAlternatingMap_zero
+ compAlternatingMapₗ
+ compMultilinearMap_add
+ compMultilinearMap_smul
+ compMultilinearMap_zero
+ smul_compAlternatingMap
+ smul_compMultilinearMap
+ zero_compAlternatingMap
+ zero_compMultilinearMap

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

The doc-module for script/declarations_diff.sh contains some details about this script.

urkud
urkud reviewed Oct 19, 2024
View reviewed changes
Mathlib/LinearAlgebra/Alternating/Basic.lean
variable (S) in
/-- `LinearMap.compAlternatingMap` as an `S`-linear map. -/
@[simps]
def compAlternatingMapₗ [Semiring S] [Module S N] [Module S N₂]
Copy link
Copy Markdown
Member

@urkud urkud Oct 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have several different conventions about naming of bundled versions of maps. Some day, we should decide what to do about it.

Copy link
Copy Markdown
Member Author

@eric-wieser eric-wieser Oct 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this case, I copied MultilinearMap.compLinearMapₗ

@urkud
Copy link
Copy Markdown
Member

urkud commented Oct 19, 2024

Thanks! 🎉
bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 19, 2024
@eric-wieser
feat: algebraic properties of LinearMap.compMultilinear (#17932)
6e38c66 
This also demotes `LinearMap.compAlternatingMap` to a plain function, for consistency.

To make up for this loss, it introduces `LinearMap.compAlternatingMapₗ` as the stronger linear version.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: algebraic properties of LinearMap.compMultilinear [Merged by Bors] - feat: algebraic properties of LinearMap.compMultilinear Oct 19, 2024
@mathlib-bors mathlib-bors bot closed this Oct 19, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/compMultilinear branch October 19, 2024 01:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@eric-wieser @urkud