liftSupQuotQuotMkₐ_toRingHom — Mathlib

English

The coercion of liftSupQuotQuotMkₐ equals liftSupQuotQuotMk, i.e., the MK-lift respects the RingHom structure.

Русский

Неявное преобразование liftSupQuotQuotMkₐ равно liftSupQuotQuotMk; MK-подъем сохраняет структуру RingHom.

LaTeX

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

Lean4

@[simp]
theorem liftSupQuotQuotMkₐ_toRingHom :
    (liftSupQuotQuotMkₐ R I J : _ →+* _ ⧸ J.map (Quotient.mkₐ R I)) = liftSupQuotQuotMk I J :=
  rfl

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