Commit 2025-12-11 08:08 053b764a

fix(Algebra/Field): ensure Field.toGrindField.toInv is def-eq to Field.toInv (#32711) This PR fixes an issue where the Inv instance obtained from Field.toGrindField was not definitionally equal to Field.toInv under instance reducibility. This caused grind to fail. Reported at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/non.20def-eq.20.60Inv.60.20instances.20in.20.60Discriminant.2EDifferent.60 🤖 Prepared with Claude Code