ker

Mathlib.RingTheory.TwoSidedIdeal.Kernel

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.ker

Lean4

/-- The kernel of a ring homomorphism, as a two-sided ideal.
-/
def ker : TwoSidedIdeal R :=
  .mk {
      r := fun x y ↦ f x = f y
      iseqv := by constructor <;> aesop
      mul' := by intro; simp_all
      add' := by intro; simp_all }

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

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

Разделы

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

Аффилиация

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