instStarModuleSubtypeMemSubmonoid

English

There is a scalar tower structure for unitary subtypes, mirroring the underlying tower of the ambient monoids.

Русский

Существует структура башни скаляров для подтипов унитарных элементов, повторяющая башню скаляров исходных моноидов.

LaTeX

$$$\\text{IsScalarTower}(\\mathrm{unitary}(R), \\mathrm{unitary}(S), \\mathrm{unitary}(A))$$$

Lean4

instance : StarModule (unitary R) (unitary A) where star_smul _ _ := Subtype.ext <| star_smul (_ : R) _

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