`BookProof.MixedLinearEsa.hasDerivAt_gaugeFun_line` (b m : V) (hm : m ≠ 0) (x : V) : HasDerivAt (fun t : ℝ => gaugeFun b m (x + t • m)) (gaugeFun b m x * (Complex.I * ((-(inner ℝ x

Initializing...

`BookProof.MixedLinearEsa.hasDerivAt_gaugeFun_line` (b m : V) (hm : m ≠ 0) (x : V) : HasDerivAt (fun t : ℝ => gaugeFun b m (x + t • m)) (gaugeFun b m x * (Complex.I * ((-(inner ℝ x · Prove2Me