kerLift_mk

Mathlib.RingTheory.Ideal.Quotient.Operations

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

English

The map kerLift f, applied to the coset of r modulo ker f, yields f(r).

Русский

Применение kerLift к косету r по ker f дает f(r).

LaTeX

$$$$\kerLift\,f\; (\overline{r}) = f(r).$$$$

Lean4

@[simp]
theorem kerLift_mk (r : R) : kerLift f (Ideal.Quotient.mk (ker f) r) = f r :=
  Ideal.Quotient.lift_mk _ _ _

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

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

Разделы

Аффилиация

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