mkₐ_toRingHom

Mathlib.RingTheory.Ideal.Quotient.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.mkₐ_toRingHom

English

The coercion of mkₐ as a function coincides with the ordinary mk map.

Русский

Сопоставление mkₐ как функция совпадает с обычным mk.

LaTeX

$$$ (mkₐ^{R_1}_I) = mk_I $$$

Lean4

theorem mkₐ_toRingHom (I : Ideal A) [I.IsTwoSided] : (Quotient.mkₐ R₁ I).toRingHom = Ideal.Quotient.mk I :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru