Theorems · Theorem · commutative algebra

AdjoinRoot.lift_of

∀ {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) {x : R}, (AdjoinRoot.lift i a h) ((AdjoinRoot.of f) x) = i x

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRing