Skip to content

[Merged by Bors] - fix(RingTheory): correct misnamed theorem#39741

Closed
vlad902 wants to merge 2 commits into
leanprover-community:masterfrom
vlad902:naming1
Closed

[Merged by Bors] - fix(RingTheory): correct misnamed theorem#39741
vlad902 wants to merge 2 commits into
leanprover-community:masterfrom
vlad902:naming1

Conversation

@vlad902

@vlad902 vlad902 commented May 23, 2026

Copy link
Copy Markdown
Collaborator

Update isFinitelyPresented to finitePresentation to match the typeclass Module.FinitePresentation.


Open in Gitpod

@github-actions github-actions Bot added the t-ring-theory Ring theory label May 23, 2026
@github-actions

github-actions Bot commented May 23, 2026

Copy link
Copy Markdown

PR summary f88a660c87

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ exists_factorization_of_finitePresentation

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.


No changes to strong technical debt.
No changes to weak technical debt.

vlad902 added 2 commits May 23, 2026 10:55
Update `isFinitelyPresented` to `finitePresentation` to match the
typeclass `Module.FinitePresentation`.
@vlad902 vlad902 added the easy < 20s of review time. See the lifecycle page for guidelines. label May 23, 2026
@ADedecker

Copy link
Copy Markdown
Member

I claim that the name FinitePresentation should be reserved for "this is some concrete finite presentation of P", but in the mean time this change is obviously good. So thanks !

bors merge

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 23, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 23, 2026
Update `isFinitelyPresented` to `finitePresentation` to match the typeclass `Module.FinitePresentation`.
@mathlib-bors

mathlib-bors Bot commented May 23, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title fix(RingTheory): correct misnamed theorem [Merged by Bors] - fix(RingTheory): correct misnamed theorem May 23, 2026
@mathlib-bors mathlib-bors Bot closed this May 23, 2026
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 24, 2026
Update `isFinitelyPresented` to `finitePresentation` to match the typeclass `Module.FinitePresentation`.
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
Update `isFinitelyPresented` to `finitePresentation` to match the typeclass `Module.FinitePresentation`.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
Update `isFinitelyPresented` to `finitePresentation` to match the typeclass `Module.FinitePresentation`.
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-ring-theory Ring theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants