Theorem minpoly.ker_aeval_eq_span_minpoly

Modification history

2024-01-26 04:28
Mathlib/FieldTheory/Minpoly/Field.lean
feat: the minimal polynomial is a generator of the annihilator ideal (#10008) …
Added minpoly.ker_aeval_eq_span_minpolyView on Github →