`BookProof.OdeUnitaryFlow.odeKoop_neg_odeKoop` (t : ℝ) (ψ : ℝ → ℂ) (x : ℝ) (hx : x ∈ flowDom (-t)) : odeKoop (-t) (odeKoop t ψ) x = ψ x

Initializing...

`BookProof.OdeUnitaryFlow.odeKoop_neg_odeKoop` (t : ℝ) (ψ : ℝ → ℂ) (x : ℝ) (hx : x ∈ flowDom (-t)) : odeKoop (-t) (odeKoop t ψ) x = ψ x · Prove2Me