prodRight_tmul_fst

Mathlib.RingTheory.TensorProduct.Pi

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

English

piRightHom is compatible with algebraic structure and acts componentwise on a family.

Русский

piRightHom совместим со структурой алгебры и действует по компонентам на семейство.

LaTeX

$$piRightHom_mul and related properties$$

Lean4

@[simp]
theorem prodRight_tmul_fst (a : A) (x : B × C) : (prodRight R S A B C (a ⊗ₜ x)).fst = a ⊗ₜ x.1 :=
  rfl

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

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

Разделы

Аффилиация

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