no goals
R : Type v
n : Type w
inst✝⁴ : Fintype n
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (∀ (i : n), i ∈ Finset.univ → v i * star (v i) = 0) ↔ v = 0
simp [Function.funext_iff, mul_eq_zero]