quotQuotEquivQuotOfLEₐ_symm_toRingEquiv

English

If I ≤ J, then the symmetry of quotQuotEquivQuotOfLEₐ R h corresponds to the symmetry of quotQuotEquivQuotOfLE h as a ring equivalence.

Русский

Если I ≤ J, то симметрия quotQuotEquivQuotOfLEₐ R h соответствует симметрии quotQuotEquivQuotOfLE h как кольцевого эквив.

LaTeX

$$$((quotQuotEquivQuotOfLEₐ R h)^{-1}) = (quotQuotEquivQuotOfLE h)^{-1}$$$

Lean4

@[simp]
theorem quotQuotEquivQuotOfLEₐ_symm_toRingEquiv (h : I ≤ J) :
    ((quotQuotEquivQuotOfLEₐ R h).symm : _ ≃+* _ ⧸ J.map (Quotient.mkₐ R I)) = (quotQuotEquivQuotOfLE h).symm :=
  rfl

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