Skip to content

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors#18596

Closed
joelriou wants to merge 12 commits intomasterfrom
linear-algebra-exterior-power-functor
Closed

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors#18596
joelriou wants to merge 12 commits intomasterfrom
linear-algebra-exterior-power-functor

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Nov 4, 2024 •
edited by alreadydone
Loading

We define the nth exterior power functor, from ModuleCat R to itself.

Co-authored-by: sophie.morel@ens-lyon.fr

This is partly extracted from #10654.

Open in Gitpod

@joelriou joelriou added the t-algebra Algebra (groups, rings, fields, etc) label Nov 4, 2024
@joelriou joelriou mentioned this pull request Nov 4, 2024
Closed
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 4, 2024 •
edited
Loading

PR summary e213b71bbc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Category.ModuleCat.ExteriorPower (new file) 1540

Declarations diff

+ AlternatingMap
+ alternatingMapLinearEquiv_symm_map
+ desc
+ desc_mk
+ ext
+ exteriorPower
+ functor
+ hom_ext
+ instance (M : ModuleCat.{v} R) (N : ModuleCat.{max u v} R) (n : ℕ) :
+ map_apply_ιMulti
+ map_comp
+ map_comp_ιMulti
+ map_id
+ map_mk
+ mk
+ postcomp
+ postcomp_apply
++ map

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 4, 2024
This was referenced Nov 4, 2024
Closed
Closed
@joelriou joelriou added the WIP Work in progress label Nov 7, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 15, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 4, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Dec 4, 2024

This PR/issue depends on:

joelriou
joelriou commented Jan 15, 2025
View reviewed changes
joelriou
joelriou commented Jan 15, 2025
View reviewed changes
@joelriou joelriou removed the WIP Work in progress label Jan 15, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 15, 2025
@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Jan 26, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 26, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 26, 2025
@joelriou
feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors (#…
0d39cc6 
…18596)

We define the `n`th exterior power functor, from `ModuleCat R` to itself.

Co-authored-by: sophie.morel@ens-lyon.fr



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 26, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors [Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors Jan 26, 2025
@mathlib-bors mathlib-bors bot closed this Jan 26, 2025
@mathlib-bors mathlib-bors bot deleted the linear-algebra-exterior-power-functor branch January 26, 2025 15:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

4 participants

@joelriou @mathlib4-dependent-issues-bot @ocfnash @leanprover-community-bot-assistant