isScalarTower — Mathlib

English

There are dual scalar-tower structures on M ⊗_R N from both left and right actions that are compatible with each other.

Русский

Существуют две совместимые структуры башни скаляров слева и справа на M ⊗_R N.

LaTeX

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

Lean4

/-- A short-cut instance for the common case, where the requirements for the `compatible_smul`
instances are sufficient. -/
instance isScalarTower [SMul R' R] [IsScalarTower R' R M] : IsScalarTower R' R (M ⊗[R] N) :=
  TensorProduct.isScalarTower_left

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