smulZeroClass — Mathlib

English

There is a SMulZeroClass structure on MonoidAlgebra R M induced from a type A acting on R; i.e., the scalar action by elements of A interacts with zero as usual.

Русский

Для MonoidAlgebra R M существует структура SMulZeroClass, полученная из действия типа A на R; т.е. скалярное действие элементов A над R взаимодействует с нулём обычным образом.

LaTeX

$$$\\text{MonoidAlgebra}(R,M)$ inherits a SMulZeroClass structure from $A$ via the embedding $A \\curvearrowright R$.$$

Lean4

@[to_additive (dont_translate := A) smulZeroClass]
instance smulZeroClass : SMulZeroClass A (MonoidAlgebra R M) :=
  Finsupp.smulZeroClass

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