instMulActionSubtypeMemAddSubgroupOfStarModule

English

If R acts on A and A carries a star-structure, then the subset of self-adjoint elements of A is preserved under the action of R.

Русский

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

LaTeX

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

Lean4

instance [Monoid R] [MulAction R A] [StarModule R A] : MulAction R (selfAdjoint A) :=
  Function.Injective.mulAction Subtype.val Subtype.coe_injective val_smul

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