quotAdjoinRootEquivQuotPolynomialQuot_mk_of

English

The mk of p under quotAdjoinRootEquivQuotPolynomialQuot corresponds to the image under the span of f.

Русский

mk p через quotAdjoinRootEquivQuotPolynomialQuot соответствует изображению через span f.

LaTeX

$$quotAdjoinRootEquivQuotPolynomialQuot_mk_of: = (quotAdjoinRootEquivQuotPolynomialQuot I f (Ideal.Quotient.mk (I.map (of f)) (mk f p)) = Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])) (p.map (Ideal.Quotient.mk I)))$$

Lean4

@[simp]
theorem quotAdjoinRootEquivQuotPolynomialQuot_mk_of (p : R[X]) :
    quotAdjoinRootEquivQuotPolynomialQuot I f (Ideal.Quotient.mk (I.map (of f)) (mk f p)) =
      Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])) (p.map (Ideal.Quotient.mk I)) :=
  rfl

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