algebraMapInv

Mathlib.Algebra.FreeAlgebra

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.algebraMapInv

English

The left inverse of the algebra map is given by lift R (0 : X → R).

Русский

Левое обратное отображения algebraMap задается через lift R (0 : X → R).

LaTeX

$$$\mathrm{algebraMapInv} = \mathrm{lift}_R (0: X \to R) : FreeAlgebra(R,X) \to_A R$$$

Lean4

/-- The left-inverse of `algebraMap`. -/
def algebraMapInv : FreeAlgebra R X →ₐ[R] R :=
  lift R (0 : X → R)

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

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

Разделы

Аффилиация

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