Skip to content

chore(Module.FinitePresentation): rename Module.FinitePresentation to Module.IsFinitelyPresented#41941

Draft
homeowmorphism wants to merge 1 commit into
leanprover-community:masterfrom
homeowmorphism:Module.IsFinitelyPresented
Draft

chore(Module.FinitePresentation): rename Module.FinitePresentation to Module.IsFinitelyPresented#41941
homeowmorphism wants to merge 1 commit into
leanprover-community:masterfrom
homeowmorphism:Module.IsFinitelyPresented

Conversation

@homeowmorphism

Copy link
Copy Markdown
Contributor

As Module.FinitePresentation is a Prop-valued class rather than a data carrying structure, this PR proposes to rename it Module.IsFinitelyPresented.


Claude Fable was used in doing this task.

Open in Gitpod

@homeowmorphism
homeowmorphism marked this pull request as draft July 20, 2026 00:26
@mathlib-bors

mathlib-bors Bot commented Jul 20, 2026

Copy link
Copy Markdown
Contributor

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant