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

Feat: Upgrade versions

Browse source
This commit is contained in:
jstoobysmith 2024-05-06 14:55:22 -04:00
parent ce66368876
commit 44adfbb0c7
7 changed files with 16 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -88,7 +88,7 @@ lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
induction k
simp
rfl
rename_i k l hl
rename_i _ l hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]