K : Type u_1
E : Type ?u.4450828
inst✝ : IsROrC K
z : K
⊢ 0 ≤ ↑normSq z ∧ ¬↑normSq z = 0 ↔ z ≠ 0
K : Type u_1
E : Type ?u.4450828
inst✝ : IsROrC K
z : K
⊢ 0 < ↑normSq z ↔ z ≠ 0
rw [lt_iff_le_and_ne, Ne, eq_comm]
no goals
K : Type u_1
E : Type ?u.4450828
inst✝ : IsROrC K
z : K
⊢ 0 ≤ ↑normSq z ∧ ¬↑normSq z = 0 ↔ z ≠ 0
simp [normSq_nonneg]