Identity transports to identity

Proved

BookProof.ChapterUnitaryTransport.transportUnitary_zero

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

spectral-theorytimepiece

If $U$ is the identity on $H$ , the conjugated operator is the identity on $K$ .

U = I_H \quad\Longrightarrow\quad W U W^{-1} = I_K.

Formalization Note. A pointwise identity hypothesis is enough.

Preamble

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

Formal statement

theorem BookProof.ChapterUnitaryTransport.transportUnitary_zero {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (U : H ≃ₗᵢ[ℂ] H) (h : ∀ x : H, U x = x) (y : K) : transportUnitary W U y = y := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportUnitary_zero

View graph