instIsScalarTower — Mathlib

English

If 𝕜 has a central action on γ, then it also acts centrally on α →ₘ[μ] γ.

Русский

Если 𝕜 действует централизованно на γ, то он действует централизованно и на α →ₘ[μ] γ.

LaTeX

$$$ IsCentralScalar 𝕜 (α \to_{μ} γ) $$$

Lean4

instance instIsScalarTower [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' γ] : IsScalarTower 𝕜 𝕜' (α →ₘ[μ] γ) :=
  ⟨fun a b f => induction_on f fun f hf => by simp_rw [smul_mk, smul_assoc]⟩

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