tmul_isSymm — Mathlib

English

The bilinear form tmul is the canonical tensor product of two bilinear forms: (B1 ⊗ B2)(m1 ⊗ m2, n1 ⊗ n2) = B1(m1, n1) B2(m2, n2).

Русский

Билинейная форма tmul есть каноническое тензорное произведение двух билинейных форм: (B1 ⊗ B2)(m1 ⊗ m2, n1 ⊗ n2) = B1(m1, n1) B2(m2, n2).

LaTeX

$$$ (B_1 \\otimes B_2)(m_1 \\otimes m_2,\, n_1 \\otimes n_2) = B_1(m_1, n_1) \\, B_2(m_2, n_2). $$$

Lean4

/-- A tensor product of symmetric bilinear maps is symmetric. -/
theorem tmul_isSymm {B₁ : BilinMap A M₁ N₁} {B₂ : BilinMap R M₂ N₂} (hB₁ : ∀ x y, B₁ x y = B₁ y x)
    (hB₂ : ∀ x y, B₂ x y = B₂ y x) (x y : M₁ ⊗[R] M₂) : B₁.tmul B₂ x y = B₁.tmul B₂ y x :=
  by
  revert x y
  rw [isSymm_iff_eq_flip]
  aesop

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