instModule — Mathlib

English

There is a module structure of PolynomialModule R M over any S with IsScalarTower S R M.

Русский

Существует структура модуля для PolynomialModule R M над любым S с IsScalarTower S R M.

LaTeX

$$$\text{Module\ S} (PolynomialModule R M)$$$

Lean4

/-- This is required to have the `IsScalarTower S R M` instance to avoid diamonds. -/
@[nolint unusedArguments]
noncomputable instance : Module S (PolynomialModule R M) :=
  Finsupp.module ℕ M

Похожие утверждения