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

feat: lint-all script for easy linting

Browse source
This commit is contained in:
jstoobysmith 2024-04-16 16:41:28 -04:00
parent 7ff351a4a5
commit 4e9d26a1a9
2 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/LinearMaps.lean
View file

@ -83,8 +83,6 @@ structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] where
map_add₁' : ∀ S1 S2 T, toFun (S1 + S2, T) = toFun (S1, T) + toFun (S2, T)
swap' : ∀ S T, toFun (S, T) = toFun (T, S)
namespace BiLinearSymm
variable {V : Type} [AddCommMonoid V] [Module ℚ V]