English
Tensor product of quadratic forms is commutative up to a canonical isometry, i.e., Q1.tmul Q2 is isometric to Q2.tmul Q1 via tensorComm.
Русский
Тензорное произведение квадратных форм допускает каноническую изометрическую перестановку порядка факторов: Q1.tmul Q2 ≅ Q2.tmul Q1 через tensorComm.
LaTeX
$$$ (Q_1 \\tmul Q_2) \\cong (Q_2 \\tmul Q_1) $ via the isometry given by tensorComm$$
Lean4
/-- **Sylvester's law of inertia**: A real quadratic form is equivalent to a weighted
sum of squares with the weights being ±1 or 0, `SignType` version. -/
theorem equivalent_signType_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M]
(Q : QuadraticForm ℝ M) :
∃ w : Fin (Module.finrank ℝ M) → SignType, Equivalent Q (weightedSumSquares ℝ fun i ↦ (w i : ℝ)) :=
let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares
⟨sign ∘ w, ⟨hw₁.trans (isometryEquivSignWeightedSumSquares w)⟩⟩
