diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean
index acb79d7aa336a..d91338b3850cf 100644
--- a/Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean
+++ b/Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean
@@ -163,7 +163,7 @@ theorem gaussSum_frob (χ : MulChar R R') (ψ : AddChar R R') :
 /-- For a quadratic character `χ` and when the characteristic `p` of the target ring
 is a unit in the source ring, the `p`th power of the Gauss sum of`χ` and `ψ` is
 `χ p` times the original Gauss sum. -/
--- Porting note: TODO
+-- Porting note: Added `nonrec` to avoid error `failed to prove termination`
 nonrec theorem MulChar.IsQuadratic.gaussSum_frob (hp : IsUnit (p : R)) {χ : MulChar R R'}
     (hχ : IsQuadratic χ) (ψ : AddChar R R') : gaussSum χ ψ ^ p = χ p * gaussSum χ ψ := by
   rw [gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit, ← mul_assoc,