associated_tmul — Mathlib

English

The polar bilinear form of the tmul of Q1 and Q2 equals the tensor product of the polar bilinear forms, scaled by 1/2.

Русский

Полярная билинейная форма tmul образует Q1 ⊗ Q2 как произведение полярных форм, умноженное на 1/2.

LaTeX

$$$\\text{polarBilin}(Q_1 \\otimes Q_2) = \\tfrac{1}{2} \\; \\text{BilinForm.tmul}(\\text{polarBilin}(Q_1), \\text{polarBilin}(Q_2))$$$

Lean4

theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
    (Q₁.tmul Q₂).associated = BilinForm.tmul Q₁.associated Q₂.associated :=
  by
  rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul, ←
    QuadraticMap.associated_tmul Q₁ Q₂]
  aesop

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