Skip to content

feat(LinearAlgebra/FreeProduct): fill out the FreeProduct.asPowers namespace#24532

Open
robertmaxton42 wants to merge 8 commits intomasterfrom
robertmaxton42_algebracat2_patch0
Open

feat(LinearAlgebra/FreeProduct): fill out the FreeProduct.asPowers namespace#24532
robertmaxton42 wants to merge 8 commits intomasterfrom
robertmaxton42_algebracat2_patch0

Conversation

@robertmaxton42
Copy link
Copy Markdown
Collaborator

@robertmaxton42 robertmaxton42 commented May 1, 2025 •
edited by YaelDillies
Loading

  • Replicate the existing API for LinearAlgebra.FreeProduct under FreeProduct.asPowers, for convenience when working primarily with the power algebra representation
  • Adds convenience lemmas for using the corresponding quotient relation rel' (used in the above).

Open in Gitpod

@robertmaxton42
refactor (LinearAlgebra/FreeProduct): rename LinearAlgebra.FreeProduc…
a51dfc9 
…tOfPowers to LinearAlgeba.FreeProduct.asPowers, add simp shortcut to lift lemmas
@robertmaxton42
feat (LinearAlgebra/FreeProduct): fill out the FreeProduct.asPowers…
ec7dbe5 
… namespace
@github-actions
Copy link
Copy Markdown

github-actions bot commented May 1, 2025 •
edited
Loading

PR summary 2ff108d501

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ PowerAlgebra.ι
+ asPowersEquiv_symm_ι
+ asPowersEquiv_ι
+ lof
+ lof_map_one
+ mkAlgHom
+ of
+ rel'_cases
+ rel'_id
+ rel'_prod
+ rel_prod
+ ι'
+ ι'_mul_ι'
+ ι'_one
+ ι_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).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label May 1, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels May 2, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented May 7, 2025

This PR/issue depends on:

@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

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

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

@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 7, 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 May 7, 2025
@robertmaxton42 robertmaxton42 mentioned this pull request May 7, 2025
Open
1 task
YaelDillies
YaelDillies reviewed May 8, 2025
View reviewed changes
Mathlib/LinearAlgebra/FreeProduct/Basic.lean
Comment on lines +153 to +155
-- We reproduce `rel.id` and `.prod here to make `R, A, i...` explicit.
@[inherit_doc rel.id]
theorem rel_id (i : I) : rel R A (ι R <| lof R I A i 1) 1 := rel.id
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies May 8, 2025

Choose a reason for hiding this comment

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

Can't you do this above by replacing | id : ∀ {i : I}, ... with | id (R A i) : ...?

Copy link
Copy Markdown
Collaborator Author

@robertmaxton42 robertmaxton42 May 8, 2025

Choose a reason for hiding this comment

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

Alas, no! It was the first thing I tried when I found out about the new depriming mechanism, but sadly it only works on classes, not inductive arms. See Kyle's answer here.

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies May 8, 2025

Choose a reason for hiding this comment

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

Sad!

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label May 8, 2025
@adomani adomani mentioned this pull request May 8, 2025
Closed
robertmaxton42
robertmaxton42 commented May 9, 2025
View reviewed changes
robertmaxton42
robertmaxton42 commented May 9, 2025
View reviewed changes
@robertmaxton42 @YaelDillies
Apply suggestions from code review
b5c4daf 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies reviewed May 9, 2025
View reviewed changes
robertmaxton42
robertmaxton42 commented May 11, 2025
View reviewed changes
@robertmaxton42 @YaelDillies
Apply suggestions from code review
078818e 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented May 11, 2025

Don't forget to remove awaiting-author when you are done addressing the comments!

@robertmaxton42 robertmaxton42 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025
YaelDillies
YaelDillies reviewed May 11, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

@eric-wieser, do you have mathematical thoughts here?

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025
@robertmaxton42 @YaelDillies
Apply suggestions from code review
2ff108d 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@robertmaxton42 robertmaxton42 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2025
mathlib-bors bot pushed a commit that referenced this pull request May 19, 2025
@adomani
fix(docstring linter): inspect also internal docstrings (#24673)
e262afd 
This omission was pointed out in #24532.
bwehlin pushed a commit to bwehlin/mathlib4 that referenced this pull request May 31, 2025
@adomani
fix(docstring linter): inspect also internal docstrings (leanprover-c…
54224c8 
…ommunity#24673)

This omission was pointed out in leanprover-community#24532.
@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 Oct 23, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Oct 23, 2025

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@adomani adomani adomani left review comments

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

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) t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@robertmaxton42 @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @YaelDillies @mathlib4-merge-conflict-bot @adomani