mk_comp_algebraMap — Mathlib

English

For an ideal I in a ring A, the composition of the quotient.mk map with the algebraMap from a base ring to A/I equals the canonical map to HasQuotient.Quotient A I; i.e., Quotient.mk I ∘ algebraMap = algebraMap to quotient.

Русский

Для идеала I в кольце A композиция мапы quotient.mk с алгебраическим отображением из осн. кольца в A/I равна канонической карте в HasQuotient.Quotient A I.

LaTeX

$$$ (\operatorname{Quotient.mk} I) \circ (\operatorname{algebraMap} R \_ A) = \operatorname{algebraMap} R (A \ / I). $$$

Lean4

@[simp]
theorem mk_comp_algebraMap (I : Ideal A) [I.IsTwoSided] :
    (Quotient.mk I).comp (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I) :=
  rfl

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