piRight_tmul

Mathlib.RingTheory.TensorProduct.Pi

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

English

For all x ∈ A and f ∈ ∀ i, B i, piRight (x ⊗ f) equals the function i ↦ x ⊗ f i.

Русский

Для всех x ∈ A и f ∈ ∀ i, B_i, piRight (x ⊗ f) равно функция i ↦ x ⊗ f(i).

LaTeX

$$piRight_tmul$$

Lean4

@[simp]
theorem piRight_tmul (x : A) (f : ∀ i, B i) : piRight R S A B (x ⊗ₜ f) = (fun j ↦ x ⊗ₜ f j) :=
  rfl

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

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

Разделы

Аффилиация

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