quotQuotEquivComm_symmₐ — Mathlib

English

The symmetry of quotQuotEquivCommₐ is the same as the symmetry of quotQuotEquivComm; i.e., the inverse maps coincide under swapping the ideals.

Русский

Симметрия quotQuotEquivCommₐ совпадает с симметрией quotQuotEquivComm; то есть обратные отображения совпадают при обмене идеалов.

LaTeX

$$$(quotQuotEquivQuotOfLEₐ\, R\, I\, J)^{-1} = (quotQuotEquivQuotOfLE\, I\, J)^{-1}$$$

Lean4

@[simp]
theorem quotQuotEquivComm_symmₐ : (quotQuotEquivCommₐ R I J).symm = quotQuotEquivCommₐ R J I := by rfl

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