[Merged by Bors] - feat: add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime by riccardobrasca · Pull Request #39982 · leanprover-community/mathlib4

riccardobrasca · 2026-05-28T17:06:22Z

github-actions · 2026-05-28T17:13:51Z

PR summary c0a8576cf7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime
+ Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c0a8576).

+2 new declarations
−0 removed declarations

+FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime
+Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime

No changes to strong technical debt.

No changes to weak technical debt.

Current commit c0a8576cf7
Reference commit 8f560a2211

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

…lassgroup

mathlib-merge-conflicts · 2026-06-05T02:28:06Z

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

# Conflicts: # Mathlib/RingTheory/ClassGroup.lean

mariainesdff · 2026-06-25T08:19:28Z

I have the impression that it will be worth it to create a ClassGroup namespace in this file (but not in this PR).

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

…lassgroup

riccardobrasca · 2026-06-30T10:38:18Z

@mariainesdff can you have another look? Thanks!

mariainesdff · 2026-07-20T11:42:22Z

Thanks!
maintainer delegate

github-actions · 2026-07-20T11:42:51Z

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

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Vierkantor

Thanks! 🎉

bors d+

mathlib-bors · 2026-07-22T17:24:07Z

✌️ riccardobrasca can now approve this pull request until 2026-08-05 17:24 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

riccardobrasca · 2026-07-23T05:40:38Z

bors merge

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-07-23T05:50:20Z

Pull request successfully merged into master.

Build succeeded:

github-actions Bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-ring-theory Ring theory labels May 28, 2026

add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime

17f3e5d

riccardobrasca force-pushed the principal-power-classgroup branch from 4a10a83 to 17f3e5d Compare May 28, 2026 17:12

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 28, 2026

riccardobrasca added 3 commits May 28, 2026 18:46

Merge remote-tracking branch 'upstream/master' into principal-power-c…

6911eea

…lassgroup

let's keep this

7a9347f

ops

44021cf

mathlib-triage Bot assigned mariainesdff Jun 2, 2026

mathlib-merge-conflicts 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 Jun 5, 2026

Merge branch 'master' into principal-power-classgroup

fa43e8a

# Conflicts: # Mathlib/RingTheory/ClassGroup.lean

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 Jun 5, 2026

riccardobrasca temporarily deployed to cache-upload-forks June 5, 2026 10:55 — with GitHub Actions Inactive

mariainesdff reviewed Jun 25, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/ClassGroup/Basic.lean Outdated

mariainesdff reviewed Jun 25, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/ClassGroup/Basic.lean Outdated

mariainesdff reviewed Jun 25, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/ClassGroup/Basic.lean Outdated

mariainesdff added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 25, 2026

riccardobrasca and others added 6 commits June 25, 2026 11:39

Update Mathlib/RingTheory/ClassGroup/Basic.lean

f874c1a

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Update Mathlib/RingTheory/ClassGroup/Basic.lean

1ce48bf

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Update Mathlib/RingTheory/ClassGroup/Basic.lean

5254ad6

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

[pre-commit.ci lite] apply automatic fixes

e401f74

Merge remote-tracking branch 'upstream/master' into principal-power-c…

ec4f65e

…lassgroup

fix

20ee7d8

riccardobrasca removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 30, 2026

Merge branch 'master' into principal-power-classgroup

293b84a

mariainesdff reviewed Jul 20, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/ClassGroup/Basic.lean Outdated

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 20, 2026

riccardobrasca and others added 3 commits July 21, 2026 10:03

Update Mathlib/RingTheory/ClassGroup/Basic.lean

8cc378d

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

fix

9e26a0d

Merge branch 'master' into principal-power-classgroup

a4b16c5

Vierkantor approved these changes Jul 22, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/ClassGroup/Basic.lean Outdated

Comment thread Mathlib/RingTheory/ClassGroup/Basic.lean Outdated

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 22, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 22, 2026

riccardobrasca and others added 3 commits July 23, 2026 13:18

Update Mathlib/RingTheory/ClassGroup/Basic.lean

b2a4aaa

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Update Mathlib/RingTheory/ClassGroup/Basic.lean

ddc770b

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Merge branch 'master' into principal-power-classgroup

c0a8576

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jul 23, 2026

mathlib-bors Bot pushed a commit that referenced this pull request Jul 23, 2026

feat: add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime (#39982)

8e45b05

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jul 23, 2026

mathlib-bors Bot changed the title ~~feat: add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime~~ [Merged by Bors] - feat: add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime Jul 23, 2026

mathlib-bors Bot closed this Jul 23, 2026

mathlib-bors Bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 23, 2026

Uh oh!

Conversation

riccardobrasca commented May 28, 2026

Uh oh!

github-actions Bot commented May 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c0a8576cf7

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented Jun 5, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mariainesdff commented Jun 25, 2026

Uh oh!

riccardobrasca commented Jun 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

mariainesdff commented Jul 20, 2026

Uh oh!

github-actions Bot commented Jul 20, 2026

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Jul 22, 2026

Uh oh!

riccardobrasca commented Jul 23, 2026

Uh oh!

mathlib-bors Bot commented Jul 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented May 28, 2026 •

edited

Loading

riccardobrasca commented Jun 30, 2026 •

edited

Loading