instIsScalarTower — Mathlib

English

There is a compatible IsScalarTower structure for the quotient c.Quotient, ensuring associativity of scalar actions across α, β, and M.

Русский

Существует совместимая структура IsScalarTower для фактор-модуля c.Quotient, обеспечивающая ассоциативность действий скаляров через α, β и M.

LaTeX

$$IsScalarTower α β c.Quotient$$

Lean4

instance instIsScalarTower {α β M : Type*} [MulOneClass M] [SMul α β] [SMul α M] [SMul β M] [IsScalarTower α M M]
    [IsScalarTower β M M] [IsScalarTower α β M] (c : Con M) : IsScalarTower α β c.Quotient where
  smul_assoc a b := Quotient.ind' fun m => congr_arg Quotient.mk'' <| smul_assoc a b m

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