From 7ac09d7d38547f19a9b2eb24d3f13adefa59e572 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Sun, 29 Mar 2026 00:09:42 +0100 Subject: [PATCH 1/5] first commit --- Mathlib/GroupTheory/FinitelyPresentedGroup.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean index 9d0f1e934cee4a..046c8756c955e8 100644 --- a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean +++ b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Hang Lu Su. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Riccardo Brasca, Fabrizio Barroero, Stefano Francaviglia, +Authors: Riccardo Brasca, Fabrizio Barroero, Thomas Browning, Kevin Buzzard, Stefano Francaviglia, Francesco Milizia, Valerio Proietti, Hang Lu Su, Lawrence Wu -/ module From 73f9e94bd51a883bff7b70451ff4bfd8a14f931b Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Sun, 29 Mar 2026 00:43:16 +0100 Subject: [PATCH 2/5] the order was not alphabetical before! --- Mathlib/GroupTheory/FinitelyPresentedGroup.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean index 046c8756c955e8..96e80d9c39d2dc 100644 --- a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean +++ b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Hang Lu Su. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Riccardo Brasca, Fabrizio Barroero, Thomas Browning, Kevin Buzzard, Stefano Francaviglia, +Authors: Fabrizio Barroero, Riccardo Brasca, Thomas Browning, Kevin Buzzard, Stefano Francaviglia, Francesco Milizia, Valerio Proietti, Hang Lu Su, Lawrence Wu -/ module From 15639fdb3d523916022acf22cfd5cfd7255a2787 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Sun, 29 Mar 2026 00:44:49 +0100 Subject: [PATCH 3/5] main authors first --- Mathlib/GroupTheory/FinitelyPresentedGroup.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean index 96e80d9c39d2dc..5ef0b08e4071b1 100644 --- a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean +++ b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean @@ -1,8 +1,8 @@ /- Copyright (c) 2025 Hang Lu Su. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Barroero, Riccardo Brasca, Thomas Browning, Kevin Buzzard, Stefano Francaviglia, - Francesco Milizia, Valerio Proietti, Hang Lu Su, Lawrence Wu +Authors: Riccardo Brasca, Thomas Browning, Kevin Buzzard, Hang Lu Su, Fabrizio Barroero, +Stefano Francaviglia, Francesco Milizia, Valerio Proietti, Lawrence Wu -/ module From 121269aafb87b0bb1920bb4e39d277f48a253554 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Sun, 29 Mar 2026 00:52:36 +0100 Subject: [PATCH 4/5] played with main / secondary author in formatting. Still not sure how to do this. --- Mathlib/GroupTheory/FinitelyPresentedGroup.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean index 5ef0b08e4071b1..bab13150585df4 100644 --- a/Mathlib/GroupTheory/FinitelyPresentedGroup.lean +++ b/Mathlib/GroupTheory/FinitelyPresentedGroup.lean @@ -1,8 +1,8 @@ /- Copyright (c) 2025 Hang Lu Su. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Riccardo Brasca, Thomas Browning, Kevin Buzzard, Hang Lu Su, Fabrizio Barroero, -Stefano Francaviglia, Francesco Milizia, Valerio Proietti, Lawrence Wu +Authors: Riccardo Brasca, Thomas Browning, Kevin Buzzard, Hang Lu Su, +Fabrizio Barroero, Stefano Francaviglia, Francesco Milizia, Valerio Proietti, Lawrence Wu -/ module From f136efab12542aad63db6ebc27cf8ac0fb5a7cd9 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Sun, 29 Mar 2026 01:23:51 +0100 Subject: [PATCH 5/5] Trigger CI now that local build works