Skip to content

feat: add finitely presented instance for free groups#38109

Open
pacastega wants to merge 8 commits intoleanprover-community:masterfrom
pacastega:free_finitelypresented
Open

feat: add finitely presented instance for free groups#38109
pacastega wants to merge 8 commits intoleanprover-community:masterfrom
pacastega:free_finitelypresented

Conversation

@pacastega
Copy link
Copy Markdown

@pacastega pacastega commented Apr 16, 2026

Add IsFinitelyPresented instance for free groups


Open in Gitpod

This commit adds a IsFinitelyPresented instance for free groups over Fin n.
@homeowmorphism

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 16, 2026
@github-actions
Copy link
Copy Markdown

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 16, 2026

PR summary f8770bc8b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Subgroup.isNormalClosureFG_bot
+ instance {n : ℕ} : Group.IsFinitelyPresented (FreeGroup (Fin n)) := by

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-group-theory Group theory label Apr 16, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 16, 2026

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@pacastega pacastega changed the title Add finitely presented instance for free groups feat: add finitely presented instance for free groups Apr 16, 2026
@tb65536
Copy link
Copy Markdown
Contributor

tb65536 commented Apr 16, 2026

Can you add a commit message above the line in the PR description?

Comment thread Mathlib/GroupTheory/FinitelyPresentedGroup.lean Outdated
Comment thread Mathlib/GroupTheory/FinitelyPresentedGroup.lean Outdated
Comment thread Mathlib/GroupTheory/FinitelyPresentedGroup.lean Outdated
@tb65536 tb65536 added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 16, 2026
@tb65536 tb65536 self-assigned this Apr 16, 2026
Comment thread Mathlib/GroupTheory/FinitelyPresentedGroup.lean Outdated
Comment thread Mathlib/GroupTheory/FinitelyPresentedGroup.lean Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants