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

refactor

Browse source
This commit is contained in:
jstoobysmith 2024-04-16 16:04:53 -04:00
parent ecf2c8f6b8
commit c7ad21ceb6
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/Basic.lean
View file

@ -191,7 +191,7 @@ instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols wher
intro i
erw [(χ.quadraticACCs i).map_smul]
rw [S.quadSol i]
simp
simp only [mul_zero]
⟩
mul_smul a b S := by
apply QuadSols.ext
@ -277,7 +277,7 @@ def Hom.comp {χ η ε : ACCSystem} (g : Hom η ε) (f : Hom χ η) : Hom χ ε
charges := LinearMap.comp g.charges f.charges
anomalyFree := g.anomalyFree ∘ f.anomalyFree
commute := by
simp
simp only [LinearMap.coe_comp]
rw [Function.comp.assoc]
rw [f.commute, ← Function.comp.assoc, g.commute, Function.comp.assoc]