mul'_apply

Mathlib.Algebra.Algebra.Bilinear

URI: https://scilib.ai/kg/mathlib#LinearMap.mul'_apply

English

The tensor-multiplication map mul' satisfies mul'(a ⊗ b) = a b.

Русский

Тензорное умножение mul' удовлетворяет mul'(a ⊗ b) = a b.

LaTeX

$$$$ mul'\,R\,A (a \otimes b) = ab. $$$$

Lean4

@[simp]
theorem mul'_apply {a b : A} : mul' R A (a ⊗ₜ b) = a * b :=
  rfl

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

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

Разделы

Аффилиация

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