linearEquivIncludeRange_tmul — Mathlib

English

For elements x in S and y in T, linearEquivIncludeRange maps x ⊗ y to rangeRestrict x ⊗ rangeRestrict y.

Русский

Для элементов x ∈ S и y ∈ T отображение линейного эквивIncludeRange переводит x ⊗ y в rangeRestrict x ⊗ rangeRestrict y.

LaTeX

$$$linearEquivIncludeRange R S T (x \\otimes y) = (includeLeft.rangeRestrict x) \\otimes (includeRight.rangeRestrict y)$$$

Lean4

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

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