instDistribMulActionSubtypeMemAddSubgroupOfStarModule

English

If R acts on A and A has a star-structure, then the distributive multiplication action restricts to self-adjoint elements of A.

Русский

Если R действует на A и A имеет звездообразную структуру, то распределяемое умножение ограничивается самосопряжёнными элементами A.

LaTeX

$$$ [\\text{Monoid } R] [\\text{DistribMulAction } R A] [\\text{StarModule } R A] \\Rightarrow \\text{DistribMulAction } R (\\mathrm{selfAdjoint}(A)). $$$

Lean4

instance [Monoid R] [DistribMulAction R A] [StarModule R A] : DistribMulAction R (selfAdjoint A) :=
  Function.Injective.distribMulAction (selfAdjoint A).subtype Subtype.coe_injective val_smul

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