PolynomialModule.eval_single

theorem PolynomialModule.eval_single : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (i : ℕ) (m : M), (PolynomialModule.eval r) ((PolynomialModule.single R i) m) = r ^ i • m

The theorem `PolynomialModule.eval_single` states that for any commutative ring `R`, any additively commutative group `M`, and any module `M` over `R`, for any element `r` of `R`, natural number `i`, and element `m` of `M`, evaluating the monomial `m * x ^ i` at `r` (using the function `PolynomialModule.eval`) is equal to `r ^ i` times `m`. In mathematical terms, it means `p(r) = r^i * m` where `p` is a polynomial represented as `m * x ^ i`. This provides a specific case of how to evaluate a polynomial at a specific point in the context of a module over a ring.

More concisely: For any commutative ring R, additively commutative group M, and module M over R, for all r in R, natural number i, and m in M, the evaluation of the monomial m * x^i in R via PolynomialModule.eval equals r^i * m.