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

doc: re-add doc

Browse source
This commit is contained in:
jstoobysmith 2024-05-14 11:23:13 -04:00
parent 7ad7f75c6f
commit f42540ffb4
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/AnomalyCancellation/GroupActions.lean
View file

@ -53,6 +53,7 @@ def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) :
apply ACCSystemLinear.LinSols.ext
exact (G.rep g).map_smul' _ _
/-- The representation acting on the vector space of solutions to the linear ACCs. -/
@[simps!]
def linSolRep {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
Representation ℚ G.group χ.LinSols where