chore(GroupTheory/FinitelyPresentedGroup): add co-authors

[homeowmorphism]

In the light of the discussions on the Zulip thread and #36996, it seems sensible to add @kbuzzard and @tb65536 as co-authors in recognition for their work designing the finitely presented group implementation. Please let me know if you think this is appropriate.

---

[github-actions]

PR summary 9f0aee2e9b

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

[SnirBroshi]

Hey, can you please add the scope GroupTheory/FinitelyPresentedGroup to the title to make the commit log entry clearer?

[homeowmorphism]

I am not sure about the author order for making a new file. I first started with alphabetical, but apparently it is not the convention in mathlib, and main contributors should go first?

I then made a different order, first listing the people who had a hand in designing the package in alphabetical order and then the other ItaLean2025 participants. If someone feels like giving their input on this so I can better understand how attributions work in the future, I would appreciate it.

[themathqueen]

If someone feels like giving their input on this so I can better understand how attributions work in the future, I would appreciate it.

I don't think order matters. It usually goes like: person who created the file, then contributors add their names as they go. So even if a new contributor did most of the file, they'd probably add their name last in the list.

[kbuzzard]

I am very happy not to be listed as an author on this file. @homeowmorphism you are a new contributor to mathlib and it's completely normal for new contributors to get help from experts, especially when it comes to definitions.

As the file gets bigger, having me as an author on it becomes more and more ridiculous, where all I did was made hopefully helpful suggestions about the idiomatic way to make one of the definitions.