equivalent_one_zero_neg_one_weighted_sum_squared

English

The tmul operation on quadratic forms is associative with respect to TensorProduct.assoc; i.e., Q1.tmul (Q2.tmul Q3) composed with assoc equals (Q1.tmul Q2).tmul Q3.

Русский

Операция tmul над квадратичными формами ассоциативна по отношению к TensorProduct.assoc: Q1.tmul (Q2.tmul Q3) = (Q1.tmul Q2).tmul Q3.

LaTeX

$$$(Q_1 \\tmul (Q_2 \\tmul Q_3)) \\circ \\mathrm{TensorProduct}.assoc = ((Q_1 \\tmul Q_2) \\tmul Q_3)$$$

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. -/
theorem equivalent_one_zero_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
    [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
    ∃ w : Fin (Module.finrank ℝ M) → ℝ, (∀ i, w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) :=
  let ⟨w, hw⟩ := Q.equivalent_signType_weighted_sum_squared
  ⟨(w ·), fun i ↦ by cases h : w i <;> simp [h], hw⟩

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