quotLeftToQuotSupₐ_toRingHom — Mathlib

English

The coercion of the algebra hom quotLeftToQuotSupₐ R I J equals the underlying ring hom quotLeftToQuotSup I J.

Русский

Неявное преобразование алгебраического отображения quotLeftToQuotSupₐ совпадает с соответствующим кольцевым отображением quotLeftToQuotSup I J.

LaTeX

$$$\uparrow(quotLeftToQuotSupₐ R I J) = quotLeftToQuotSup I J$$$

Lean4

@[simp]
theorem quotLeftToQuotSupₐ_toRingHom : (quotLeftToQuotSupₐ R I J : _ →+* _) = quotLeftToQuotSup I J :=
  rfl

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