coe_quotQuotEquivQuotOfLEₐ_symm

English

The ring-equivalence underlying quotQuotEquivQuotOfLEₐ R h has the same underlying function as the standard RingEquiv quotQuotEquivQuotOfLE h.

Русский

Кольцевое эквивалентное отображение quotQuotEquivQuotOfLEₐ R h имеет ту же самую функцию-основу, что и стандартное RingEquiv quotQuotEquivQuotOfLE h.

LaTeX

$$$\text{toRingEquiv}((quotQuotEquivQuotOfLEₐ R h)) = quotQuotEquivQuotOfLE h$$$

Lean4

@[simp]
theorem coe_quotQuotEquivQuotOfLEₐ_symm (h : I ≤ J) :
    ⇑(quotQuotEquivQuotOfLEₐ R h).symm = (quotQuotEquivQuotOfLE h).symm :=
  rfl

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