coe_factorₐ — Mathlib

English

The AlgHom version of the factor morphism coincides with the standard factor morphism; the coercion to a ring homomorphism is the same in both presentations.

Русский

Версия фактор-морфизма в виде AlgHom совпадает с обычной версией фактор-морфизма; преобразование к кольцевому гомоморфизму одинаково в обоих представлениях.

LaTeX

$$$(Ideal.Quotient.factorₐ R_1 hIJ) : A ⧸ I →+* A ⧸ J = Ideal.Quotient.factor hIJ$$$

Lean4

@[simp]
theorem coe_factorₐ : (Ideal.Quotient.factorₐ R₁ hIJ : A ⧸ I →+* A ⧸ J) = Ideal.Quotient.factor hIJ :=
  rfl

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