`BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift` (s t : ℝ) (x y : H) : ⟪ y, G.U s (G.U t x) ⟫_ℂ = ⟪ G.U (-s) y, G.U t x ⟫_ℂ

Initializing...

`BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift` (s t : ℝ) (x y : H) : ⟪ y, G.U s (G.U t x) ⟫_ℂ = ⟪ G.U (-s) y, G.U t x ⟫_ℂ · Prove2Me