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-08-31 18:08:43 +02:00
parent 86b3b8acd6
commit bf3a2df9b4
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -74,8 +74,7 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
· intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
· exact fun _ _=> rfl
rw [h1]
rw [Fin.sum_univ_add, Finset.sum_add_distrib]
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
@ -85,8 +84,7 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
· intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
· exact fun _ _ => rfl
rw [h1]
rw [Fin.sum_univ_add, Finset.sum_add_distrib]
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :