ker_quotQuotMk

Mathlib.RingTheory.Ideal.Quotient.Operations

URI: https://scilib.ai/kg/mathlib#DoubleQuot.ker_quotQuotMk

← MathLib Explorer

English

The kernel of quotQuotMk equals I ⊔ J.

Русский

Ядро quotQuotMk равно I ⊔ J.

LaTeX

$$$\\ker(\\mathrm{quotQuotMk}\\; I\\; J) = I \\sqcup J$$$

Lean4

/-- The kernel of `quotQuotMk` -/
theorem ker_quotQuotMk : RingHom.ker (quotQuotMk I J) = I ⊔ J := by
  rw [RingHom.ker_eq_comap_bot, quotQuotMk, ← comap_comap, ← RingHom.ker, mk_ker,
    comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective, ← RingHom.ker, mk_ker, sup_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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