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

Update BMinusL.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-08-31 18:08:55 +02:00
parent 81e6c6d68e
commit 56e4d6cf40
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
View file

@ -66,8 +66,7 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
ring
lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (BL n).val S.val = 0 := by
rw [on_quadBiLin]
rw [YYsol S, SU2Sol S, SU3Sol S]
rw [on_quadBiLin, YYsol S, SU2Sol S, SU3Sol S]
simp
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
@ -87,7 +86,7 @@ def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b)
lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by
simp [addQuad, linearToQuad]
simp only [addQuad, linearToQuad, zero_smul, add_zero]
rfl
lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
@ -100,8 +99,7 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
cubeTriLin (BL n).val (BL n).val S.val = 0 := by
rw [on_cubeTriLin]
rw [gravSol S, SU3Sol S]
rw [on_cubeTriLin, gravSol S, SU3Sol S]
simp
lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :