instIsScalarTower — Mathlib

English

There is a relationship IsScalarTower between S, T and the DoubleCentralizer: smul_assoc holds via ext on the underlying maps, i.e. (s • t) • a = s • (t • a) for s ∈ S, t ∈ T, a ∈ 𝓜(𝕜,A).

Русский

Существует отношение IsScalarTower между S, T и DoubleCentralizer: выполняется associativity smul через отображения, то есть (s • t) • a = s • (t • a).

LaTeX

$$$$ \\text{smul\_assoc}(s,t,a): (s \\cdot t) \\cdot a = s \\cdot (t \\cdot a) \\quad\\text{для всех } s \\in S, t \\in T, a \\in 𝓜(𝕜,A) $$$$

Lean4

instance instIsScalarTower [SMul S T] [IsScalarTower S T A] : IsScalarTower S T 𝓜(𝕜, A) where
  smul_assoc _ _ a := ext (𝕜 := 𝕜) (A := A) _ _ <| smul_assoc _ _ a.toProd

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