algEquivIncludeRange_tmul — Mathlib

English

The algebra equivalence takes x ⊗ y to the tensor of the restricted x and y in their ranges.

Русский

Алгебраизоморфизм принимает x ⊗ y в тензор ограниченных x и y в их диапазонах.

LaTeX

$$$\\mathrm{algEquivIncludeRange}(R,S,T)(x \\otimes y) = (includeLeft.rangeRestrict x) \\otimes (includeRight.rangeRestrict y)$$$

Lean4

@[simp]
theorem algEquivIncludeRange_tmul (x y) :
    algEquivIncludeRange R S T (x ⊗ₜ[R] y) =
      ((includeLeft : S →ₐ[R] S ⊗[R] T).rangeRestrict x) ⊗ₜ[R] ((includeRight : T →ₐ[R] S ⊗[R] T).rangeRestrict y) :=
  rfl

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