Update Sun Sep 8 01:30:10 EDT 2024

hrmacbeth · Sep 8, 2024 · 686abc6 · 686abc6
1 parent 6ff653f
commit 686abc6
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/PolyrithTutorial/02_Using_Polyrith/solutions/Solutions01Chebyshev.lean b/PolyrithTutorial/02_Using_Polyrith/solutions/Solutions01Chebyshev.lean
@@ -42,5 +42,4 @@ theorem mul_T : ∀ m : ℕ, ∀ k, 2 * T m * T (m + k) = T (2 * m + k) + T k
     have h₂ := T_add_two (2 * m + k + 2)
     have h₃ := T_add_two k
     ring_nf at H₁ H₂ h₁ h₂ h₃ ⊢
-    -- FIXME polyrith needs a type annotation
-    linear_combination 2 * (X : ℤ[X]) * H₁ - 1 * H₂ + 2 * T (2 + m + k) * h₁ - 1 * h₂ - 1 * h₃
+    linear_combination 2 * X * H₁ - 1 * H₂ + 2 * T (2 + m + k) * h₁ - 1 * h₂ - 1 * h₃