isometryEquivSumSquaresUnits — Mathlib

English

If w:ι → Units(ℂ) is a weight function, then the weighted sum of squares with weights w is isometric to the standard sum of squares with unit weights, via the unit-weight expansion.

Русский

Если w:ι → Units(ℂ) задаёт веса, то взвешенная сумма квадратов с весами w изоморфна стандартной сумме квадратов с единичными весами.

LaTeX

$$$ IsometryEquiv\\ (weightedSumSquares\\ ℂ w)\\ (weightedSumSquares\\ ℂ 1) $$$

Lean4

/-- The isometry between a weighted sum of squares on the complex numbers and the
sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/
noncomputable def isometryEquivSumSquaresUnits (w : ι → Units ℂ) :
    IsometryEquiv (weightedSumSquares ℂ w) (weightedSumSquares ℂ (1 : ι → ℂ)) := by
  simpa using isometryEquivSumSquares ((↑) ∘ w)

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