instSMulCommClass — Mathlib

English

If 𝕜 acts on γ and 𝕜' acts on γ with IsScalarTower, then α →ₘ[μ] γ inherits a compatible IsScalarTower structure.

Русский

Если 𝕜 действует на γ и 𝕜' действует на γ, удовлетворяя IsScalarTower, то α →ₘ[μ] γ наследует совместную структуру IsScalarTower.

LaTeX

$$$ IsScalarTower 𝕜 𝕜' (α \to_{μ} γ) $$$

Lean4

instance instSMulCommClass [SMulCommClass 𝕜 𝕜' γ] : SMulCommClass 𝕜 𝕜' (α →ₘ[μ] γ) :=
  ⟨fun a b f => induction_on f fun f hf => by simp_rw [smul_mk, smul_comm]⟩

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