ring — Mathlib

English

The MonoidAlgebra R M carries a ring structure whenever M is a monoid and R a ring, i.e., MonoidAlgebra R M is a ring with standard addition and convolution-like multiplication.

Русский

MonoidAlgebra R M образует кольцо, когда M — моноид, а R — кольцо; сложение и свёртка умножения соответствуют обычной конструкции.

LaTeX

$$$\\mathrm{Ring}(\\mathrm{MonoidAlgebra}(R,M))$$$

Lean4

@[to_additive (dont_translate := R)]
instance ring [Monoid M] : Ring (MonoidAlgebra R M) where

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