tmul — Mathlib

English

If B1 and B2 are symmetric bilinear forms, then their tensor product B1.tm ul B2 is symmetric as a bilinear form on the tensor product space.

Русский

Если B1 и B2 симметричные билинейные формы, то их тензорное произведение симметрично по аргументам.

LaTeX

$$$$ (B_1 \ tmul B_2)^{\mathrm{IsSymm}}. $$$$

Lean4

/-- A tensor product of symmetric bilinear forms is symmetric. -/
theorem _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
    (B₁.tmul B₂).IsSymm := by
  rw [LinearMap.isSymm_iff_eq_flip]
  ext x₁ x₂ y₁ y₂
  exact congr_arg₂ (HSMul.hSMul) (hB₂.eq x₂ y₂) (hB₁.eq x₁ y₁)

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