∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R}, (0 < star v ⬝ᵥ v) = (v ≠ 0)