mk₂'_apply

Mathlib.LinearAlgebra.BilinearMap

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

English

A tensor product of symmetric bilinear forms is symmetric.

Русский

Тензорное произведение симметричных билинейных форм симметрично.

LaTeX

$$$$ (B_1 \ tmul B_2).IsSymm $$$$

Lean4

@[simp]
theorem mk₂'_apply (f : M → N → Pₗ) {H1 H2 H3 H4} (m : M) (n : N) :
    (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] Pₗ) m n = f m n :=
  rfl

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

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

Разделы

Аффилиация

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