English
AEval' is a specialization of AEval where the base algebra is the endomorphism algebra of M over R.
Русский
AEval' есть специализация AEval, где базовый алгебра является алгеброй эндоморфизмов M над R.
LaTeX
$$$\text{AEval}'\; = \text{AEval}\; R\ M\ \varphi$ для $\varphi : M \to M$ линейного отображения по $R$$$
Lean4
/-- Given and `R`-module `M` and a linear map `φ : M →ₗ[R] M`, `Module.AEval' φ` is loosely speaking
the `R[X]`-module with elements `m : M`, where the action of a polynomial $f$ is given by
$f • m = f(a) • m$.
More precisely, `Module.AEval' φ` has elements `Module.AEval'.of φ m` for `m : M`,
and the action of `f` is `f • (of φ m) = of φ ((aeval φ f) • m)`.
`Module.AEval'` is defined as a special case of `Module.AEval` in which the `R`-algebra is
`M →ₗ[R] M`. Lemmas involving `Module.AEval` may be applied to `Module.AEval'`.
-/
abbrev AEval' :=
AEval R M φ
