ofTensorProduct_tmul

Mathlib.RingTheory.AdicCompletion.AsTensorProduct

URI: https://scilib.ai/kg/mathlib#AdicCompletion.ofTensorProduct_tmul

English

The map ofTensorProduct I M respects tensor product by sending r ⊗ x to r • of I M x.

Русский

Карта ofTensorProduct сохраняет тензорный произведение: r ⊗ x ↦ r • of I M x.

LaTeX

$$ofTensorProduct(I,M)(r ⊗ x) = r • of(I,M)(x)$$

Lean4

@[simp]
theorem ofTensorProduct_tmul (r : AdicCompletion I R) (x : M) : ofTensorProduct I M (r ⊗ₜ x) = r • of I M x := by
  simp [ofTensorProduct]

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

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

Разделы

Аффилиация

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