Skip to content
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

[Merged by Bors] - chore(AdicCompletion): generalise algebra instance to separate rings #19466

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(AdicCompletion): generalise algebra instance to separate rings #19466

wants to merge 2 commits into from
+76 −58

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Nov 25, 2024 •
edited
Loading

In the existing instance Algebra R (AdicCompletion I R), R appears three times: On the left, on the right, and in I : Ideal R. The left occurrence can be generalised to a ring S such that R is a S-algebra.

Closes ImperialCollegeLondon/FLT/issues/230.

From FLT

Open in Gitpod

@YaelDillies YaelDillies added t-algebra Algebra (groups, rings, fields, etc) FLT part of the ongoing formalization of Fermat's Last Theorem labels Nov 25, 2024
@github-actions GitHub Actions
Copy link

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

PR summary bf5de9cbbb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instIsCentralScalar
+ instIsScalarTower
+ instSMul
+ instSMulCommClass
+ instance [Algebra S R] : Algebra S (AdicCompletion I R)
+ instance [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
+ val_add_apply
+ val_neg
+ val_neg_apply
+ val_smul_apply
+ val_sub_apply
+ val_sum_apply
+ val_zero_apply
- instance : Algebra R (AdicCompletion I R)
- instance : Module R (AdicCompletion I M)
- instance : SMul R (AdicCompletion I M)
- instance : SMul ℕ (AdicCompletion I M)
- instance : SMul ℤ (AdicCompletion I M)

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

@YaelDillies YaelDillies force-pushed the adic_completion_general_smul branch from dc6152b to 323e4c3 Compare November 25, 2024 18:14
@kbuzzard kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 4, 2024
@YaelDillies YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 7, 2024
eric-wieser
eric-wieser reviewed Dec 8, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors d+

Thanks!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 8, 2024

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@YaelDillies
chore(AdicCompletion): generalise algebra instance to separate rings
5ccaa3c 
In the existing instance `Algebra R (AdicCompletion I R)`, `R` appears three times: On the left, on the right, and in `I : Ideal R`. The left occurrence can be generalised to a ring `S` such that `R` is a `S`-algebra.

From FLT
@YaelDillies
IsCentralScalar instance
bf5de9c
@YaelDillies YaelDillies force-pushed the adic_completion_general_smul branch from 285449d to bf5de9c Compare December 8, 2024 07:40
@YaelDillies
Copy link
Collaborator Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Dec 8, 2024
@YaelDillies
chore(AdicCompletion): generalise algebra instance to separate rings (#…
31530f3 
…19466)

In the existing instance `Algebra R (AdicCompletion I R)`, `R` appears three times: On the left, on the right, and in `I : Ideal R`. The left occurrence can be generalised to a ring `S` such that `R` is a `S`-algebra.

Closes ImperialCollegeLondon/FLT/issues/230.

From FLT
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(AdicCompletion): generalise algebra instance to separate rings [Merged by Bors] - chore(AdicCompletion): generalise algebra instance to separate rings Dec 8, 2024
@mathlib-bors mathlib-bors bot closed this Dec 8, 2024
@mathlib-bors mathlib-bors bot deleted the adic_completion_general_smul branch December 8, 2024 07:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

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

Assignees
No one assigned
Labels
delegated FLT part of the ongoing formalization of Fermat's Last Theorem t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Avoiding Algebra K (adicCompletion L w) diamond
4 participants
@YaelDillies @eric-wieser @kbuzzard @leanprover-community-mathlib4-bot