instIsScalarTowerSubtypeMem — Mathlib

English

If a subset s of α is endowed with compatible actions to form a SubMulAction, then the induced tower of actions is preserved on the subtype: m • (n • x) = (m • n) • x for all m ∈ M, n ∈ N, x ∈ s.

Русский

Если s ⊆ α образует SubMulAction с совместимыми действиями, то для подтипа сохраняется тензорная структура действия: m • (n • x) = (m • n) • x для всех m ∈ M, n ∈ N, x ∈ s.

LaTeX

$$$\\forall m \\in M, \\forall n \\in N, \\forall x \\in s:\\ (m \\cdot (n \\cdot x)) = ((m \\cdot n) \\cdot x)$$$

Lean4

instance (priority := 50) : IsScalarTower M N s where smul_assoc m n x := Subtype.ext (smul_assoc m n x.1)

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