mulActionBaseChange_smul_tmul

Mathlib.RingTheory.Kaehler.TensorProduct

URI: https://scilib.ai/kg/mathlib#KaehlerDifferential.mulActionBaseChange_smul_tmul

English

The A-action distributes over the tensor product: a • (s ⊗ x) = s ⊗ (a • x).

Русский

Действие A над тензорным произведением распределяется: a · (s ⊗ x) = s ⊗ (a · x).

LaTeX

$$$a \\cdot (s \\otimes x) = s \\otimes (a \\cdot x).$$$

Lean4

@[simp]
theorem mulActionBaseChange_smul_tmul (a : A) (s : S) (x : Ω[A⁄R]) : a • (s ⊗ₜ[R] x) = s ⊗ₜ (a • x) :=
  rfl

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

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

Разделы

Аффилиация

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