quotientSpanXSubCAlgEquiv_mk — Mathlib

English

The evaluation map descends to an algebra isomorphism: evaluating a polynomial at x induces an isomorphism between R[X] modulo the ideal generated by X − Cx and the quotient R by the ideal generated by x.

Русский

Оценивание многочлена в x порождает изоморфизм по алгебраическим структурам: равенство X − Cx порождает изоморфизм между R[X] / ⟨X − Cx⟩ и R / ⟨x⟩.

LaTeX

$$$\\bigl(R[X] / \\langle X - C x \\rangle\\bigr) \\cong_R R / \\langle x \\rangle$$$

Lean4

@[simp]
theorem quotientSpanXSubCAlgEquiv_mk (x : R) (p : R[X]) :
    quotientSpanXSubCAlgEquiv x (Ideal.Quotient.mk _ p) = p.eval x :=
  rfl

Похожие утверждения