tensorProductTo_tmul

Mathlib.RingTheory.Kaehler.Basic

URI: https://scilib.ai/kg/mathlib#Derivation.tensorProductTo_tmul

English

For a derivation D, on simple tensors, D(s ⊗ t) equals s times D(t) in the tensor product context.

Русский

Для выводной операции D на простые тензоры выполняется D(s ⊗ t) = s · D(t).

LaTeX

$$D.tensorProductTo (s ⊗ t) = s • D t$$

Lean4

theorem tensorProductTo_tmul (D : Derivation R S M) (s t : S) : D.tensorProductTo (s ⊗ₜ t) = s • D t :=
  rfl

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

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

Разделы

Аффилиация

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