Theorem not_mem_iff_exists_ne_and_isConjRoot

Modification history

2025-05-25 12:30

Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

chore(*): not_mem/nmem -> notMem (#25159)

Deleted not_mem_iff_exists_ne_and_isConjRoot View on Github →

2024-10-26 13:22

Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

feat(FieldTheory): define `IsConjRoot` and prove its basic properties (#17783) …

Added not_mem_iff_exists_ne_and_isConjRoot View on Github →