kerLiftAlg_mk

Mathlib.RingTheory.Ideal.Quotient.Operations

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

English

The canonical lifting maps the coset of an element to its image: kerLiftAlg f (a mod ker f) = f(a).

Русский

Каноническое поднятие отправляет косет элемента в его образ: kerLiftAlg f (a mod ker f) = f(a).

LaTeX

$$$ kerLiftAlg f (\operatorname{Quotient.mk} (\ker f) a) = f(a)$$$

Lean4

@[simp]
theorem kerLiftAlg_mk (f : A →ₐ[R₁] B) (a : A) : kerLiftAlg f (Quotient.mk (RingHom.ker f) a) = f a := by rfl

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

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

Разделы

Аффилиация

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