instSMulSubtypeMemAddSubgroupOfStarModule

English

There is a scalar multiplication of R on the subtype skewAdjoint A, defined by r • x = ⟨r • (x : A)⟩, i.e., the action respects the subtype structure.

Русский

Существует скалярное умножение R на подтип skewAdjoint A, определённое как r • x = ⟨r • (x : A)⟩, которое сохраняет структуру подтипа.

LaTeX

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

Lean4

instance [Monoid R] [DistribMulAction R A] [StarModule R A] : SMul R (skewAdjoint A) where
  smul r x := ⟨r • (x : A), smul_mem r x.prop⟩

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