`BookProof.BrstLeakage.norm_unitary_apply` {U : E →L[ℂ] E} (hU : U ∈ unitary (E →L[ℂ] E)) (x : E) : ‖U x‖ = ‖x‖

Initializing...

`BookProof.BrstLeakage.norm_unitary_apply` {U : E →L[ℂ] E} (hU : U ∈ unitary (E →L[ℂ] E)) (x : E) : ‖U x‖ = ‖x‖ · Prove2Me