coe_quotQuotEquivQuotSupₐ_symm — Mathlib

English

The underlying function of the symmetry-involved isomorphism between the two-step quotients coincides with the standard symmetry map on the two-step quotients; in particular, the simplification (coe) of the symmetry is identical to the standard symmetry’s function.

Русский

Функциональная реализация симметричного перехода между двумяступенчатыми фактор-кольцами совпадает с обычной реализацией симметрии между ними; то есть одно и то же отображение задаётся двумя эквивалентными способами.

LaTeX

$$$\text{coe}((\text{quotQuotEquivQuotSup}_a\, R\, I\, J)^{-1}) = \text{coe}((\text{quotQuotEquivQuotSup}\, I\, J)^{-1})$$$

Lean4

@[simp]
theorem coe_quotQuotEquivQuotSupₐ_symm : ⇑(quotQuotEquivQuotSupₐ R I J).symm = (quotQuotEquivQuotSup I J).symm :=
  rfl

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