instModuleTensorProductMop — Mathlib

English

There is a natural bimodule structure of A on A ⊗_R A^{op} turning it into an A-module via the tensor product construction.

Русский

Существует естественная структура би-модуля над A на A ⊗_R A^{op}, делающая этот тензорный продукт модулем над A.

LaTeX

$$$\text{instModuleTensorProductMop}: \text{Module} (A \otimes_R A^{op})\, A$$$

Lean4

/-- `A` as a `A ⊗[R] Aᵐᵒᵖ`-module (or equivalently, an `A`-`A` bimodule). -/
abbrev instModuleTensorProductMop : Module (A ⊗[R] Aᵐᵒᵖ) A :=
  TensorProduct.Algebra.module

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