equivalent_weightedSumSquares_units_of_nondegenerate'

English

If Q is nondegenerate, there exists a weight function w with values in units K^× such that Q is equivalent to weightedSumSquares with weights w.

Русский

Если $Q$ непроходима, существует функция весов, принимающих значения в единицах поля, так что $Q$ эквивалентна weightedSumSquares с весами $w$.

LaTeX

$$$\exists w: Fin(\mathrm{finrank}_K V) \to K^\times,\; Q \;\text{Equivalent}\; \operatorname{weightedSumSquares} K w$$$

Lean4

theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm K V)
    (hQ : (associated (R := K) Q).SeparatingLeft) :
    ∃ w : Fin (Module.finrank K V) → Kˣ, Equivalent Q (weightedSumSquares K w) :=
  by
  obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
  have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ
  simp_rw [LinearMap.IsOrtho, associated_eq_self_apply] at hv₂
  exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

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