English
Given a function f from X to an R-algebra A, liftFun extends f to a function from Pre R X to A, preserving of, add, mul, and scalar operations.
Русский
Дано отображение f: X → A в R-алгебру A; liftFun расширяет f до отображения Pre R X → A, сохраняя операции of, add, mul и скаляры.
LaTeX
$$$liftFun\\{R, X, A\\} (f) : Pre R X \\to A$ defined by\n f on .of, +, *, and .ofScalar$$
Lean4
/-- Given a function from `X` to an `R`-algebra `A`, `lift_fun` provides a lift of `f` to a function
from `Pre R X` to `A`. This is mainly used in the construction of `FreeAlgebra.lift`. -/
def liftFun {A : Type*} [Semiring A] [Algebra R A] (f : X → A) : Pre R X → A
| .of t => f t
| .add a b => liftFun f a + liftFun f b
| .mul a b => liftFun f a * liftFun f b
| .ofScalar c => algebraMap _ _ c
