instSMulCommClassTensorProduct_1

Mathlib.RingTheory.Kaehler.TensorProduct

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

English

There is a SMulCommClass between A, S and the tensor product S ⊗R Ω[A/R].

Русский

Существует SMulCommClass между A, S и тензорным произведением S ⊗R Ω[A/R].

LaTeX

$$$\\text{SMulCommClass } A S (S \\otimes_R \\Omega[A/R]).$$$

Lean4

instance : SMulCommClass A S (S ⊗[R] Ω[A⁄R]) where smul_comm s a x := by rw [← smul_comm]

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

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

Разделы

Аффилиация

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