mkₐ_eq_mk — Mathlib

English

For a commutative base ring R and an ideal I ⊆ A, the algebra map from R to R/I equals the composition of the map R → A → A/I.

Русский

Для коммутативного основания R и идеала I ⊆ A, алгебраическое отображение R → R/I равно композиции R → A → A/I.

LaTeX

$$$ \text{algebraMap}_R^{R/I} = (\text{Quotient.mk}_I) \circ (\text{algebraMap}_{R,A}) $$$

Lean4

@[simp]
theorem mkₐ_eq_mk (I : Ideal A) [I.IsTwoSided] : ⇑(Quotient.mkₐ R₁ I) = Quotient.mk I :=
  rfl

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