mem_ker

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#RingHom.mem_ker

← MathLib Explorer

English

For any r in R, r lies in the kernel of f if and only if f(r) = 0.

Русский

Для любого элемента r из R верно: r принадлежит ядру f тогда и только тогда, когда f(r) = 0.

LaTeX

$$$r \\in \\ker f \\iff f(r) = 0$$$

Lean4

/-- An element is in the kernel if and only if it maps to zero. -/
@[simp]
theorem mem_ker {r} : r ∈ ker f ↔ f r = 0 := by rw [ker, Ideal.mem_comap, Submodule.mem_bot]

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

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

Разделы

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

Аффилиация

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