Theorems · Definition · commutative algebra

AdjoinRoot.Minpoly.toAdjoin

(R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (x : S) → AdjoinRoot (minpoly R x) →ₐ[R] ↥R[x]

The surjective algebra morphism R[X]/(minpoly R x) → R[x]. If R is an integrally closed domain and x is integral, this is an isomorphism, see minpoly.equivAdjoin.

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra