`BookProof.ChapterG2.no_translation_invariant_unit_vector` {G : Type*} [Group G] [Infinite G] : ¬ ∃ Ψ : lp (fun _ : G => ℂ) 2, ‖Ψ‖ = 1 ∧ ∀ g x : G, Ψ (g * x) = Ψ x

Initializing...

`BookProof.ChapterG2.no_translation_invariant_unit_vector` {G : Type*} [Group G] [Infinite G] : ¬ ∃ Ψ : lp (fun _ : G => ℂ) 2, ‖Ψ‖ = 1 ∧ ∀ g x : G, Ψ (g * x) = Ψ x · Prove2Me