fix merge

loefflerd · loefflerd · commit 0b967b2ef405 · 2024-10-30T22:42:09.000+01:00
diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
@@ -488,7 +488,7 @@ theorem T_mul_apply_one (g : SL(2, ℤ)) : (T * g) 1 = g 1 := by
 theorem T_inv_mul_apply_one (g : SL(2, ℤ)) : (T⁻¹ * g) 1 = g 1 := by
   simpa using T_pow_mul_apply_one (-1) g
 
-lemma S_mul_S_eq : (↑ₘS * ↑ₘS) = -1 := by
+lemma S_mul_S_eq : (S : Matrix (Fin 2) (Fin 2) ℤ) * S = -1 := by
   simp only [S, Int.reduceNeg, pow_two, coe_mul, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd,
     vecMul_cons, head_cons, zero_smul, tail_cons, neg_smul, one_smul, neg_cons, neg_zero, neg_empty,
     empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply]
