quotQuotEquivComm_symm_mk_mk — Mathlib

English

Symmetric image under the inverse of quotQuotEquivComm aligns the mk image with the expected quotient.

Русский

Образ симметрично в обратном направлении эквив Про квот-сквозной симметрии соответствует ожидаемому квотированному отображению.

LaTeX

$$$\text{quotQuotEquivComm_symm_mk_mk}: (\text{quotQuotEquivComm})^{\,-1} (\mathrm{mk}(f)) = \mathrm{mk}(f)$$$

Lean4

@[simp]
theorem quotQuotEquivComm_symm_mk_mk (p : R[X]) :
    (Polynomial.quotQuotEquivComm I f).symm
        (Ideal.Quotient.mk (span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))))
          (Ideal.Quotient.mk (I.map C) p)) =
      Ideal.Quotient.mk (span {f.map (Ideal.Quotient.mk I)}) (p.map (Ideal.Quotient.mk I)) :=
  by simp only [Polynomial.quotQuotEquivComm, quotientEquiv_symm_mk, polynomialQuotientEquivQuotientPolynomial_symm_mk]

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