Theorems · Theorem · commutative algebra

AdjoinRoot.lift_root

∀ {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), (AdjoinRoot.lift i a h) (AdjoinRoot.root f) = a

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRing