quotQuotEquivCommₐ_toRingEquiv — Mathlib

English

The ring-algebra isomorphism quotQuotEquivCommₐ R I J defined from the commutative analogue is identical, as a function, to quotQuotEquivComm I J.

Русский

Указанный изоморфизм колец-алгебр quotQuotEquivCommₐ R I J по существу совпадает с прослеживаемым изоморфизмом quotQuotEquivComm I J по своей функции.

LaTeX

$$$(quotQuotEquivCommₐ R I J) = quotQuotEquivComm I J$$$

Lean4

@[simp]
theorem quotQuotEquivCommₐ_toRingEquiv :
    (quotQuotEquivCommₐ R I J : _ ⧸ J.map (Quotient.mkₐ R I) ≃+* _ ⧸ I.map (Quotient.mkₐ R J)) =
      quotQuotEquivComm I J :=
  rfl

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