instIsScalarTower — Mathlib

English

There is a scalar tower structure on the space of continuous alternating maps: if a ∈ R', b ∈ R'', then a • (b • f) = (a • b) • f for any f in the space of continuous alternating maps.

Русский

На пространстве непрерывных чередующих отображений существует структура цепи скаляров: для любых a ∈ R', b ∈ R'' и f выполняется a • (b • f) = (a • b) • f.

LaTeX

$$$ IsScalarTower\\ R'\\ R'' (M [⋀^ι]→L[A] N) $$$

Lean4

instance [SMul R' R''] [IsScalarTower R' R'' N] : IsScalarTower R' R'' (M [⋀^ι]→L[A] N) :=
  ⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

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