quotQuotMkₐ_toRingHom

Mathlib.RingTheory.Ideal.Quotient.Operations

URI: https://scilib.ai/kg/mathlib#DoubleQuot.quotQuotMkₐ_toRingHom

English

The equality of quotQuotMkₐ to RingHom holds, showing the canonical MK map is a RingHom.

Русский

Равенство quotQuotMkₐ и RingHom демонстрирует, что каноническое MK-отображение является RingHom.

LaTeX

$$$quotQuotMkₐ R I J = quotQuotMk I J$$$

Lean4

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

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

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

Разделы

Аффилиация

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