bot_right — Mathlib

English

The images of the left and right inclusion maps into a tensor product are linearly disjoint inside the tensor product.

Русский

Образы вложений слева и справа в тензорном произведении линейно дизъюнктны друг другу внутри тензорного произведения.

LaTeX

$$$\text{range} \,(\text{includeLeft}) \; \text{LinearDisjoint} \; \text{range} \,(\text{includeRight})$$$

Lean4

/-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/
theorem bot_right : A.LinearDisjoint ⊥ :=
  by
  rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
  exact Submodule.LinearDisjoint.one_right _

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