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-20 00:19:24 +02:00
parent 90deb528a2
commit a25dcb4d9c
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/Odd/BasisLinear.lean
View file

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