instModuleSubtypeMemAddSubgroupOfStarModule

English

The self-adjoint subtype of A forms a module over R when A is a module over R.

Русский

Подтип самосопряжённых элементов A образует модуль над R, если A является модулем над R.

LaTeX

$$$ [\\text{Semiring } R] [\\text{Module } R A] [\\text{StarModule } R A] \\Rightarrow \\text{Module } R (\\mathrm{skewAdjoint}(A)). $$$

Lean4

instance [Semiring R] [Module R A] [StarModule R A] : Module R (skewAdjoint A) :=
  Function.Injective.module R (skewAdjoint A).subtype Subtype.coe_injective val_smul

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