equivOfCompatibleSMul — Mathlib

English

If the R- and S-actions on S and A satisfy compatibility in both ways, then s ⊗ a maps to s • a under lidOfCompatibleSMul.

Русский

Если действия R и S на S и A совместимы в обе стороны, то s ⊗ a отображается как s • a под lidOfCompatibleSMul.

LaTeX

$$$\\mathrm{lidOfCompatibleSMul}\\; R\\; S\\; A\\; (s \\otimes_R\\; a) = s \\cdot a$$$

Lean4

/-- If the R- and S-actions on A and B satisfy `CompatibleSMul` both ways,
then `A ⊗[S] B` is canonically isomorphic to `A ⊗[R] B`. -/
def equivOfCompatibleSMul [CompatibleSMul S R A B] : A ⊗[S] B ≃ₐ[S] A ⊗[R] B
    where
  __ := mapOfCompatibleSMul R S A B
  invFun := mapOfCompatibleSMul S R A B
  __ := _root_.TensorProduct.equivOfCompatibleSMul R S A B

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