Theorems · Definition · field theory

IsConjRoot

(R : Type u_1) → {A : Type u_5} → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → A → A → Prop

We say that y is a conjugate root of x over K if the minimal polynomial of x is the same as the minimal polynomial of y.

Defined in

Mathlib.FieldTheory.Minpoly.IsConjRoot

Cited by

43 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra