Theorems · Definition · field theory

FixedPoints.minpoly

(G : Type u) →
  [inst : Group G] →
    (F : Type v) →
      [inst_1 : Field F] → [inst_2 : MulSemiringAction G F] → [Fintype G] → F → Polynomial ↥(FixedPoints.subfield G F)

minpoly G F x is the minimal polynomial of (x : F) over FixedPoints.subfield G F.

Defined in

Mathlib.FieldTheory.Fixed

Cited by

9 results in Mathlib

Foundations

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

Assumes

GroupFieldMulSemiringActionFintype