instIsScalarTowerComplex — Mathlib

English

There is a canonical scalar-tower structure linking α, Real, and Complex, expressing associativity of scalar multiplication when α acts through Real into Complex.

Русский

Существует каноническая структура- «скалярного башмака» между α, Real и Complex, выражающая ассоциативность умножения на скаляры, когда α действует через Real на Complex.

LaTeX

$$$\text{IsScalarTower } α \mathbb{R} \mathbb{C}$ holds, i.e., (a • r) • c = a • (r • c) for all a ∈ α, r ∈ ℝ, c ∈ ℂ.$$

Lean4

local instance : IsScalarTower α ℂ ℂ where smul_assoc a y z := by simpa using smul_assoc (a • (1 : ℝ)) y z

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