Prove2Me

Unitary maps commute with real scalars

Proved
BookProof.ChapterUnitaryTransport.map_real_smul

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

spectral-theorytimepiece

A complex-linear unitary map commutes with real scalar multiplication, because a real scalar is a complex scalar with vanishing imaginary part.

W(rx)=r Wx(r∈R).W(r x) = r\, Wx \qquad (r\in\mathbb{R}).

Formalization Note. The real action is Complex.coe_smul.

Preamble
import Mathlib
import Definitions.Def_ChapterUnitaryTransport
open BookProof.ChapterUnitaryTransport
open scoped InnerProductSpace
Formal statement
theorem BookProof.ChapterUnitaryTransport.map_real_smul {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (r : ℝ) (x : H) : W (r • x) = r • W x := by sorry
Source
timepiece BookProof, ChapterUnitaryTransport.lean, theorem map_real_smul

View graph