instIsScalarTower — Mathlib

English

IsScalarTower lifts to ZeroHom: with SMul M N and IsScalarTower M N B, we have IsScalarTower M N (ZeroHom A B).

Русский

IsScalarTower поднимается до ZeroHom: при наличии SMul M N и IsScalarTower M N B имеем IsScalarTower M N (ZeroHom A B).

LaTeX

$$[SMul M N] [SMulZeroClass M B] [SMulZeroClass N B] [IsScalarTower M N B] : IsScalarTower M N (ZeroHom A B)$$

Lean4

instance [SMul M N] [SMulZeroClass M B] [SMulZeroClass N B] [IsScalarTower M N B] : IsScalarTower M N (ZeroHom A B)
    where smul_assoc _ _ _ := ext fun _ => smul_assoc _ _ _

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