Skip to content

chore: add ContinuousLinearEquiv.prodAssoc#25522

Closed
grunweg wants to merge 1 commit intomasterfrom
MR-cle-prodAssoc
Closed

chore: add ContinuousLinearEquiv.prodAssoc#25522
grunweg wants to merge 1 commit intomasterfrom
MR-cle-prodAssoc

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jun 6, 2025

A continuous version of LinearEquiv.prodAssoc. Part of #25505 (on the path towards defining submanifolds).


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 6, 2025

PR summary 93e9e95c5a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coe_prodAssoc
+ prodAssoc
+ prodAssoc_toEquiv
+ prodAssoc_toLinearEquiv

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 Jun 6, 2025
@grunweg grunweg force-pushed the MR-cle-prodAssoc branch from 5cfc966 to 3ef3447 Compare June 11, 2025 15:50
@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 Jun 11, 2025
@grunweg grunweg requested a review from ocfnash June 14, 2025 18:09
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jun 18, 2025

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

@grunweg grunweg closed this Jun 18, 2025
@grunweg grunweg deleted the MR-cle-prodAssoc branch June 18, 2025 17:59
mathlib-bors bot pushed a commit that referenced this pull request Jun 24, 2025
This PR continues the work from #25522.

Original PR: #25522
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants