∀ {R : Type u_1} {T : Type u_3} [inst : CommRing R] [inst_1 : Semiring T] {p : Polynomial R} {f g : AdjoinRoot p →+* T},
  f = g ↔ f.comp (AdjoinRoot.of p) = g.comp (AdjoinRoot.of p) ∧ f (AdjoinRoot.root p) = g (AdjoinRoot.root p)