Skip to content

feat(LinearAlgebra): generators of pi tensor products #26464

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 76 commits into
base: master
Choose a base branch
from
Open

feat(LinearAlgebra): generators of pi tensor products #26464

wants to merge 76 commits into from
+269 −4

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Jun 27, 2025 •
edited
Loading

In this PR, we show that the R-module ⨂[R] i, M i is finitely generated if the index type is finite and all M i are finitely generated. This follows from a more precise result about generators of ⨂[R] i, M i.

This PR continues the work from #18725.

Original PR: #18725

joelriou and others added 30 commits November 1, 2024 18:54
@joelriou
draft
ba55f88
@joelriou
wip
89ebec1
@joelriou
fixing the build
8bcbaf1
@joelriou
fixing the build
4d6e656
@joelriou
Merge remote-tracking branch 'origin' into generalize-tmulequiv
9a520dd
@joelriou
moved the code
96f5019
@joelriou
better syntax
f34e253
@joelriou
fixing the build
75d7c5c
@joelriou
fixing the build
c974768
@joelriou
fixing the build
2aa202c
@joelriou @github-actions
Update Mathlib/Data/Sum/Basic.lean
ae054f4 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
Merge remote-tracking branch 'origin' into generalize-tmulequiv
4b0b2a5
@joelriou
fixing the build
bf4bd7a
@joelriou
Merge remote-tracking branch 'origin' into generalize-tmulequiv
f690ffe
@joelriou
proof by rfl
4c05afe
@joelriou
generators of pi tensor products
2f599f9
@joelriou
Merge remote-tracking branch 'origin' into generalize-tmulequiv
69e3b17
@joelriou
removed deprecated alias for uncurrySum
626ebea
@joelriou
deprecated def
2410565
@joelriou
used update_comp_eq_of_injective'
f3dd5b9
@joelriou @github-actions
Update Mathlib/LinearAlgebra/Multilinear/Basic.lean
26a9f0c 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
fixed deprecated defs
e04b7cb
@joelriou
Merge remote-tracking branch 'origin' into generalize-tmulequiv
94315f2
@joelriou
fix
b42804b
@joelriou
fix
a1f7cad
@joelriou
fix
451de95
@joelriou
fix
8d60684
@eric-wieser
Merge branch 'master' into generalize-tmulequiv
af765d1
@eric-wieser
remove duplicates, golf
e2f574c
@joelriou
Merge remote-tracking branch 'origin' into generalize-tmulequiv
70c695e
@leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 29, 2025
@leanprover-community-bot-assistant
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 31, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 5, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 5, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 8, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 10, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 11, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 15, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 22, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 22, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 22, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
file-removed A Lean module was (re)moved without a `deprecated_module` annotation merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) 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 @leanprover-community-bot-assistant @mathlib4-merge-conflict-bot @eric-wieser