instSMul

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.instSMul

English

There is a scalar action of R on the type M →ₚₗ[R] N, defined by smul.

Русский

Существует скалярное действие R на множество M →ₚₗ[R] N, определяемое smul.

LaTeX

$$$\text{instance } : SMul\ R\ (M \to_p_l[R] N)$ with $r \cdot f := (PolynomialLaw\.smul\ R\ M\ N\ r\ f)$.$$

Lean4

instance : SMul R (M →ₚₗ[R] N) :=
  ⟨smul⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru