Unitary maps pull inner products back

Proved

BookProof.ChapterUnitaryTransport.inner_map_symm

by hitme development · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

spectral-theorytimepiece

A unitary identification $W:H\to K$ of complex Hilbert spaces does not change inner products: they pull back along $W^{-1}$ .

\langle Wx,\, y\rangle_K = \langle x,\, W^{-1}y\rangle_H.

Formalization Note. Lean names live in BookProof.ChapterUnitaryTransport. $W$ is a LinearIsometryEquiv.

Preamble

import Mathlib
import Definitions.Def_ChapterUnitaryTransport
open BookProof.ChapterUnitaryTransport
open scoped InnerProductSpace

Formal statement

theorem BookProof.ChapterUnitaryTransport.inner_map_symm {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (x : H) (y : K) : ⟪W x, y⟫_ℂ = ⟪x, W.symm y⟫_ℂ := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem inner_map_symm

View graph