kerLiftAlg_injective

Mathlib.RingTheory.Ideal.Quotient.Operations

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

← MathLib Explorer

English

The induced algebra morphism kerLiftAlg f is injective.

Русский

Индукцируемый алгебра-гомоморфизм kerLiftAlg f инъективен.

LaTeX

$$$\text{Injective}(\kerLiftAlg f)$$$

Lean4

/-- The induced algebra morphism from the quotient by the kernel is injective. -/
theorem kerLiftAlg_injective (f : A →ₐ[R₁] B) : Function.Injective (kerLiftAlg f) :=
  RingHom.kerLift_injective (R := A) (S := B) f

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

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

Разделы

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

Аффилиация

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