isCentralScalar — Mathlib

English

There exists a central scalar structure: N acts centrally on MonoidAlgebra R M when IsCentralScalar N R holds and the opposite action also respects centrality.

Русский

Существует структура центрального скаляра: N действует в центре MonoidAlgebra R M при выполнении IsCentralScalar N R и соответствующего противоположного действия.

LaTeX

$$$\\text{IsCentralScalar } N\\ (MonoidAlgebra\\ R\\ M)$$$

Lean4

@[to_additive (dont_translate := N) isCentralScalar]
instance isCentralScalar [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] :
    IsCentralScalar N (MonoidAlgebra R M) :=
  Finsupp.isCentralScalar ..

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