R : Type u_1
inst✝ : CommRing R
v : Fin 3 → R
⊢ v 1 * v 2 - v 1 * v 2 = 0 ∧ v 0 * v 2 - v 0 * v 2 = 0 ∧ v 0 * v 1 - v 0 * v 1 = 0 ∧ ![] = 0
R : Type u_1
inst✝ : CommRing R
v : Fin 3 → R
⊢ ↑(↑crossProduct v) v = 0
simp_rw [cross_apply, mul_comm, cons_eq_zero_iff]
no goals
R : Type u_1
inst✝ : CommRing R
v : Fin 3 → R
⊢ v 1 * v 2 - v 1 * v 2 = 0 ∧ v 0 * v 2 - v 0 * v 2 = 0 ∧ v 0 * v 1 - v 0 * v 1 = 0 ∧ ![] = 0
exact ⟨sub_self _, sub_self _, sub_self _, zero_empty.symm⟩