prodRight_tmul

Mathlib.RingTheory.TensorProduct.Pi

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.prodRight_tmul

English

If R→A and R→B are injective and A,B are domains, then A ⊗_R B is nontrivial.

Русский

Если инъективны отображения R→A и R→B и A,B — домены, то A ⊗_R B не тривиален.

LaTeX

$$Nontrivial (A ⊗_R B)$$

Lean4

theorem prodRight_tmul (a : A) (x : B × C) : prodRight R S A B C (a ⊗ₜ x) = (a ⊗ₜ x.1, a ⊗ₜ x.2) :=
  rfl

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

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

Разделы

Аффилиация

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