Commit 2025-11-06 02:33 0f6314af
View on Github →feat(FieldTheory/IsAlgClosed/Basic): generalize exists_aeval_eq_zero (#31311)
from CommRing+IsSimpleRing to CommSemiring+FaithfulSMul.
Mathlib.Algebra.Algebra.IsSimpleRing contains an instance of FaithfulSMul given IsSimpleRing if needed.