DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Change git-hub repo for llm

Browse source
This commit is contained in:
jstoobysmith 2024-07-15 15:10:10 -04:00
parent d6460e62bc
commit cc7a6b874b
3 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/MSSMNu/Basic.lean
View file

@ -60,7 +60,7 @@ def toSpeciesMaps' : (Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ) :=
((@finProdFinEquiv 6 3).arrowCongr (Equiv.refl ℚ))).symm
/-- An equivalence between `MSSMCharges.charges` and `(Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ))`.
This split charges up into the SM and additional fermions, and further splits the SM into
This splits charges up into the SM and additional fermions, and further splits the SM into
species. -/
@[simps!]
def toSpecies : MSSMCharges.Charges ≃ (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ) :=
@ -233,7 +233,7 @@ lemma accSU3_ext {S T : MSSMCharges.Charges}
repeat erw [hj]
rfl
/-- The acc for `Y²`. -/
/-- The ACC for `Y²`. -/
@[simp]
def accYY : MSSMCharges.Charges →ₗ[ℚ] ℚ where
toFun S := ∑ i, ((Q S) i + 8 * (U S) i + 2 * (D S) i + 3 * (L S) i