chore: Test stats workflow

.github/workflows/stats.yml

@@ -0,0 +1,32 @@
+on:
+  pull_request:
+
+name: Create and Commit File on Pull Request
+
+jobs:
+  create-and-commit:
+    runs-on: ubuntu-latest
+
+    steps:
+      # Step 1: Checkout the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v3
+
+      # Step 2: Create a file
+      - name: Create a New File
+        run: echo "This is a new file created by the GitHub Actions workflow." > newfile.txt
+
+      # Step 3: Configure Git
+      - name: Set up Git user
+        run: |
+          git config --global user.name "github-actions"
+          git config --global user.email "[email protected]"
+
+      # Step 4: Stage and commit the file
+      - name: Commit and Push Changes
+        run: |
+          git add newfile.txt
+          git commit -m "Automated commit: added newfile.txt"
+          git push origin HEAD:${{ github.head_ref }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

HepLean/AnomalyCancellation/MSSMNu/Permutations.lean

@@ -29,6 +29,7 @@ open BigOperators
 @[simp]
 def PermGroup := Fin 6 → Equiv.Perm (Fin 3)
 
+/-- The type `PermGroup` has a group instances derived from the group instance of it's target. -/
 @[simp]
 instance : Group PermGroup := Pi.group
 

HepLean/AnomalyCancellation/PureU1/BasisLinear.lean

@@ -120,6 +120,7 @@ noncomputable
 def asBasis : Basis (Fin n) ℚ ((PureU1 n.succ).LinSols) where
   repr := coordinateMap
 
+/-- The module over `ℚ` defined by linear solutions to the pure `U(1)` ACCs is finite. -/
 instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
   Module.Finite.of_basis asBasis
 

HepLean/AnomalyCancellation/PureU1/Permutations.lean

@@ -26,6 +26,7 @@ namespace PureU1
 @[simp]
 def PermGroup (n : ℕ) := Equiv.Perm (Fin n)
 
+/-- The type `PermGroup n` inherits the instance of a group from `Equiv.Perm`. -/
 instance {n : ℕ} : Group (PermGroup n) := Equiv.Perm.permGroup
 
 section Charges

HepLean/AnomalyCancellation/SM/Permutations.lean

@@ -30,6 +30,8 @@ def PermGroup (n : ℕ) := ∀ (_ : Fin 5), Equiv.Perm (Fin n)
 
 variable {n : ℕ}
 
+/-- The type `PermGroup n` inherits the instance of a group from it's
+  target space `Equiv.Perm`.  -/
 @[simp]
 instance : Group (PermGroup n) := Pi.group
 

HepLean/FlavorPhysics/CKMMatrix/Basic.lean

@@ -155,6 +155,7 @@ scoped[CKMMatrix] notation (name := ts_element) "[" V "]ts" => V.1 2 1
 /-- The `tb`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := tb_element) "[" V "]tb" => V.1 2 2
 
+/-- The setoid of CKM matrices defined by phase shifts of fermions. -/
 instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨PhaseShiftRelation, phaseShiftRelation_equiv⟩
 
 /-- The matrix obtained from `V` by shifting the phases of the fermions. -/

HepLean/Lorentz/ComplexTensor/Basic.lean

@@ -215,6 +215,7 @@ instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
 instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
     Fintype (OverColor.mk c).left := Fin.fintype n
 
+/-- The equality of two maps in `OverColor C` from objects based on `Fin _` is decidable. -/
 instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C} (σ σ' : OverColor.mk c ⟶ OverColor.mk c1) :
     Decidable (σ = σ') :=