Theorem IsSepClosed.exists_aeval_eq_zero

Modification history

2025-11-06 02:33
Mathlib/FieldTheory/IsSepClosed.lean
feat(FieldTheory/IsAlgClosed/Basic): generalize `exists_aeval_eq_zero` (#31311) …
Modified IsSepClosed.exists_aeval_eq_zeroView on Github →
2025-11-05 17:11
Mathlib/FieldTheory/IsSepClosed.lean
feat(Algebra/Polynomial): small and useful lemmas (#29956)
Modified IsSepClosed.exists_aeval_eq_zeroView on Github →
2023-08-14 12:56
Mathlib/FieldTheory/IsSepClosed.lean
feat(Mathlib/FieldTheory/IsSepClosed) separably closed field and separable closure - basic definition (#6285) …
Added IsSepClosed.exists_aeval_eq_zeroView on Github →