ker_algebraMap_residueField

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

URI: https://scilib.ai/kg/mathlib#Ideal.ker_algebraMap_residueField

← MathLib Explorer

English

Kernel equality as in the previous item, restated.

Русский

Равенство ядра, как в предыдущем пункте.

LaTeX

$$$\ker(\mathrm{algebraMap}\; R \; I.\mathrm{ResidueField}) = I.$$$

Lean4

@[simp high] -- marked `high` to override the more general `FaithfulSMul.ker_algebraMap_eq_bot`

theorem ker_algebraMap_residueField : RingHom.ker (algebraMap R I.ResidueField) = I :=
  Ideal.ext fun _ ↦ Ideal.algebraMap_residueField_eq_zero

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

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

Разделы

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

Аффилиация

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