Theorems · Definition · commutative algebra

AdjoinRoot.map

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) → (p : Polynomial R) → (q : Polynomial S) → q ∣ Polynomial.map f p → AdjoinRoot p →+* AdjoinRoot q

The canonical homomorphism from AdjoinRoot p to AdjoinRoot q induced by f : R →+* S, where the polynomial q : S[X] divides f(p) : R[X].

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommRingCommRing