lidOfCompatibleSMul — Mathlib

English

If the R-action on M and the A-action on A and M satisfy the compatibility conditions in both directions, then the tensor product A ⊗R M is canonically isomorphic to M as an A-module.

Русский

Если действия R на M и A на A и M совместимы в обе стороны, то тензорное произведение A ⊗R M канонически изоморфно M как A-модуль.

LaTeX

$$$A \\otimes_R M \\;\\cong_A\\; M$$$

Lean4

/-- If the R- and A- action on A and M satisfy `CompatibleSMul` both ways,
then `A ⊗[R] M` is canonically isomorphic to `M`. -/
def lidOfCompatibleSMul : A ⊗[R] M ≃ₗ[A] M :=
  (equivOfCompatibleSMul R A A M).symm ≪≫ₗ TensorProduct.lid _ _

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