kerLift_injective

Mathlib.RingTheory.Ideal.Quotient.Operations

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

← MathLib Explorer

English

The induced map kerLift f: R/ker f → S is injective.

Русский

Отображение kerLift f: R/ker f → S инъективно.

LaTeX

$$$$\text{kerLift } f\; \text{injective}.$$$$

Lean4

/-- The induced map from the quotient by the kernel is injective. -/
theorem kerLift_injective : Function.Injective (kerLift f) :=
  lift_injective_of_ker_le_ideal (ker f) (fun a => by simp only [mem_ker, imp_self]) le_rfl

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

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

Разделы

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

Аффилиация

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