smulCommClass' — Mathlib

English

There is a scalar tower structure: IsScalarTower(R1, R2, ⨂[R] i, s i).

Русский

Существует структура степенного тензорного произведения: IsScalarTower(R1, R2, ⨂[R] i, s i).

LaTeX

$$$ \text{IsScalarTower } R_1 R_2 (\PiTensorProduct(R, s)) $$$

Lean4

instance smulCommClass' [SMulCommClass R₁ R₂ R] : SMulCommClass R₁ R₂ (⨂[R] i, s i) :=
  ⟨fun {r' r''} x ↦
    PiTensorProduct.induction_on' x (fun {xr xf} ↦ by simp only [smul_tprodCoeff', smul_comm]) fun {z y} ihz ihy ↦ by
      simp_rw [PiTensorProduct.smul_add, ihz, ihy]⟩

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