English
The AEval construction inherits an additive group structure from M when M is an additive commutative group.
Русский
Конструкция AEval наследует структуру аддитивной группы от M, когда M является аддитивной коммутативной группой.
LaTeX
$$$ \\text{AddGroup}(AEval\\,R\\,M\\,a) \\cong \\text{AddGroup}(M) $$$
Lean4
/-- Suppose `a` is an element of an `R`-algebra `A` and `M` is an `A`-module.
Loosely speaking, `Module.AEval R M a` is 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 R M a` has elements `Module.AEval.of R M a m` for `m : M`,
and the action of `f` is `f • (of R M a m) = of R M a ((aeval a f) • m)`.
-/
@[nolint unusedArguments]
def AEval (R M : Type*) {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module A M]
[Module R M] [IsScalarTower R A M] (_ : A) :=
M
