Theorems · Definition · field theory

RatFunc.minpolyX

{K : Type u_1} →
  [inst : Field K] →
    (f : RatFunc K) → (A : Type u_2) → [inst_1 : CommRing A] → [Algebra K A] → [Algebra (↥K[f]) A] → Polynomial A

The minimal polynomial of X over K⟮f⟯. It is defined as f.num - f * f.denom, viewed as a polynomial with coefficients in A, where A is a K[f]-algebra.

Defined in

Mathlib.FieldTheory.RatFunc.IntermediateField

Cited by

12 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebraAlgebra