[Merged by Bors] - feat: `8 ∣ a ^ 2 - 1` for each odd `a` by yuanyi-350 · Pull Request #28790 · leanprover-community/mathlib4

yuanyi-350 · 2025-08-23T04:55:29Z

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

yuanyi-350 · 2025-08-23T04:55:40Z

easy

github-actions · 2025-08-23T04:56:32Z

PR summary 3d73639872

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Int.eight_dvd_sq_sub_one_of_odd
+ Nat.eight_dvd_sq_sub_one_of_odd
++ two_dvd_mul_add_one

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

euprunin · 2025-08-23T05:21:53Z

It looks like the PR is missing two_dvd_mul_add_one?

yuanyi-350 · 2025-08-23T06:10:49Z

Thank you for your reminder. I think this issue is now resolved.

It looks like the PR is missing two_dvd_mul_add_one?

Mathlib/Algebra/Ring/Int/Parity.lean

Mathlib/Algebra/Ring/Parity.lean

Mathlib/NumberTheory/Multiplicity.lean

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

…one_of_odd-

MichaelStollBayreuth · 2025-09-01T13:02:58Z

Please read the explanation of the "easy" label. I don't think it applies here.
Read this and edit the PR title accordingly.
Add a PR description.

yuanyi-350 · 2025-09-01T13:03:43Z

-easy

MichaelStollBayreuth · 2025-09-01T13:14:02Z

You could mention in the PR description that this is for natural numbers and integers a specifically.

Mathlib/NumberTheory/Multiplicity.lean

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Mathlib/Algebra/Ring/Int/Parity.lean

Mathlib/Algebra/Ring/Parity.lean

MichaelStollBayreuth · 2025-09-01T17:48:37Z

I think this is OK now (regarding the naming of the two_dvd_... results, see this Zulip thread).

maintainer merge

github-actions · 2025-09-01T17:48:48Z

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

github-actions · 2025-09-01T17:49:38Z

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

kbuzzard · 2025-09-01T17:53:23Z

bors merge

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

mathlib-bors · 2025-09-01T20:14:53Z

Pull request successfully merged into master.

Build succeeded:

CI Success

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

- [x] depends on: #28788 - [x] depends on: #28790 - [x] depends on: #28829

- [x] depends on: leanprover-community#28788 - [x] depends on: leanprover-community#28790 - [x] depends on: leanprover-community#28829

Update Multiplicity.lean

cd8fb79

github-actions bot added the easy < 20s of review time. See the lifecycle page for guidelines. label Aug 23, 2025

yuanyi-350 requested a review from joneugster August 23, 2025 04:55

yuanyi-350 changed the title ~~eight_dvd_sq_sub_one_of_odd~~ eight_dvd_sq_sub_one_of_odd Aug 23, 2025

github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Aug 23, 2025

yuanyi-350 mentioned this pull request Aug 23, 2025

[Merged by Bors] - feat: 2025 imo problem3 #27254

Closed

3 tasks

Update Parity.lean

41a84bf

Update Parity.lean

848dc80

themathqueen reviewed Aug 24, 2025

View reviewed changes

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 24, 2025

yuanyi-350 and others added 6 commits August 25, 2025 06:44

Update Mathlib/Algebra/Ring/Int/Parity.lean

7d6c283

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Update Mathlib/Algebra/Ring/Int/Parity.lean

fd2dd92

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Update Mathlib/Algebra/Ring/Parity.lean

3197587

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Update Mathlib/Algebra/Ring/Parity.lean

b34ae3e

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Update Mathlib/NumberTheory/Multiplicity.lean

1d90c9f

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Update Mathlib/NumberTheory/Multiplicity.lean

007ff5f

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

yuanyi-350 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 24, 2025

Merge remote-tracking branch 'upstream/master' into eight_dvd_sq_sub_…

c46b7c4

…one_of_odd-

yuanyi-350 requested review from alreadydone and themathqueen August 27, 2025 05:27

leanprover-community-bot-assistant assigned MichaelStollBayreuth Sep 1, 2025

github-actions bot removed the easy < 20s of review time. See the lifecycle page for guidelines. label Sep 1, 2025

