`BookProof.FockCubicQuarticStability.quart_form_eq` (k : ℕ) (u : FockAlg) : (inner ℂ (toLp u) (toLp (quartA k u)) : ℂ).re = ‖toLp (annA k (annA k u))‖ ^ 2

Initializing...

`BookProof.FockCubicQuarticStability.quart_form_eq` (k : ℕ) (u : FockAlg) : (inner ℂ (toLp u) (toLp (quartA k u)) : ℂ).re = ‖toLp (annA k (annA k u))‖ ^ 2 · Prove2Me