toModule — Mathlib

English

A semiring R is turned into a module over itself by multiplication: R is a left module over R with r · s = rs.

Русский

Кольцо-полугруппа R трактуется как левый модуль над собой: r · s = rs.

LaTeX

$$$\\text{Module } R R \\text{ with } r \\cdot s = rs$$$

Lean4

instance (priority := 910) toModule [Semiring R] : Module R R
    where
  smul_add := mul_add
  add_smul := add_mul
  zero_smul := zero_mul
  smul_zero := mul_zero

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