instModuleSubtypeMemAddSubgroupOfStarModule

English

If A is a module over a semiring R and StarModule R A holds, then the self-adjoint subset of A is a module over R.

Русский

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

LaTeX

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

Lean4

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

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