Skip to content

chore: semilinearize LinearAlgebra.TensorProduct.Basic#24208

Closed
ADedecker wants to merge 6 commits intomasterfrom
AD_semilinearize_tensor_part1
Closed

chore: semilinearize LinearAlgebra.TensorProduct.Basic#24208
ADedecker wants to merge 6 commits intomasterfrom
AD_semilinearize_tensor_part1

Conversation

@ADedecker
Copy link
Copy Markdown
Member

@ADedecker ADedecker commented Apr 19, 2025

This was painful, and it's not without consequences, but this is necessary in order to talk about tensor products of Hilbert spaces.

Open in Gitpod

@ADedecker ADedecker added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Apr 19, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 19, 2025 •
edited
Loading

PR summary 8a30dbe596

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ liftAux.smulₛₗ
+ llcompₛₗ
+ llcompₛₗ_apply
+ llcompₛₗ_apply'

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).

@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 May 15, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented May 15, 2025

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

@themathqueen themathqueen mentioned this pull request Jul 17, 2025
Closed
1 task
@ADedecker ADedecker mentioned this pull request Jul 18, 2025
Closed
2 tasks
eric-wieser
eric-wieser reviewed Jul 18, 2025
View reviewed changes
Mathlib/LinearAlgebra/BilinearMap.lean
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Jul 18, 2025

Choose a reason for hiding this comment

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

Could you try to extract this to a standalone PR? These types of results tend to be needed in lots of places!

@themathqueen themathqueen mentioned this pull request Jul 19, 2025
Closed
@ADedecker
Copy link
Copy Markdown
Member Author

ADedecker commented Jul 20, 2025

This PR has been migrated to a fork-based workflow: #27310

@ADedecker ADedecker mentioned this pull request Jul 20, 2025
Closed
@ADedecker ADedecker closed this Jul 20, 2025
This was referenced Jul 22, 2025
Closed
Closed
mathlib-bors bot pushed a commit that referenced this pull request Aug 13, 2025
@themathqueen
chore(LinearAlgebra/BilinearMap): semi-linearize (#27467)
bbd1ca8 
Semi-linearizes `llcomp` and creates a new definition `compr₂ₛₗ` for the semi-linear version of `compr₂`.

Original PRs: #27353 (#27310, #24208).

Co-authored-by: @ADedecker



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>
@YaelDillies YaelDillies deleted the AD_semilinearize_tensor_part1 branch August 17, 2025 11:45
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@themathqueen @Paul-Lez
chore(LinearAlgebra/BilinearMap): semi-linearize (leanprover-communit…
34101f3 
…y#27467)

Semi-linearizes `llcomp` and creates a new definition `compr₂ₛₗ` for the semi-linear version of `compr₂`.

Original PRs: leanprover-community#27353 (leanprover-community#27310, leanprover-community#24208).

Co-authored-by: @ADedecker



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@themathqueen @pechersky
chore(LinearAlgebra/BilinearMap): semi-linearize (leanprover-communit…
ece35f0 
…y#27467)

Semi-linearizes `llcomp` and creates a new definition `compr₂ₛₗ` for the semi-linear version of `compr₂`.

Original PRs: leanprover-community#27353 (leanprover-community#27310, leanprover-community#24208).

Co-authored-by: @ADedecker



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>
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

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) migrated-to-fork t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ADedecker @leanprover-community-bot-assistant @eric-wieser