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₁)