∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {x : E}, (inner A x x = 0) = (x = 0)