isScalarTower' — Mathlib

English

There is an instance IsScalarTower for R, R, and the PiTensorProduct, i.e., the tower law holds for the canonical scalar actions.

Русский

Существует экземпляр IsScalarTower для R, R и PiTensorProduct, то есть правило башни действует для канонических скалярных действий.

LaTeX

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

Lean4

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

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