instIsScalarTower — Mathlib

English

If SMul M N, SMul M α, SMul N α and IsScalarTower M N α hold, then there is an IsScalarTower M N αᵐᵒᵖ with smul_assoc transported via unop.

Русский

Если заданы SMul M N, SMul M α, SMul N α и IsScalarTower M N α, то существует IsScalarTower M N αᵐᵒᵖ, где тождество умножения сохраняет ассоциативность через unop.

LaTeX

$$$\text{If } SMul M N, SMul M α, SMul N α, IsScalarTower M N α\text{, then } IsScalarTower M N α^{\mathrm{op}}$ with smul_assoc congruent via unop.$$

Lean4

@[to_additive]
instance instIsScalarTower [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower M N αᵐᵒᵖ where
  smul_assoc _ _ _ := unop_injective <| smul_assoc _ _ _

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