Theorems · Theorem · commutative algebra

AdjoinRoot.lift_mk

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
  (h : Polynomial.eval₂ i a f = 0) (g : Polynomial R),
  (AdjoinRoot.lift i a h) ((AdjoinRoot.mk f) g) = Polynomial.eval₂ i a g

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRing