quotQuotEquivQuotOfLE_symm_comp_mkₐ

English

The composition of the inverse of quotQuotEquivQuotOfLEₐ R h with quotQuotMkₐ R I J equals quotQuotMkₐ R J I.

Русский

Обратное отображение quotQuotEquivQuotOfLEₐ R h после quotQuotMkₐ R I J равно quotQuotMkₐ R J I.

LaTeX

$$$\text{(quotQuotEquivQuotOfLEₐ R h)^{-1}} \circ quotQuotMkₐ R I J = quotQuotMkₐ R J I$$$

Lean4

@[simp]
theorem quotQuotEquivQuotOfLE_symm_comp_mkₐ (h : I ≤ J) :
    AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h).symm) (Quotient.mkₐ R J) = quotQuotMkₐ R I J :=
  rfl

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