From 4a0e6a97efffcdf7071304b1fff1d12db70d16af Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 5 Jan 2025 22:50:23 +0100 Subject: [PATCH] fix @Basis.mk --- Mathlib/RingTheory/AdjoinRoot.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean index 36a2d4a72e50f..e9fcd0a5fad9c 100644 --- 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 -