Theorem isConjRoot_zero_iff_eq_zero_of_injective

Modification history

2026-01-13 19:40
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified isConjRoot_zero_iff_eq_zero_of_injectiveView on Github →
2024-10-26 13:22
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
feat(FieldTheory): define `IsConjRoot` and prove its basic properties (#17783) …
Added isConjRoot_zero_iff_eq_zero_of_injectiveView on Github →