isScalarTower_left — Mathlib

English

Under suitable commutation, the scalar action from R'' on M ⊗_R N commutes with all tensor factors, making it central.

Русский

При условии совместимости скаляров, действие из R'' на M ⊗_R N коммутирует с тензорными множителями и образует центральный элемент.

LaTeX

$$$\text{IsCentralScalar}_{R''}(M \otimes_R N)$$$

Lean4

/-- `IsScalarTower R'₂ R' M` implies `IsScalarTower R'₂ R' (M ⊗[R] N)` -/
instance isScalarTower_left [IsScalarTower R'₂ R' M] : IsScalarTower R'₂ R' (M ⊗[R] N) :=
  ⟨fun s r x =>
    x.induction_on (by simp) (fun m n => by rw [smul_tmul', smul_tmul', smul_tmul', smul_assoc]) fun x y ihx ihy => by
      rw [smul_add, smul_add, smul_add, ihx, ihy]⟩

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