Theorems · Definition · commutative algebra

Module.AEval

(R : Type u_1) →
  (M : Type u_2) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module A M] → [inst_5 : Module R M] → [IsScalarTower R A M] → A → Type u_2

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).

Defined in

Mathlib.Algebra.Polynomial.Module.AEval

Cited by

18 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebraAddCommMonoidModuleModuleIsScalarTower