adjoin_tmul_eq_top — Mathlib

English

The subalgebra generated by all simple tensors a ⊗ b (with a ∈ A, b ∈ B) equals the whole tensor product algebra A ⊗_R B.

Русский

Подалгебра, порождённая всеми простыми тензорными тензорами a ⊗ b, порождает всё тензорное произведение A ⊗_R B.

LaTeX

$$$ \\operatorname{adjoin}_{R} \\{ a \\otimes b \mid a \\in A, b \\in B \\} = \\top $$$

Lean4

theorem adjoin_tmul_eq_top : adjoin R {t : A ⊗[R] B | ∃ a b, a ⊗ₜ[R] b = t} = ⊤ :=
  top_le_iff.mp <| (top_le_iff.mpr <| span_tmul_eq_top R A B).trans (span_le_adjoin R _)

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