English
The symm of llift applied to f and evaluated at x equals f evaluated at singleton x 1.
Русский
Симметричное применение llift к f на x равно f(одиночный x 1).
LaTeX
$$$$ llift\; M\; R\; S\; X \; .\; symm\; f\; x = f(\mathrm{single}(x,1)). $$$$
Lean4
/-- Given compatible `S` and `R`-module structures on `M` and a type `X`, the set of functions
`X → M` is `S`-linearly equivalent to the `R`-linear maps from the free `R`-module
on `X` to `M`. -/
noncomputable def llift : (X → M) ≃ₗ[S] (X →₀ R) →ₗ[R] M :=
{ lift M R X with
map_smul' := by
intros
dsimp
ext
simp only [coe_comp, Function.comp_apply, lsingle_apply, lift_apply, Pi.smul_apply, sum_single_index, zero_smul,
one_smul, LinearMap.smul_apply] }
