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

Update BasisLinear.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-21 14:07:53 +02:00
parent 665289854a
commit ae2b974669
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -10,7 +10,7 @@ import Mathlib.Logic.Equiv.Fin
/-! /-!
# Basis of `LinSols` in the even case # Basis of `LinSols` in the even case
We give a basis of `LinSols` in the even case. This basis has the special propoerty We give a basis of `LinSols` in the even case. This basis has the special property
that splits into two planes on which every point is a solution to the ACCs. that splits into two planes on which every point is a solution to the ACCs.
-/ -/
universe v u universe v u