diff --git a/PhysLean/QFT/AnomalyCancellation/Basic.lean b/PhysLean/QFT/AnomalyCancellation/Basic.lean
index 7cdec4cf..6461a302 100644
--- a/PhysLean/QFT/AnomalyCancellation/Basic.lean
+++ b/PhysLean/QFT/AnomalyCancellation/Basic.lean
@@ -503,7 +503,11 @@ def solsInclLinSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.LinSols :=
 @[sorryful]
 lemma solsInclLinSols_injective (χ : ACCSystem) :
     Function.Injective χ.solsInclLinSols := by
-  sorry
+  intro S T h
+  have h' : χ.solsInclQuadSols S = χ.solsInclQuadSols T := by
+    apply ACCSystemQuad.quadSolsInclLinSols_injective (χ := χ.toACCSystemQuad)
+    simpa [ACCSystem.solsInclLinSols, MulActionHom.comp_apply] using h
+  exact solsInclQuadSols_injective χ h'
 
 /-!