Theorems · Theorem · field theory

minpoly.dvd

∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  (Polynomial.aeval x) p = 0 → minpoly A x ∣ p

If an element x is a root of a polynomial p, then the minimal polynomial of x divides p. See also minpoly.isIntegrallyClosed_dvd which relaxes the assumptions on A in exchange for stronger assumptions on B.

Defined in

Mathlib.FieldTheory.Minpoly.Field

Cited by

31 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebra