From 4528d22dc67a7c8d155fdb9e2983adb8a260cf25 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 21 May 2024 14:12:53 +0200 Subject: [PATCH] Update LinearParameterization.lean --- .../SM/NoGrav/One/LinearParameterization.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean index d34340a..01ae991 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean @@ -46,7 +46,7 @@ lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E cases' S simp_all only -/-- The map from the linear paramaters to elements of `(SMNoGrav 1).charges`. -/ +/-- The map from the linear parameters to elements of `(SMNoGrav 1).charges`. -/ @[simp] def asCharges (S : linearParameters) : (SMNoGrav 1).charges := fun i => match i with