instBracketTensorProduct

Mathlib.Algebra.Lie.BaseChange

URI: https://scilib.ai/kg/mathlib#LieAlgebra.ExtendScalars.instBracketTensorProduct

English

The bracket on pure tensors satisfies [s ⊗ x, t ⊗ y] = (s t) ⊗ [x, y] for s,t ∈ A, x ∈ L, y ∈ M.

Русский

Скобка на простых тензорах удовлетворяет формуле [s ⊗ x, t ⊗ y] = (s t) ⊗ [x, y].

LaTeX

$$$⁅s \otimes x, t \otimes y⁆ = (s t) \otimes ⁅x,y⁆ \quad( s,t \in A, x \in L, y \in M ).$$$

Lean4

instance : Bracket (A ⊗[R] L) (A ⊗[R] M) where bracket x m := bracket' R A L M x m

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru