isScalarTower_right — Mathlib

English

There is a right scalar tower: if R'₂ acts on N in a suitable way, then (M ⊗_R N) inherits a scalar tower from R'₂ to R.

Русский

Существует правая тензорная скалярная башня: если R'₂ действует на N соответствующим образом, то (M ⊗_R N) наследует башню скаляров от R'₂ к R.

LaTeX

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

Lean4

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

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