Theorem IsConjRoot.isIntegral

Modification history

2024-10-26 13:22

Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

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

Added IsConjRoot.isIntegral View on Github →