Theorems · Definition · number theory

QuadraticForm.isometryEquivSignWeightedSumSquares

{ι : Type u_1} →
  [inst : Fintype ι] →
    (w : ι → ℝ) →
      (QuadraticMap.weightedSumSquares ℝ w).IsometryEquiv
        (QuadraticMap.weightedSumSquares ℝ fun i => ↑(SignType.sign (w i)))

The isometry between a weighted sum of squares with weights u on the (non-zero) real numbers and the weighted sum of squares with weights sign ∘ u.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Real

Cited by

2 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype