`BookProof.NsLagrangianDet.dispField_im` (kv : K → Fin 3 → ℝ) (y : DIdx K → ℝ) (a : Fin 3 → ℝ) (i : Fin 3) : (dispField kv y a i).im = 0

Initializing...

`BookProof.NsLagrangianDet.dispField_im` (kv : K → Fin 3 → ℝ) (y : DIdx K → ℝ) (a : Fin 3 → ℝ) (i : Fin 3) : (dispField kv y a i).im = 0 · Prove2Me