Commit 2024-10-26 13:22 8a7de7ec

feat(FieldTheory): define IsConjRoot and prove its basic properties (#17783) We define the property IsConjRoot K x y as two elements having the same minimal polynomial over K. We show that it is equivalent to the existence of an algebra equivalence σ : L ≃ₐ[K] L such that y = σ x. We also show that if x is a separable element over K and the minimal polynomial of x splits in L, then x is not in the K iff there exists a different conjugate root of x in L over K. Most of the properties have a similar version already proved in Mathlib.