instIsScalarTowerSubtypeMemSubmonoid

English

The IsScalarTower instance holds for unitary subtypes, reflecting interactions between unitary R, S, and A.

Русский

Существуют инстансы IsScalarTower для подтипов унитарных элементов, отображающие взаимодействия unitary(R), unitary(S) и unitary(A).

LaTeX

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

Lean4

instance [IsScalarTower R S S] [SMulCommClass R S S] [IsScalarTower R S A] :
    IsScalarTower (unitary R) (unitary S) (unitary A) where
  smul_assoc _ _ _ := Subtype.ext <| smul_assoc _ (_ : S) (_ : A)

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