Theorem isConjRoot_iff_mem_minpoly_aroots

Modification history

2024-10-26 13:22
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
feat(FieldTheory): define `IsConjRoot` and prove its basic properties (#17783) …
Added isConjRoot_iff_mem_minpoly_arootsView on Github →