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

test: Doc Lint error

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

3
HepLean/AnomalyCancellation/GroupActions.lean
View file

@ -51,9 +51,8 @@ def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) :
exact (G.rep g).map_add' _ _
map_smul' a S := by
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