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

Update Lemmas.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-20 00:19:31 +02:00
parent 7515fde402
commit e77dd4b098
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
View file

@ -12,7 +12,7 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
The main result of this file is the conclusion of this paper: The main result of this file is the conclusion of this paper:
https://arxiv.org/abs/1907.00514 https://arxiv.org/abs/1907.00514
That eveery solution to the ACCs without gravity satifies for free the gravitational anomaly. That eveery solution to the ACCs without gravity satisfies for free the gravitational anomaly.
-/ -/
universe v u universe v u
@ -67,7 +67,7 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0
rw [← hS'] rw [← hS']
exact S'.grav_of_cubic hC FLTThree exact S'.grav_of_cubic hC FLTThree
/-- Any solution to the ACCs without gravity satifies the gravitational ACC. -/ /-- Any solution to the ACCs without gravity satisfies the gravitational ACC. -/
theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) : theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) :
accGrav S.val = 0 := by accGrav S.val = 0 := by
by_cases hQ : Q S.val (0 : Fin 1)= 0 by_cases hQ : Q S.val (0 : Fin 1)= 0