nonUnitalRing — Mathlib

English

The MonoidAlgebra R M inherits a nonunital ring structure (i.e., a ring without multiplicative identity) from R and M when M is a semigroup.

Русский

MonoidAlgebra R M наследует структуру кольца без единицы, если M — полугруппа.

LaTeX

$$$\\mathrm{NonUnitalRing}(\\mathrm{MonoidAlgebra}(R,M)).$$$

Lean4

@[to_additive (dont_translate := R)]
instance nonUnitalRing [Semigroup M] : NonUnitalRing (MonoidAlgebra R M) where

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