Skip to content

[Merged by Bors] - fix(FieldTheory/Perfect): move one/mul/pow into namespace#37957

Closed
wwylele wants to merge 1 commit intoleanprover-community:masterfrom
wwylele:perfect-ring-namespace
Closed

[Merged by Bors] - fix(FieldTheory/Perfect): move one/mul/pow into namespace#37957
wwylele wants to merge 1 commit intoleanprover-community:masterfrom
wwylele:perfect-ring-namespace

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented Apr 12, 2026

Fixes #37936. The names one/mul/pow should obviously not in the global namespace. I also checked the rest of the file, and they look fine IMO. (e.g. powMulEquiv is only an equivalence for perfect ring so there is no ambiguity)

I did not add deprecation note because I think it makes sense for these names to go away as quick as possible and nobody should be using them.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

PR summary c290b55c6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Apr 12, 2026
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Apr 12, 2026

easy

@github-actions github-actions bot added the easy < 20s of review time. See the lifecycle page for guidelines. label Apr 12, 2026
@themathqueen
Copy link
Copy Markdown
Collaborator

I did not add deprecation note ...

Instance names don't need deprecations, so you're good. And these definitely should not be global names: one, mul, pow.

maintainer merge

@github-actions
Copy link
Copy Markdown

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 12, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 13, 2026
Fixes #37936. The names `one`/`mul`/`pow` should obviously not in the global namespace. I also checked the rest of the file, and they look fine IMO. (e.g. `powMulEquiv` is only an equivalence for perfect ring so there is no ambiguity)

I did not add deprecation note because I think it makes sense for these names to go away as quick as possible and nobody should be using them.
@mathlib-triage mathlib-triage bot 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 Apr 13, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 13, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(FieldTheory/Perfect): move one/mul/pow into namespace [Merged by Bors] - fix(FieldTheory/Perfect): move one/mul/pow into namespace Apr 13, 2026
@mathlib-bors mathlib-bors bot closed this Apr 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Irrelevant Links in Data.Nat.Init

3 participants