fix @Basis.mk

leanprover-community · Jan 5, 2025 · 4a0e6a9 · 4a0e6a9
1 parent 51ffcb5
commit 4a0e6a9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean
@@ -506,7 +506,7 @@ def powerBasisAux (hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f) := b
     rw [natDegree_mul hf, natDegree_C, add_zero]
     · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
   have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
-  apply @Basis.mk _ _ _ fun i : Fin f.natDegree => root f ^ i.val
+  apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
   · rw [← deg_f', ← minpoly_eq]
     exact linearIndependent_pow (root f)
   · rintro y -