yuanyi-350 changed the title ~~eight_dvd_sq_sub_one_of_odd~~ feat: 8 ∣ a ^ 2 - 1 for each odd aeight_dvd_sq_sub_one_of_odd Sep 1, 2025

yuanyi-350 changed the title ~~feat: 8 ∣ a ^ 2 - 1 for each odd aeight_dvd_sq_sub_one_of_odd~~ feat: 8 ∣ a ^ 2 - 1 for each odd a Sep 1, 2025

MichaelStollBayreuth reviewed Sep 1, 2025

View reviewed changes

Mathlib/NumberTheory/Multiplicity.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Sep 1, 2025

View reviewed changes

Mathlib/NumberTheory/Multiplicity.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 1, 2025

yuanyi-350 and others added 2 commits September 1, 2025 21:20

Update Mathlib/NumberTheory/Multiplicity.lean

0bae080

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Update Mathlib/NumberTheory/Multiplicity.lean

aaac9c8

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

yuanyi-350 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 1, 2025

MichaelStollBayreuth reviewed Sep 1, 2025

View reviewed changes

Mathlib/Algebra/Ring/Int/Parity.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Sep 1, 2025

View reviewed changes

Mathlib/Algebra/Ring/Parity.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 1, 2025

remove useless thm

b37e1e2

MichaelStollBayreuth removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 1, 2025

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 1, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Sep 1, 2025

mathlib-bors bot pushed a commit that referenced this pull request Sep 1, 2025

feat: 8 ∣ a ^ 2 - 1 for each odd a (#28790)

caa187a

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

mathlib-bors bot changed the title ~~feat: 8 ∣ a ^ 2 - 1 for each odd a~~ [Merged by Bors] - feat: 8 ∣ a ^ 2 - 1 for each odd a Sep 1, 2025

mathlib-bors bot closed this Sep 1, 2025

yuanyi-350 deleted the eight_dvd_sq_sub_one_of_odd- branch September 2, 2025 00:01

CBirkbeck pushed a commit to CBirkbeck/mathlib4 that referenced this pull request Sep 8, 2025

feat: 8 ∣ a ^ 2 - 1 for each odd a (leanprover-community#28790)

3826118

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

yuanyi-350 added a commit to yuanyi-350/yuanyi_mathlib4 that referenced this pull request Sep 10, 2025

feat: 8 ∣ a ^ 2 - 1 for each odd a (leanprover-community#28790)

d0443f8

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025

feat: 8 ∣ a ^ 2 - 1 for each odd a (leanprover-community#28790)

41aa017

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

mathlib-bors bot pushed a commit that referenced this pull request Dec 20, 2025

feat: 2025 imo problem3 (#27254)

e9a7156

- [x] depends on: #28788 - [x] depends on: #28790 - [x] depends on: #28829

kim-em pushed a commit to kim-em/mathlib4 that referenced this pull request Jan 6, 2026

feat: 2025 imo problem3 (leanprover-community#27254)

67f0c7d

- [x] depends on: leanprover-community#28788 - [x] depends on: leanprover-community#28790 - [x] depends on: leanprover-community#28829

Conversation

yuanyi-350 commented Aug 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

In this PR, we proved 8 ∣ a ^ 2 - 1 for each odd natural numbers and integers a

Uh oh!

yuanyi-350 commented Aug 23, 2025

Uh oh!

github-actions bot commented Aug 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3d73639872

Import changes for modified files

Declarations diff

Uh oh!

euprunin commented Aug 23, 2025

Uh oh!

yuanyi-350 commented Aug 23, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth commented Sep 1, 2025

Uh oh!

yuanyi-350 commented Sep 1, 2025

Uh oh!

MichaelStollBayreuth commented Sep 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth commented Sep 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 1, 2025

Uh oh!

github-actions bot commented Sep 1, 2025

Uh oh!

kbuzzard commented Sep 1, 2025

Uh oh!

mathlib-bors bot commented Sep 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

yuanyi-350 commented Aug 23, 2025 •

edited

Loading

In this PR, we proved `8 ∣ a ^ 2 - 1` for each odd natural numbers and integers `a`

github-actions bot commented Aug 23, 2025 •

edited

Loading

MichaelStollBayreuth commented Sep 1, 2025 •

edited

Loading

MichaelStollBayreuth commented Sep 1, 2025 •

edited

Loading