no goals
S : Type ?u.477083
R : Type u_1
R₁ : Type ?u.477089
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ¬Anisotropic Q ↔ ∃ x, x ≠ 0 ∧ ↑Q x = 0
simp only [Anisotropic, not_forall, exists_prop, and_comm]